红绿灯旋转

Question

首先我要说我对此很陌生，我必须在某些条件下做一个信号量。

我们将只为每个方向的一个交通灯建模（第二个只是重复相同的行为）。例如，在上图中，垂直灯为绿色，水平灯为红色。最初，两个方向都是红色的。当汽车到达时，它会被传感器检测到，并且其对应的灯会变为绿色。但是，这只有在另一个方向仍然是红色时才会发生；否则，它将等到另一个方向关闭。一旦任何一个方向变成绿色，它就会变成橙色（有一个计时器，但我们不会模拟延迟）然后它会再次变成红色。

实际上这是我现在的代码：

mtype = { red, yellow, green };
mtype light0 = red;
mtype light1 = red;

active proctype TL0() {
    do
        :: if
        :: light0 == red -> Ered: atomic {
            light1 == red; /* wait*/
            light0 = green;
        }
        :: light0 == green -> EY: light0 = yellow
        :: light0 == yellow -> EG: light0 =red
        fi;
        printf("The light0 is now %e\n", light0)
    od
}

active proctype TL1() {
    do
        :: if
        :: light1 == red -> Ered: atomic {
            light0 == red; /* wait*/
            light1 = green;
        }
        :: light1 == green -> EY: light1 = yellow
        :: light1 == yellow -> EG: light1 =red
        fi;
        printf("The light1 is now %e\n", light1)
    od
}

问题是当我使用

spin -a -f '<>(!TL0@Ered && !TL1@Ered)' sem3.pml

为了检查安全性我得到一个错误。

warning: never claim + accept labels requires -a flag to fully verify warning: for p.o. reduction to be valid the never claim must be stutter-invariant (never claims generated from LTL formulae are stutter-invariant) pan:1: assertion violated !(( !((TL0._p==Ered))&& !((TL1._p==Ered)))) (at depth 0) pan: wrote sem3.pml.trail

(Spin Version 6.4.8 -- 2 March 2018) Warning: Search not completed + Partial Order Reduction

Full statespace search for: never claim + (never_0) assertion violations + (if within scope of claim) acceptance
cycles - (not selected) invalid end states - (disabled by -E flag)

State-vector 36 byte, depth reached 0, errors: 1 1 states, stored 0 states, matched 1 transitions (= stored+matched) 0 atomic steps hash conflicts: 0 (resolved)

但实际上我不知道问题出在哪里:(

希望有人能帮助我

谢谢！

Answer 1

模型没问题，但我建议您手动生成验证器。

首先，在文件底部添加以下行：

ltl p1 { <>(!TL0@Ered && !TL1@Ered) };
ltl p2 { [] !(TL0@EY && TL1@EY) };     // perhaps you wanted (something like) this?

然后，生成验证器：

~$ spin -a file_name.pml
~$ gcc -o run pan.c
~$ ./run -a -N p1
...
~$ ./run -a -N p2
...

红绿灯旋转

Traffic light spin

semaphore

spin

promela