为何SPIN在此场景下无法检测非进展循环？

初始代码与检测结果 #

原始Promela代码如下：

byte x=2;
active proctype A() {
  do  
  :: x = 3-x
  od  
}
active proctype B() {
  do  
  :: x = 3-x 
  od                                                                                                                          
}

经gcc -DNP -o my pan.c编译后，执行./my -l，SPIN可检测到非进展循环。

第一次修改后的检测结果 #

将进程A修改为：

active proctype A() {
  do  
  :: x = 3-x; progress: skip
  od  
}

• 执行./my -l -f（-f表示CPU时间片公平分配）时，非进展循环消失；
• 执行./my -l时，仍可检测到该循环。

第二次修改后的检测结果 #

仅将进程A修改为：

active proctype A() {
progress:
  do  
  :: x = 3-x
  od  
}

此时./my -l与./my -l -f两种模式均无法检测到非进展循环。

用户猜测 #

• 猜测1：SPIN存在bug
• 猜测2：两个进程共用同一FSM（及状态），而修改后将该共用FSM的整个状态标记为始终处于进展中

FSM图佐证 #

通过./my -D生成的FSM图显示仅存在一个状态S2：

digraph p_A {
size="8,10";
  GT [shape=box,style=dotted,label="A"];
  GT -> S2;
        S2 -> S2  [color=black,style=bold,label="x = (3-x)"];
  S2 [color=green,style=bold];
digraph p_B {
size="8,10";
  GT [shape=box,style=dotted,label="B"];
  GT -> S2;
        S2 -> S2  [color=black,style=bold,label="x = (3-x)"];

原因解析 #

你的第二个猜测是正确的，并非SPIN的bug。

SPIN中progress:标签的作用是标记进程当前所处的状态属于进展状态——只要进程处于带有该标签的状态，就会被判定为正在推进系统的进展，不会被计入非进展循环的判定逻辑。

在第二次修改中，你将progress:标签放在了do循环的外部，意味着进程A从启动后就直接进入了带有progress:标记的状态，并且整个循环过程中始终处于这个状态。结合FSM图可以看到，两个进程的状态机完全重合（共用同一状态S2），SPIN的状态合并机制会将结构完全一致的进程状态机合并为同一个。这就导致只要其中一个进程的状态被标记为progress，整个共用状态就会被判定为进展状态。

当系统处于这个状态时，无论调度哪个进程执行，都会被认为是在推进进展，自然不会检测到非进展循环——因为非进展循环的判定条件是：存在一个循环路径，其中所有进程都没有产生任何进展（即都不在progress标记的状态，且没有执行任何能推进系统的动作）。

而第一次修改中，progress:标签放在了循环体的动作之后，只有当进程A执行完x=3-x后才会进入进展状态。在非公平调度模式下（./my -l），SPIN可能会一直调度进程B执行，此时进程A始终处于未到达progress:标记的状态，进程B也没有任何progress标记，因此系统会被判定为陷入非进展循环；而公平调度模式（-f）会保证每个进程都有机会执行，进程A能周期性进入progress状态，打破非进展循环的判定条件。

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