PromelaのSPINがproctypeのエラーに達していません

Question

私はSPINとPromelaには新しく、私のモデルではライブネスのプロパティを検証しようとしています。

エラーコード：

unreached in proctype P 
     (0 of 29 states) 
unreached in proctype monitor 
     mutex_assert.pml:39, state 1, "assert(!((mutex>1)))" 
     mutex_assert.pml:42, state 2, "-end-" 
     (2 of 2 states) 
unreached in init 
     (0 of 3 states) 
unreached in claim ltl_0 
     _spin_nvr.tmp:10, state 13, "-end-" 
     (1 of 13 states) 

pan: elapsed time 0 seconds 

コードは、基本的にはピーターソンのアルゴリズムの実装であると私は、安全性をチェックし、有効であると思われます。しかし、ltl {[]（（wait - > <>（cs）））}}を使用してライブネスプロパティを検証しようとすると、上記のエラーが発生します。私は、彼らが何を意味するかわからないので、私は続行する方法がわからない...

次のように私のコードは次のとおりです。

#define N 3 
#define wait (P[1]@WAIT) 
#define cs  (P[1]@CRITICAL) 

int pos[N]; 
int step[N]; 
int enter; 
byte mutex; 
ltl {[]((wait -> <> (cs)))} 

proctype P(int i) { 
    int t; 
    int k; 
    WAIT: 
    for (t : 1 .. (N-1)){ 
    pos[i] = t 
    step[t] = i 
    k = 0; 
    do 
    :: atomic {(k != i && k < N && (pos[k] < t|| step[t] != i)) -> k++} 
    :: atomic {k == i -> k++} 
    :: atomic {k == N -> break} 
    od; 
    } 

CRITICAL: 
    atomic {mutex++; 
    printf("MSC: P(%d) HAS ENTERED THE CRITICAL SECTION.\n", i); 
    mutex--;} 
    pos[i] = 0; 
} 

init { 
    atomic { run P(0); } 
} 

Answer 1

全般

これは警告です回答しますは、決して奪われない遷移のためにに到達できない状態があります。一般的に

、これはないエラーですが、のためにあなたがをモデル化し、すべてのルーチンを到達不能状態に近い見てみると、あなたがのどれを期待していないことを確認するために良い習慣ですそれらに達することができます。 、すなわち、モデルが正しいwrtでない場合。意図された振る舞い。

注意。ラベルの末尾には、特定のコード行の前にを使用して、有効な終了状態をマークすることができます。これらの警告を取り除くには、などがあります。プロシージャが終了しないとき。詳細情報here。

---

具体的な回答

私はあなたの出力を再現することはできません。特に、

~$ spin -a file.pml 
~$ gcc pan.c 
~$ ./a.out -a 

を実行して、私はあなたのものと異なっている次の出力、取得：特に

(Spin Version 6.4.3 -- 16 December 2014) 
    + Partial Order Reduction 

Full statespace search for: 
    never claim    + (ltl_0) 
    assertion violations + (if within scope of claim) 
    acceptance cycles  + (fairness disabled) 
    invalid end states - (disabled by never claim) 

State-vector 64 byte, depth reached 47, errors: 0 
     41 states, stored (58 visited) 
     18 states, matched 
     76 transitions (= visited+matched) 
     0 atomic steps 
hash conflicts:   0 (resolved) 

Stats on memory usage (in Megabytes): 
    0.004 equivalent memory usage for states (stored*(State-vector + overhead)) 
    0.288 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 P 
    (0 of 29 states) 
unreached in init 
    (0 of 3 states) 
unreached in claim ltl_0 
    _spin_nvr.tmp:10, state 13, "-end-" 
    (1 of 13 states) 

pan: elapsed time 0 seconds 

を、私はモニター過程における未到達の状態に関する警告を欠いています。私が関心を持つ限り、ソースコードから始まって、私が得た警告は問題ではありません。

スピンの私とは異なるバージョンを使用しているか、質問に完全なソースコードを含めていません。後者の場合、質問を編集してコードを追加できますか？私はその後、私の答えを更新します。

---

EDITは：「請求ltl_0の_spin_nvrで未到達：コメントで、次のメッセージがどういう意味尋ねます。TMP：10、状態13、「 - 終わり - 」」

ファイル_spin_nvr.tmpを開くと、ビュッヒオートマトンに対応Promelaモデル次のコードを、見ることができますそれはあなたのLTLプロパティに違反しているすべてと実行のみを受け付け[]（（待つ - > <>（CS）））

メッセージは単純に、このコードの実行が到達することはありませんことを警告

never ltl_0 { /* !([] ((! ((P[1]@WAIT))) || (<> ((P[1]@CRITICAL))))) */ 
T0_init: 
    do 
    :: (! ((! ((P[1]@WAIT)))) && ! (((P[1]@CRITICAL)))) -> goto accept_S4 
    :: (1) -> goto T0_init 
    od; 
accept_S4: 
    do 
    :: (! (((P[1]@CRITICAL)))) -> goto accept_S4 
    od; 
} 

。最後の閉じ括弧}（状態"-end-"）は、プロシージャが決して終了しないことを意味します。