9

私はスピンモデルのチェックにかなり慣れていないので、このエラーの意味を知りたいと思っていました:

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
}

実際に終了する必要はありません。これは、2 つのプロセスが一緒にクリティカル セクションにないかどうかをチェックする相互排除プログラムです。エラーはプログラムが終了しないことを意味しますか? ありがとう！

4

2 に答える 2

6

チェックされた答えは良いものです。endラベルを適切に追加して明示するのは良い形式です。ただし、それが常に可能であるとは限らないため、フラグを使用してpan検証を実行することで SPIN を停止できます。-n

-n : no listing of unreached states at the end of the run
于 2014-04-09T14:36:53.630 に答える