プログラミングなどなど

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

SPIN:LTLを使った2プロセスの実行順序確認

SPIN

SPINでは記述したモデルについてLTLで記述した性質の検証を行うことで反例がないかどうかをチェックしてくれます。私はまだ理解が浅いのでLTLで記述した検証が意図したものになっているかどうかについて自信がありません。そこで、記述した検証が、意図した検証になっていそうだということを確かめたいと思いました。

結論としては解をつかめていないのですが、大丈夫そうだと思える部分まで行くことができましたので、行った手順とメモを残します。

モデルとしては、2つのプロセスがそれぞれが管理する変数を更新するパターンが2通りあるということを検出したいと思います。

モデル

$ cat -n 2pro.pml
     1	bool isAProced = false;
     2	bool isBProced = false;
     3	
     4	active proctype A()
     5	{
     6	  isAProced = true;
     7	}
     8	
     9	active proctype B()
    10	{
    11	  isBProced = true;
    12	}

プロセスAとBがあり、並列に動作するモデルです。実行の制約は無いので、6行目:プロセスAのisAProced = trueが先に実行される場合と11行目:プロセスBのisBProced = trueが先に実行される場合があるはずです。

ランダムシミュレーション

ランダムシミュレーションを何度か行ってみると、確かに上記の2ケースが結果として出てきます。

プロセスAの処理が先に実行されるケース

$ spin -p 2pro.pml
  0:	proc  - (:root:) creates proc  0 (A)
  0:	proc  - (:root:) creates proc  1 (B)
  1:	proc  0 (A:1) 2pro.pml:6 (state 1)	[isAProced = 1]
  2:	proc  1 (B:1) 2pro.pml:11 (state 1)	[isBProced = 1]
  2:	proc  1 (B:1)           terminates
  2:	proc  0 (A:1)       terminates
2 processes created

プロセスBの処理が先に実行されるケース

$ spin -p 2pro.pml
  0:	proc  - (:root:) creates proc  0 (A)
  0:	proc  - (:root:) creates proc  1 (B)
  1:	proc  1 (B:1) 2pro.pml:11 (state 1)	[isBProced = 1]
  1:	proc  1 (B:1)           terminates
  2:	proc  0 (A:1) 2pro.pml:6 (state 1)	[isAProced = 1]
  2:	proc  0 (A:1)       terminates
2 processes created

LTLでの確認

上記のモデルではプロセスA,Bのどちらが先に実行されても最終的にisAProced == true && isBProced == trueが成立します。成立する性質の否定を使って、プロセスAから実行される場合とプロセスBから実行される場合を検出させたいと思います。

検証式

以下の検証式をモデルに追加します。

検証したい性質
ltl a01 { <>[](isAProced == true && isBProced == true) }
検証したい性質の否定
ltl c01 { !<>[](isAProced == true && isBProced == true) }
実行
検証したい性質の確認
$ spin -run -ltl a01 2pro.pml
pan: ltl formula a01

