在 proctype“-end-”中未达到旋转

Question

我对旋转模型检查很陌生，想知道这个错误意味着什么：

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
}

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

Answer 1

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

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
}

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

---

本文档是相关的。

• 接受标签
• 结束标签
• 进度标签

end标签本身可能无法解决此问题。如果碰巧你有一个 accept 标签前缀，你仍然可以获得神秘的验证消息。例如，面向连接的协议可能会天真地使用“accept”标签。这些标签对于旋转验证模式是特殊的（其他功能如trace、

never

等）。在某些方面，这有点不幸，因为

goto label;

是模型或模拟属性。标签

end

、progress和accept对于模拟/建模和模型验证具有双重目的。 因此，如果您是旋转新手，请注意“标签”不应使用这些前缀（当然，除非您知道并理解验证含义）。对于面向连接的界面，应使用

open

、active 和 close（或其他替代方案）等标签，而不是 open、accept 和 end。

Answer 2

end

标签来明确是一种很好的形式。但是，并不总是可以做到这一点，因此您可以通过使用

pan

标志运行

-n

验证来安静 SPIN：-n : no listing of unreached states at the end of the run