红绿灯旋转

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 %en", 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 %en", light1)
od
}

问题是当我使用

旋转 -a -f '<>(！TL0@Ered&&！TL1@Ered(' sem3.pml

为了检查安全性，我得到一个 erorr。

警告：从不声明 + 接受标签需要 -a 标志才能完全验证 警告：要使 P.O. 减少有效，"永不索赔"必须 口吃不变(从不从 LTL 公式生成的声明是 口吃不变量(平移：1：违反断言！(( !((TL0._p==Ered((&& !((TL1._p==埃雷德(((((深度 0( 平移：写入 SEM3.PML.Trail

(旋转版本 6.4.8 -- 2018 年 3 月 2 日(警告：搜索未完成 + 部分降阶

完整的状态空间搜索：从不声明 + (never_0( 断言冲突 +(如果在索赔范围内(接受
周期 -(未选择(无效的结束状态 -(由 -E 标志禁用(

状态向量 36 字节，深度达到 0，错误：1 1 个状态，已存储 0 个状态，匹配 1 个过渡(= 存储+匹配( 0 原子步骤哈希冲突：0(已解决(

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

希望有人能帮助我

感谢！

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
...