PCI总线控制协议
    PCI是Peripheral?Component?Interconnect（外围设备互联）的简称，是计算机上普遍使用的外设总线，所有PCI插槽上的设备都共享了这仅有的一个PCI总线，并且都通过这仅有的一个PCI总线连到了CPU，PCI实现上下之间的接口以协调数据的传送。
    当不同设备同时申请总线的使用权时，PCI需要一个仲裁器模块，此模块采取一定的设备调度策略分配使用权，如固定优先级调度策略和轮转优先级调度策略。

要验证的PPTL性质：
1.[](b_frame_switch -> <>!b_frame_switch)
含义：在所有状态下，如果数据开始传输，则未来某个状态完成数据传输，释放PCI总线的使用权。
模型满足该性质。

2.<>((scsi_ctrl.end_transaction) || (isa_bridge.end_transaction) || (vga_ctrl.end_transaction)&& processor.start_transaction)
含义：未来存在一个状态，scsi_ctrl、isa_bridge或vga_ctrl模块使用总线完成数据传输后，处理器模块同时开始处理。
模型不满足该性质。

3.[]((all_FP && scsi_ctrl.req) -> <>(arb.grant = 1))
含义：在所有状态下，如果采用固定优先级调度策略，scsi_ctrl模块提出申请后，未来存在状态， scsi_ctrl模块一定会获得总线使用权。
模型不满足该性质。

4.((all_FP && req) -> <>(grant))*
含义：此性质描述周期性的重复性质，采取固定优先级调度策略，一个模块获得总线使用权并进行数据传输后，所有模块继续申请并且能获得总线使用权，此过程是周期重复出现的。
模型不满足该性质。