在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

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

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

Answer 2

旋转通知您,您的proctypes永远不会达到"结束"状态,这当然是真实的,因为它们由无限循环组成.如果这不是预期的行为,那将是一个有用的信息.在你的情况,但是,你可能只是告诉旋转该程序允许通过添加对应的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
}

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