SPIN:状態探索(1プロセス,分岐あり)とグラフ化
SPINの検証器が状態空間をどのように探索しているのかが気になったので、状態ベクトルを出力させながら追ってみました。
使用したソースは以下となります。
使用したソースから検証器の実行まで
分岐を2箇所に用意した計4経路を通るような以下のソースを用意しました。
ソース branch.pml
byte a = 0; active proctype p() { if :: a = 170; /* 0xaa = -86 */ :: a = 187; /* 0xbb = -69 */ fi if :: a = 204; /* 0xcc = -52 */ :: a = 221; /* 0xdd = -35 */ fi }
検証器の生成
$ spin -a -o2 2p.pml
検証器のコンパイル
$ gcc -w -g3 -DVERBOSE -DSDUMP -DNOCOMP pan.c -o pan
実行結果
$ ./pan
0: Down - program non-accepting [pids 0-0]
New state 0
State: 1,0,0,0,0,0,20,0,0,0,0,0,0,0,0,0,0,12,0,0,
Vector: 1,0,0,0,0,0,20,0,0,0,0,0,0,0,0,0,0,12,0,0,
Pr: 0 Tr: 3
0: proc 0 exec 3, 3 to 7, a = 170 non-accepting [tau=0]
1: Down - program non-accepting [pids 0-0]
New state 1
State: 1,0,0,0,0,0,20,0,-86,0,0,0,0,0,0,0,0,28,0,0,
Vector: 1,0,0,0,0,0,20,0,-86,0,0,0,0,0,0,0,0,28,0,0,
Pr: 0 Tr: 5
1: proc 0 exec 5, 7 to 9, a = 204 non-accepting [tau=0]
2: Down - program non-accepting [pids 0-0]
New state 2
State: 1,0,0,0,0,0,20,0,-52,0,0,0,0,0,0,0,0,36,0,0,
Vector: 1,0,0,0,0,0,20,0,-52,0,0,0,0,0,0,0,0,36,0,0,
Pr: 0 Tr: 7
2: proc 0 exec 7, 9 to 0, -end- non-accepting [tau=0]
3: Down - program non-accepting [pids -1-0]
New state 3
State: 0,0,0,0,0,0,10,0,-52,0,
Vector: 0,0,0,0,0,0,10,0,-52,0,
3: no move [II=-1, tau=0, boq=-1]
3: Up - program
3: proc 0 reverses 7, 9 to 0
-end- [abit=0,adepth=0,tau=0,0]
2: Up - program
2: proc 0 reverses 5, 7 to 9
a = 204 [abit=0,adepth=0,tau=0,0]
Pr: 0 Tr: 6
1: proc 0 exec 6, 7 to 9, a = 221 non-accepting [tau=0]
2: Down - program non-accepting [pids 0-0]
New state 4
State: 1,0,0,0,0,0,20,0,-35,0,0,0,0,0,0,0,0,36,0,0,
Vector: 1,0,0,0,0,0,20,0,-35,0,0,0,0,0,0,0,0,36,0,0,
Pr: 0 Tr: 7
2: proc 0 exec 7, 9 to 0, -end- non-accepting [tau=0]
3: Down - program non-accepting [pids -1-0]
New state 5
State: 0,0,0,0,0,0,10,0,-35,0,
Vector: 0,0,0,0,0,0,10,0,-35,0,
3: no move [II=-1, tau=0, boq=-1]
3: Up - program
3: proc 0 reverses 7, 9 to 0
-end- [abit=0,adepth=0,tau=0,0]
2: Up - program
2: proc 0 reverses 6, 7 to 9
a = 221 [abit=0,adepth=0,tau=0,0]
1: Up - program
1: proc 0 reverses 3, 3 to 7
a = 170 [abit=0,adepth=0,tau=0,0]
Pr: 0 Tr: 4
0: proc 0 exec 4, 3 to 7, a = 187 non-accepting [tau=0]
1: Down - program non-accepting [pids 0-0]
New state 6
State: 1,0,0,0,0,0,20,0,-69,0,0,0,0,0,0,0,0,28,0,0,
Vector: 1,0,0,0,0,0,20,0,-69,0,0,0,0,0,0,0,0,28,0,0,
Pr: 0 Tr: 5
1: proc 0 exec 5, 7 to 9, a = 204 non-accepting [tau=0]
2: Down - program non-accepting [pids 0-0]
Old state 2
State: 1,0,0,0,0,0,20,0,-52,0,0,0,0,0,0,0,0,36,0,0,
Vector: 1,0,0,0,0,0,20,0,-52,0,0,0,0,0,0,0,0,36,0,0,
2: Up - program
2: proc 0 reverses 5, 7 to 9
a = 204 [abit=0,adepth=0,tau=0,0]
Pr: 0 Tr: 6
1: proc 0 exec 6, 7 to 9, a = 221 non-accepting [tau=0]
2: Down - program non-accepting [pids 0-0]
Old state 4
State: 1,0,0,0,0,0,20,0,-35,0,0,0,0,0,0,0,0,36,0,0,
Vector: 1,0,0,0,0,0,20,0,-35,0,0,0,0,0,0,0,0,36,0,0,
2: Up - program
2: proc 0 reverses 6, 7 to 9
a = 221 [abit=0,adepth=0,tau=0,0]
1: Up - program
1: proc 0 reverses 4, 3 to 7
a = 187 [abit=0,adepth=0,tau=0,0]
(Spin Version 6.4.9 -- 17 December 2018)
+ Partial Order Reduction
+ FullStack Matching
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 20 byte, depth reached 3, errors: 0
7 states, stored
2 states, matched
0 matches within stack
9 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
stackframes: 1/0
stats: fa 0, fh 0, zh 0, zn 0 - check 0 holds 0
stack stats: puts 0, probes 0, zaps 0
128.730 memory usage (Mbyte)
unreached in proctype p
(0 of 9 states)
pan: elapsed time 0 seconds
結果のグラフ化
上記の結果を見ると深さ優先探索で以下の流れて探索しています。
- 1経路目 : s1からs3まで探索して終了状態まで進み、s1まで戻っています。
- 2経路目 : s1からs5のまで探索し、s0まで戻っています。
- 3経路目 : s1からs6まで進み、遷移先s2が探索済みだったのでs6に戻っています。
- 4経路目 : s6からs4と進みますが、こちらも探索済みだったので、s0まで戻って探索終了となっています。
グラフ化したものが以下になります。
円形は状態で「State X」に対応するものを「sX」で、各状態でのaの値とプロセスの状態p(1:実行中,0:終了)を「a,p」で記載しています。四角は遷移で「Pr: A Tr: B」に対応するものを「trA,B」で記載しています。
