プログラミングなどなど

プログラミングに関係しそうな内容を

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関数から戻り、結果の出力処理へと進みました。