(Spin Version 6.5.0 -- 17 July 2019)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (a01)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 28 byte, depth reached 9, errors: 0
       12 states, stored (21 visited)
       13 states, matched
       34 transitions (= visited+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
    0.001	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


unreached in proctype A
	(0 of 2 states)
unreached in proctype B
	(0 of 2 states)
unreached in claim a01
	_spin_nvr.tmp:10, state 13, "-end-"
	(1 of 13 states)
unreached in claim c01
	_spin_nvr.tmp:19, state 10, "(((isAProced==1)&&(isBProced==1)))"
	_spin_nvr.tmp:21, state 13, "-end-"
	(2 of 13 states)

pan: elapsed time 0 seconds
検証したい性質がどのように成り立ったかの確認

実行してみるとエラーが3件検出されます。私の理想としては、2件の検出なのですがどの様な式にすればよいのかわかりませんでした。

$ spin -run -ltl c01 -c0 -e 2pro.pml
pan: ltl formula c01
pan:1: acceptance cycle (at depth 8)
pan: wrote 2pro.pml1.trail
pan: wrote 2pro.pml2.trail
pan: wrote 2pro.pml3.trail

(Spin Version 6.5.0 -- 17 July 2019)
	+ Partial Order Reduction

Full statespace search for:
	never claim         	+ (c01)
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	- (disabled by never claim)

State-vector 28 byte, depth reached 9, errors: 3
        9 states, stored (11 visited)
        7 states, matched
       18 transitions (= visited+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


unreached in proctype A
	(0 of 2 states)
unreached in proctype B
	(0 of 2 states)
unreached in claim c01
	_spin_nvr.tmp:21, state 13, "-end-"
	(1 of 13 states)

pan: elapsed time 0 seconds

エラートレイルの確認

プロセスBの処理が先に実行されるケース
$ spin -t1 -p 2pro.pml
ltl a01: <> ([] (((isAProced==1)) && ((isBProced==1))))
ltl c01: ! (<> ([] (((isAProced==1)) && ((isBProced==1)))))
starting claim 3
Never claim moves to line 15	[(1)]
  2:	proc  1 (B:1) 2pro.pml:11 (state 1)	[isBProced = 1]
  4: proc 1 terminates
  6:	proc  0 (A:1) 2pro.pml:6 (state 1)	[isAProced = 1]
Never claim moves to line 14	[(((isAProced==1)&&(isBProced==1)))]
  8: proc 0 terminates
  <<<<<START OF CYCLE>>>>>
Never claim moves to line 19	[(((isAProced==1)&&(isBProced==1)))]
spin: trail ends after 10 steps
#processes: 0
		isAProced = 1
		isBProced = 1
 10:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
2 processes created

$ spin -t2 -p 2pro.pml
ltl a01: <> ([] (((isAProced==1)) && ((isBProced==1))))
ltl c01: ! (<> ([] (((isAProced==1)) && ((isBProced==1)))))
starting claim 3
Never claim moves to line 15	[(1)]
  2:	proc  1 (B:1) 2pro.pml:11 (state 1)	[isBProced = 1]
  4: proc 1 terminates
  6:	proc  0 (A:1) 2pro.pml:6 (state 1)	[isAProced = 1]
Never claim moves to line 14	[(((isAProced==1)&&(isBProced==1)))]
  8: proc 0 terminates
Never claim moves to line 19	[(((isAProced==1)&&(isBProced==1)))]
  <<<<<START OF CYCLE>>>>>
spin: trail ends after 10 steps
#processes: 0
		isAProced = 1
		isBProced = 1
 10:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
2 processes created
プロセスAの処理が先に実行されるケース
$ spin -t3 -p 2pro.pml
ltl a01: <> ( (((isAProced==1)) && ((isBProced==1))))
ltl c01: ! (<> ( (((isAProced==1)) && ((isBProced==1)))))
starting claim 3
Never claim moves to line 15	[(1)]
  2:	proc  0 (A:1) 2pro.pml:6 (state 1)	[isAProced = 1]
  4:	proc  1 (B:1) 2pro.pml:11 (state 1)	[isBProced = 1]
Never claim moves to line 14	[(((isAProced==1)&&(isBProced==1)))]
  6: proc 1 terminates
Never claim moves to line 19	[(((isAProced==1)&&(isBProced==1)))]
  8: proc 0 terminates
spin: trail ends after 8 steps
#processes: 0
		isAProced = 1
		isBProced = 1
  8:	proc  - (c01:1) _spin_nvr.tmp:18 (state 10)
2 processes created

トライ&エラー

上記の結果が得られるまで、あ〜だ。こ〜だ。とトライ&エラーを繰り返しました。今後の役に立ちそうだったので残しておきます。

常に失敗させる

以下の様なLTLを記述して常に失敗させました。結果としては、18のエラーが検出されました。中身を確認すると、確かに欲しい結果が入っていたので、これを元に検証したい性質でエラーが出るように進めました。

/* errors: 18 */
ltl l01 { false }

改良1

ゴールにすこし近づくように以下を記述しました。なぜ、エラー検出数が異なるのかは、まだ理解できていません。

/* errors: 6 */
ltl l02 { !<>(isAProced == true) }

/* errors: 7 */
ltl l03 { !<>(isBProced == true) }

改良2

さらにゴールに近づけました。
これに[]を追加したものが最初に紹介した検証式となります。

/* errors: 5 */
ltl l04 { !<>(isAProced == true && isBProced == true) }