Spin工具交通灯状态机模型LTL验证报错排查求助

我来帮你一步步排查这个问题。先梳理你的需求和当前代码的核心问题，再解释验证报错的原因，最后给出修正方案。

需求回顾 #

你要实现的交通灯规则：

• 两个方向的交通灯初始均为红灯
• 只有当车辆触发传感器后，对应方向的灯才尝试转绿，且仅在另一方向为红灯时才能转绿，否则等待
• 绿灯后依次转为黄灯、红灯

当前代码的核心问题 #

你的Promela代码存在几个关键逻辑错误，这不仅会导致验证报错，还会违反交通灯的安全规则：

1. 缺少传感器触发逻辑 #

需求里明确是“车辆触发传感器后”才尝试转绿，但你的代码中没有任何传感器相关的变量或触发条件。两个交通灯进程会无限制地循环尝试转绿，完全忽略了“车辆触发”这个前提。

2. 等待逻辑错误（最关键） #

你在注释里写了/* wait*/，但代码里的light1 == red;只是一个布尔表达式计算，没有任何等待作用。Promela中要等待某个条件成立，必须使用await语句，否则代码会直接跳过条件检查，执行后续的灯色变更操作——这会导致即使另一方向是绿灯，当前方向也会强行转绿，违反安全规则。

3. Atomic块使用不当 #

当前的atomic块只是把两个语句打包成原子操作，但没有实现“仅当另一方向为红灯时才转绿”的逻辑。如果另一方向不是红灯，代码依然会执行light0 = green;，直接导致双向绿灯的冲突。

4. 并行进程的竞态问题 #

两个交通灯进程是并行执行的，初始状态下两个灯都是红灯，它们会同时进入Ered分支。由于没有等待逻辑，两个进程会同时将自己的灯设为绿灯，这就出现了双向绿灯的严重安全问题。

验证报错的原因分析 #

你使用的LTL公式是：

<>(!TL0@Ered && !TL1@Ered)

这个公式的意思是：最终会存在一个状态，TL0和TL1都不在Ered标签的位置。

spin报错“assertion violated”的原因在于：

1. 初始状态下，两个进程都停在Ered标签处，此时!TL0@Ered && !TL1@Ered为假
2. 由于代码逻辑错误，spin的部分序约减（Partial Order Reduction）导致搜索没有完成，无法找到满足公式的状态
3. 更关键的是，当前代码中即使进程离开Ered，也会很快循环回来，加上竞态问题，spin无法确认是否能稳定到达满足公式的状态

修正后的代码示例 #

我帮你修正了代码，加入传感器逻辑、正确的等待机制，修复竞态问题：

mtype = { red, yellow, green };
mtype light0 = red;
mtype light1 = red;
// 传感器变量：true表示有车辆触发
bool sensor0 = false;
bool sensor1 = false;

// 模拟车辆触发传感器的进程（可选，用于测试）
active proctype VehicleGenerator() {
    do
    :: timeout -> sensor0 = true;
    :: timeout -> sensor1 = true;
    :: timeout -> sensor0 = false;
    :: timeout -> sensor1 = false;
    od
}

active proctype TL0() {
    do
    :: if
        // 只有传感器触发且当前灯为红灯时，才尝试转绿
        :: light0 == red && sensor0 -> 
            Ered: 
                // 等待另一方向为红灯，原子操作确保条件检查和灯色变更的原子性
                atomic {
                    await light1 == red;
                    light0 = green;
                }
        :: light0 == green -> 
            EY: light0 = yellow;
            // 黄灯持续一段时间（用timeout模拟）
            timeout;
        :: light0 == yellow -> 
            EG: light0 = red;
            // 红灯时重置传感器（可选，避免重复触发）
            sensor0 = false;
    fi;
    printf("The light0 is now %e\n", light0)
    od
}

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

修正后的验证 #

使用同样的命令重新验证：

spin -a -f '<>(!TL0@Ered && !TL1@Ered)' sem3.pml
gcc -o pan pan.c
./pan

此时spin应该能找到满足公式的状态，不会再出现初始状态的断言违反错误。

内容的提问来源于stack exchange，提问作者Urkidy