SPIN:LTLの記述によっては意図した検査にならない?
前回モデル(SPIN:モデル(安全性(排他)と応答性) - プログラミングなどなど)でLTLで検証式を記述する際に実は、トライ&エラーを行っていました。その際、記述したLTLで想定していた検査が行われていないようなケースがありました。
そもそも、記述したLTLが誤っているかもしれないので、慣れている人やよく理解している人には無縁かもしれませんが、私は最初気がつかなかったので、メモとして残したいと思います。
モデル(model.pml)(前回と同じもの)
/* OPE-SV間のメッセージ定義 */ mtype = { START_SND_SRV, /* 第2サービス開始 */ STOP_SND_SRV /* 第2サービス停止 */ } /* SVとの通信用チャネル */ chan svCh = [2] of { mtype } /* 運用者による操作を受付てSVに操作に対応するメッセージを送信するプロセス */ active proctype OPE() { bool sndSrvOrd = false; /* 運用者による第2サービス開始操作 */ atomic { sndSrvOrd = true; svCh ! START_SND_SRV; } /* 時間経過などもろもろ */ /* 運用者による第2サービス停止操作 */ atomic { sndSrvOrd = false; svCh ! STOP_SND_SRV; } } /* 実際のサービスを制御するサーバプロセス */ active proctype SV() { /* デフォルトでは第1サービスが有効になっているものとする。*/ /* 運用者から第2サービスの開始操作が行われた場合に、 第2サービスを開始する。*/ /* 第1サービスと第2サービスは排他関係になっており、両者が共に有効になってはならない。*/ bool isFstSrvOn = true; bool isSndSrvOn = false; mtype event; do :: svCh ? event -> if :: atomic { event == START_SND_SRV -> isFstSrvOn = false; isSndSrvOn = true; } :: atomic { event == STOP_SND_SRV -> isFstSrvOn = true; isSndSrvOn = false; } fi od }
前回の検証式
前回は、運用者からの第2サービスの開始にともなって第2サービスが有効になること。また、停止に伴って第2サービスが停止することを、応答性として以下の様に記述しました。
応答性(第2サービス開始)
/* 運用者による第2サービスの開始操作が行われたら、第2サービスが有効になる。*/ ltl liveSndStart { [](OPE:sndSrvOrd == true -> <>(SV:isFstSrvOn == false && SV:isSndSrvOn == true)) }
応答性2(第2サービス停止)
/* 運用者による第2サービスの停止操作が行われたら、第1サービスが有効になる。*/ ltl liveSndStop { [](OPE:sndSrvOrd == false -> <>(SV:isFstSrvOn == true && SV:isSndSrvOn == false)) }
検証式(誤り?)
上記の形になる試行錯誤の前は以下の様に記述していました。
注目して頂きたいのは前提条件(OPE:sndSrvOrd == true, OPE:sndSrvOrd == false)の部分となります。
例1
/* 運用者による第2サービスの開始操作が行われたら、第2サービスが有効になる。*/ ltl liveSndStart2 { OPE:sndSrvOrd == true -> <>[](SV:isSndSrvOn == true) } ltl nliveSndStart2 { !(OPE:sndSrvOrd == true -> <>[](SV:isSndSrvOn == true)) }
例2
/* 運用者による第2サービスの停止操作が行われたら、第1サービスが有効になる。*/ ltl liveSndStop2 { OPE:sndSrvOrd == false -> <>[](SV:isFstSrvOn == true) } ltl nliveSndStop2 { !(OPE:sndSrvOrd == false -> <>[](SV:isFstSrvOn == true)) }
検証の実行
例1
例1の検証を実行してみると、確かにエラーが0件であることは想定どおりなのですが、「1 states, stored」となっていたり、「unreached」に実行を想定している行が出力されていたりと怪しい感じが出ています。
$ spin -run -ltl liveSndStart2 model.pml pan: ltl formula liveSndStart2 (Spin Version 6.5.0 -- 17 July 2019) + Partial Order Reduction Full statespace search for: never claim + (liveSndStart2) assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 52 byte, depth reached 0, errors: 0 1 states, stored 0 states, matched 1 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.261 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 OPE model.pml:16, state 2, "svCh!START_SND_SRV" model.pml:21, state 5, "svCh!STOP_SND_SRV" model.pml:21, state 6, "sndSrvOrd = 0" model.pml:22, state 7, "-end-" (4 of 7 states) unreached in proctype SV model.pml:37, state 3, "isFstSrvOn = 0" model.pml:37, state 4, "isSndSrvOn = 1" model.pml:38, state 7, "isFstSrvOn = 1" model.pml:38, state 8, "isSndSrvOn = 0" model.pml:37, state 10, "((event==START_SND_SRV))" model.pml:37, state 10, "((event==STOP_SND_SRV))" model.pml:41, state 15, "-end-" (6 of 15 states) unreached in claim liveSndStart2 _spin_nvr.tmp:101, state 10, "(1)" _spin_nvr.tmp:105, state 17, "(!((SV.isSndSrvOn==1)))" _spin_nvr.tmp:105, state 17, "(1)" _spin_nvr.tmp:108, state 20, "-end-" (3 of 20 states) pan: elapsed time 0 seconds
例2
因みに例2を実行した場合は、ちゃんと探索してくれていそうな感じがあります。
$ spin -run -ltl liveSndStop2 model.pml pan: ltl formula liveSndStop2 (Spin Version 6.5.0 -- 17 July 2019) + Partial Order Reduction Full statespace search for: never claim + (liveSndStop2) assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 52 byte, depth reached 20, errors: 0 12 states, stored (17 visited) 9 states, matched 26 transitions (= visited+matched) 20 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.001 equivalent memory usage for states (stored*(State-vector + overhead)) 0.261 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 OPE (0 of 7 states) unreached in proctype SV model.pml:41, state 15, "-end-" (1 of 15 states) unreached in claim liveSndStop2 _spin_nvr.tmp:143, state 20, "-end-" (1 of 20 states) pan: elapsed time 0 seconds
デバッグ
例1で探索が行われていないのかを部分を見たいと考えデバッグしてみることにしました。検証器のコンパイルまでに行った手順は以下となります。
検証器コードの整形とデバッグオプション付きでのコンパイル
$ spin -a model.pml ltl safe: [] (! (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==1)))) : ltl nliveSndStart3: ! ([] (<> ((! ((OPE:sndSrvOrd==1))) || (<> ([] ((SV:isSndSrvOn==1))))))) the model contains 13 never claims: nliveSndStart3, liveSndStart3, nliveSndStop2, liveSndStop2, nliveSndStart2, liveSndStart2, nliveSndStop, liveSndStop, nliveSndStart, liveSndStart, notStop, nsafe, safe only one claim is used in a verification run choose which one with ./pan -a -N name (defaults to -N safe) or use e.g.: spin -search -ltl safe model.pml $ gcc -E -C -P -DNOREDUCE pan.c > ppan.c $ indent ppan.c -o pppan.c $ gcc -g3 -O0 pppan.c
GDBによるデバッグ
do_transit関数にブレークポイントを設定しステップ実行していくと、確かにすぐに検証を完了したルートに入っていそうでした。
$ gdb --args ./a.out -a -N liveSndStart2 (gdb) break do_transit Breakpoint 1 at 0x6d09: file pppan.c, line 9653. (gdb) r Starting program: /home/makoto/blog/ltlNG/a.out -a -N liveSndStart2 pan: ltl formula liveSndStart2 Breakpoint 1, do_transit (t=0x19010, II=32767) at pppan.c:9653 9653 { (gdb) backtrace #0 do_transit (t=0x19010, II=32767) at pppan.c:9653 #1 0x0000555555561645 in new_state () at pppan.c:11685 #2 0x000055555555acf2 in do_the_search () at pppan.c:9648 #3 0x00005555555587e0 in run () at pppan.c:8945 #4 0x000055555556485d in main (argc=1, argv=0x7fffffffdd80) at pppan.c:13316
上記設定後に処理を再開させてステップ実行させていくと、他状態への遷移がなく、すぐにrun関数から戻り、結果の出力処理へと進みました。