model-checking - 使用 Spin 和 Promela 语法检查 LTL 模型

Question

我正在尝试重现 Dijkstra 在题为“合作顺序进程”的论文中编写的 ALGOL 60 代码，该代码是解决互斥问题的第一次尝试，这里是语法:

begin integer turn; turn:= 1;
      parbegin
      process 1: begin Ll: if turn = 2 then goto Ll;
                           critical section 1;
                           turn:= 2;
                           remainder of cycle 1; goto L1
                 end;
      process 2: begin L2: if turn = 1 then goto L2;
                           critical section 2;
                           turn:= 1;
                           remainder of cycle 2; goto L2
                  end
      parend
end 

所以我试图在 Promela 中重现上面的代码，这是我的代码:

#define true    1
#define Aturn true
#define Bturn false

bool turn, status;

active proctype A()
{   
    L1: (turn == 1); 
    status = Aturn;
    goto L1;
    /* critical section */
    turn = 1;

}

active proctype B()
{   
    L2: (turn == 2); 
    status = Bturn;
    goto L2;
    /* critical section */
    turn = 2;
}

never{ /* ![]p */ 
    if
    :: (!status) -> skip
    fi;
}

init
{   turn = 1;
    run A(); run B();
}

我想要做的是，验证公平属性永远不会成立，因为标签 L1 无限运行。

这里的问题是我的 never claim 块没有产生任何错误，我得到的输出只是说我的语句从未达到过..

这是 iSpin 的实际输出

spin -a  dekker.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -w -o pan pan.c
./pan -m10000 
Pid: 46025

(Spin Version 6.2.3 -- 24 October 2012)
    + Partial Order Reduction

Full statespace search for:
    never claim             - (not selected)
    assertion violations    +
    cycle checks        - (disabled by -DSAFETY)
    invalid end states  +

State-vector 44 byte, depth reached 8, errors: 0
       11 states, stored
        9 states, matched
       20 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001   equivalent memory usage for states (stored*(State-vector + overhead))
    0.291   actual memory usage for states
  128.000   memory used for hash table (-w24)
    0.534   memory used for DFS stack (-m10000)
  128.730   total actual memory usage


unreached in proctype A
    dekker.pml:13, state 4, "turn = 1"
    dekker.pml:15, state 5, "-end-"
    (2 of 5 states)
unreached in proctype B
    dekker.pml:20, state 2, "status = 0"
    dekker.pml:23, state 4, "turn = 2"
    dekker.pml:24, state 5, "-end-"
    (3 of 5 states)
unreached in claim never_0
    dekker.pml:30, state 5, "-end-"
    (1 of 5 states)
unreached in init
    (0 of 4 states)

pan: elapsed time 0 seconds
No errors found -- did you verify all claims?

我已经阅读了 never{..} 上的所有自旋文档。阻止但找不到我的答案(这里是 link )，我也试过使用 ltl{..}块( link )但这只是给了我语法错误，即使它在文档中明确提到它可以在 init 之外和 proctypes ，有人可以帮我更正这个代码吗？

谢谢

Answer 1

你已经重新定义了“真”，这不可能是好的。我取消了重新定义，并且从不声称失败。但是，失败对您的目标来说无关紧要——“状态”的初始状态是“假”，因此从不声明退出，这是一个失败。

此外，将 1 或 0 分配给 bool 的形式有点糟糕；改为分配 true 或 false - 或使用位。为什么不更密切地遵循 Dijkstra 代码 - 使用“int”或“byte”。在这个问题中，性能并不是一个问题。

如果您要调用 'run'，则不需要 'active' - 只需其中一个。

我对“过程 1”的翻译是:

proctype A ()
{
L1: turn !=2 ->
  /* critical section */
  status = Aturn;
  turn = 2
  /* remainder of cycle 1 */
  goto L1;
}

但我可能错了。