Page 232 - 《软件学报》2021年第6期

1806 Journal of Software 软件学报 Vol.32, No.6, June 2021

Q 3 = ¬(p 3 ∧p 6 ).
性质 4. 在任意时刻,任一方向的红黄绿这 3 个灯同时只能亮一个,以主干道为例:
Q 4 = ((p 1 ⊕p 2 ⊕p 3 )∧¬(p 1 ∧p 2 ∧p 3 )).

5.4 性质描述文件
根据 UMC4M 工具的输入要求,将 PPTL 公式转化为 signal_light.p 文件.性质 1 的.p 文件的格式如下.
〈/
define p0:signal_light_top_rst=1;
define p1:signal_light_top_light1[2]=1;
define p2:signal_light_top_light1[1]=1;
define p3:signal_light_top_light1[0]=1;
define p4:signal_light_top_light2[2]=1;
define p5:signal_light_top_light2[1]=1;
define p6:signal_light_top_light2[0]=1;
alw(!p 0 →(p 2 and p 5 ))
/〉
性质 2 的.p 文件的格式如下:
〈/
define p 0 :signal_light_top_rst=1;
define p 1 :signal_light_top_light1[2]=1;
define p 2 :signal_light_top_light1[1]=1;
define p 3 :signal_light_top_light1[0]=1;
define p 4 :signal_light_top_light2[2]=1;
define p 5 :signal_light_top_light2[1]=1;
define p 6 :signal_light_top_light2[0]=1;
alw(p 0 →(som(p 3 ) and som(p 6 )))
/〉
性质 3 的.p 文件的格式如下:
〈/
define p 0 :signal_light_top_rst=1;
define p 1 :signal_light_top_light1[2]=1;
define p 2 :signal_light_top_light1[1]=1;
define p 3 :signal_light_top_light1[0]=1;
define p 4 :signal_light_top_light2[2]=1;
define p 5 :signal_light_top_light2[1]=1;
define p 6 :signal_light_top_light2[0]=1;
alw(!(p 3 and p 6 ))
/〉
性质 4 的.p 文件的格式如下:
〈/
define p 0 :signal_light_top_rst=1;
define p 1 :signal_light_top_light1[2]=1;
define p 2 :signal_light_top_light1[1]=1;