スピンとプロメラの構文を使用したLTLモデルのチェック

Question

私はDijkstraによって書かれたALGOL 60コードを「Cooperating sequential processes」という論文に再現しようとしています。このコードはmutexの問題を解決するための最初の試みです。

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は無限に動作しています。

ここでの問題は、私がここ

が

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? 

IsPinを

から実際の出力です..私は単純に取得出力は私の文は達していなかったことを言って、ブロックがエラーを生成されていないと主張しないことです

私はnever{..}ブロックのスピンに関するすべてのドキュメントを読んだが、私の答え（ここではlink）を見つけることができなかった。また、ltl{..}ブロックも使用しようとしたが（link）その文書で明示的に言及されているが、 initとproctypesの外にいる場合は、このコードを修正してください。

あなたは

Answer 1

あなたはおそらく良いことができない「真の」再定義しましたありがとうございました。私はその再定義と絶対的な主張が失敗したと主張した。しかし、失敗はあなたの目標にとって重要ではありません。つまり、「状態」の初期状態は「偽」であり、したがって、失敗であることはありません。

また、boolに1または0を割り当てるのはやや難しい形式です。代わりに真または偽を割り当てるか、ビットを使用します。なぜDijkstraコードに従わないと、「int」か「byte」を使用してください。これはパフォーマンスがこの問題の問題になるかのようではありません。

'実行'を呼び出す場合は、どちらか一方のみをアクティブにする必要はありません。 「プロセス1」の

私の翻訳は次のようになります。

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

が、私はその上で間違っている可能性があります。