proctype“-end-”中的旋转未达到答案

【问题标题】：Spin unreached in proctype "-end-"proctype“-end-”中的旋转未达到
【发布时间】：2014-05-10 15:38:58
【问题描述】：

我是自旋模型检查的新手，想知道这个错误是什么意思：

unreached in proctype P1
    ex2.pml:16, state 11, "-end-"
    (1 of 11 states)
unreached in proctype P2
    ex2.pml:29, state 11, "-end-"
    (1 of 11 states)

这是我的代码：

int y1, y2;
byte insideCritical;

active proctype P1(){
do
    ::true->
        y2 = y1 + 1;
        (y1 == 0 || y2 < y1);
        /* Entering critical section */
            insideCritical++;
            assert(insideCritical < 2);
            insideCritical--;
        /* Exiting critical section */
        y2 = 0;
od
}
active proctype P2(){
do
    ::true->
        y1 = y2 + 1;
        (y2 == 0 || y1 < y2);
        /* Entering critical section */
            insideCritical++;
            assert(insideCritical < 2);
            insideCritical--;
        /* Exiting critical section */
        y1 = 0;
od
}

它实际上不必结束，它是一个互斥程序，用于检查两个进程是否一起不在临界区。错误是否意味着程序没有结束？谢谢！

【问题讨论】：

标签： process mutual-exclusion spin promela

【解决方案1】：

Spin 告诉您，您的 proctype 永远不会达到“结束”状态，这当然是正确的，因为它们由无限循环组成。如果这不是预期的行为，那将是有用的信息。但是，在您的情况下，您可以通过在代码中添加 结束标签 来告诉 Spin，允许程序以与 do-loop 对应的状态结束，例如：

active proctype P1(){
  endHere:
  do
  :: true->
    y2 = y1 + 1;
    (y1 == 0 || y2 < y1);
    /* Entering critical section */
        insideCritical++;
        assert(insideCritical < 2);
        insideCritical--;
    /* Exiting critical section */
    y2 = 0;
  od
}

结束标签是任何以“结束”开头的标签。如果您的 proctype 以这种方式标记的状态结束，Spin 将不会向您显示这些警告。

【讨论】：

太棒了！和我想的一样。。谢谢！

【解决方案2】：

检查的答案是好的；通过适当地添加end 标签来明确是一种很好的形式。但是，并非总是可以这样做，因此您可以通过使用 -n 标志运行 pan 验证来使 SPIN 静音：

-n : no listing of unreached states at the end of the run

【讨论】：