SPIN:-searchオプションを指定した場合の動きについて
PROMELAで記述したモデルから検証器を生成する際にnever claimが2つ以上になると、どれか一つを選択して欲しい旨と-searchオプションを指定する例が出力されます。
本などには以下の流れで記載されていますが、何か違いがあったりするのでしょうか。
- 検証器の生成
- 検証器のコンパイル
- 検証器の実行
straceコマンドを利用して見てみたいと思います。
サンプルソース : sample.pml
byte b = 0; active proctype p() { if :: b = 1; :: b = 2; fi } ltl l01 { <>(b == 1) }
検証器の生成
$ spin -a sample.pml ltl l01: <> ((b==1))
コンパイルと実行
$ gcc -w pan.c -o pan
$ ./pan -a
pan:1: acceptance cycle (at depth 4)
pan: wrote sample.pml.trail
(Spin Version 6.4.9 -- 17 December 2018)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (l01)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 28 byte, depth reached 5, errors: 1
4 states, stored
0 states, matched
4 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 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
ltlの追加
サンプルソース(ltl追加) : sample.pml
以下のようにltlを追加します。
byte b = 0; active proctype p() { if :: b = 1; :: b = 2; fi } ltl l01 { <>(b == 1) } ltl l01n { !(<>(b == 1)) }
検証器の生成(ltl追加後)
検証器を生成しようとすると1つの場合とは異なりオプションの説明が出力されます。
$ spin -a sample.pml ltl l01: <> ((b==1)) ltl l01n: ! (<> ((b==1))) the model contains 2 never claims: l01n, l01 only one claim is used in a verification run choose which one with ./pan -a -N name (defaults to -N l01) or use e.g.: spin -search -ltl l01 sample.pml
検証器の生成からコンパイル、実行
例に習って-searchオプションを指定してみます。
$ spin -search -ltl l01 sample.pml
ltl l01: <> ((b==1))
ltl l01n: ! (<> ((b==1)))
the model contains 2 never claims: l01n, l01
only one claim is used in a verification run
choose which one with ./pan -a -N name (defaults to -N l01)
or use e.g.: spin -search -ltl l01 sample.pml
pan: ltl formula l01
pan:1: acceptance cycle (at depth 4)
pan: wrote sample.pml.trail
(Spin Version 6.4.9 -- 17 December 2018)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (l01)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 20 byte, depth reached 5, errors: 1
4 states, stored
0 states, matched
4 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.290 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
-searchオプションを指定した際の動作を追う
-searchオプションを使用した場合のspinコマンドの動作をstraceコマンドを使用して追ってみます。
straceによるシステムコールのトレース取得
$ strace -o sout -f spin -search -ltl l01 sample.pml
トレース確認
以下はトレースの抜粋です。
コンパイル時のオプションが手動で実行した場合と異なりますが、生成、コンパイル、実行を順に行ってくれていることがわかります。
$ less sout
5255 execve("/home/makoto/bin/spin", ["spin", "-search", "-ltl", "l01", "sample.pml"], 0x7ffeb6c98828 /* 67 vars */) = 0
:
5255 openat(AT_FDCWD, "pan.c", O_WRONLY|O_CREAT|O_TRUNC, 0666) = 3 <-- pan.cの生成部分
:
fd=3についてwriteが呼び出されている。
:
5255 close(3) = 0
:
5260 execve("/usr/bin/gcc", ["gcc", "-std=gnu99", "-O", "-DNOFAIR", "-o", "pan", "pan.c"], 0x5573ac3132d8 /* 67 vars */) = 0 <-- コンパイル部分
;
5265 execve("/bin/sh", ["sh", "-c", "./pan -N l01 -a"], 0x7ffed5d7edc8 /* 67 vars */) = 0 <-- 実行部分
