スピンで複数の（またはすべての）違反トレースを求める

Question

スピンを使用してプロパティに対して複数の（またはすべての）違反トレースを取得することは可能ですか？

例として、私は以下のPromelaモデルモデルを作成：

byte mutex = 0; 

active proctype A() { 
A1: mutex==0; /* Is free? */ 
A2: mutex++; /* Get mutex */ 
A3: /* A's critical section */ 
A4: mutex--; /* Release mutex */ 
} 

active proctype B() { 
B1: mutex==0; /* Is free? */ 
B2: mutex++; /* Get mutex */ 
B3: /* B's critical section */ 
B4: mutex--; /* Release mutex */ 
} 

ltl {[] (mutex < 2)} 

をそれはナイーブミューテックスの実装を持っています。プロセスAとプロセスBがクリティカルセクションに一緒に到達しないことを期待して、それを確認するためのLTL式を書きました。

spin -run mutex_example.pml 

を実行

は、プロパティが有効と

spin -p -t mutex_example.pml 

を実行していないことを示している財産を侵害する一連の文を示しています。

Never claim moves to line 4  [(1)] 
    2: proc 1 (B:1) mutex_example.pml:11 (state 1) [((mutex==0))] 
    4: proc 0 (A:1) mutex_example.pml:4 (state 1)  [((mutex==0))] 
    6: proc 1 (B:1) mutex_example.pml:12 (state 2) [mutex = (mutex+1)] 
    8: proc 0 (A:1) mutex_example.pml:5 (state 2)  [mutex = (mutex+1)] 
spin: _spin_nvr.tmp:3, Error: assertion violated 
spin: text of failed assertion: assert(!(!((mutex<2)))) 
Never claim moves to line 3  [assert(!(!((mutex<2))))] 
spin: trail ends after 9 steps 
#processes: 2 
       mutex = 2 
    9: proc 1 (B:1) mutex_example.pml:14 (state 3) 
    9: proc 0 (A:1) mutex_example.pml:7 (state 3) 
    9: proc - (ltl_0:1) _spin_nvr.tmp:2 (state 6) 

これは（ラベルで示されている）一連の文「B1」ことを示している - >「A1」 - >「B2」 - >「A2」のプロパティに違反するが、それにつながる他のインターリービングのオプションが（あります例えば ​​'A1'→ 'B1'→ 'B2'→ 'A2'）。

私に複数の（またはすべての）トレースを与えるようにスピンに質問することはできますか？

Answer 1

すべて違反トレースがスピンにあるとは思っていません。例えば

我々は次のモデルを考慮すれば、その後、無限に多くの反例があります。あなたは何ができるか

byte mutex = 0; 

active [2] proctype P() { 
    do 
     :: mutex == 0 -> 
      mutex++; 
      /* critical section */ 
      mutex--; 
    od 
} 

ltl {[] (mutex <= 1)} 

---

、あなたの検証ため異なる検索アルゴリズムを使用することであり、このは私の例では、いくつかの異なる反例に

-search (or -run) generate a verifier, and compile and run it 
     options before -search are interpreted by spin to parse the input 
     options following a -search are used to compile and run the verifier pan 
     valid options that can follow a -search argument include: 
     -bfs perform a breadth-first search 
     -bfspar perform a parallel breadth-first search 
     -bcs use the bounded-context-switching algorithm 
     -bitstate or -bit, use bitstate storage 
     -biterate use bitstate with iterative search refinement (-w18..-w35) 
     -swarmN,M like -biterate, but running all iterations in parallel 
      perform N parallel runs and increment -w every M runs 
      default value for N is 10, default for M is 1 
     -link file.c link executable pan to file.c 
     -collapse use collapse state compression 
     -hc  use hash-compact storage 
     -noclaim ignore all ltl and never claims 
     -p_permute use process scheduling order permutation 
     -p_rotateN use process scheduling order rotation by N 
     -p_reverse use process scheduling order reversal 
     -ltl p verify the ltl property named p 
     -safety compile for safety properties only 
     -i   use the dfs iterative shortening algorithm 
     -a   search for acceptance cycles 
     -l   search for non-progress cycles 
    similarly, a -D... parameter can be specified to modify the compilation 
    and any valid runtime pan argument can be specified for the verification