プログラミングなどなど

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

SPIN:Never Claimと通常プロセスの動作の違いに気をつけよう

SPIN

SPINでは検証式の記述に時相論理という論理が使えるのですが、よく理解できなかったので簡単なものから理解していこうと考えました。しかし、単純と思いきやハマった例を紹介します。ハマった部分を確認しようとしましたが、結果としては現状、手詰まりとなりました。

モデル(never.pml)

以下のようなモデルと検証式があるとします。

bool i = false;

active proctype A()
{
  i = true;
}

ltl { i == false }

検証の実行

上記のLTLの検証結果を予想してみて下さい。

$ spin -run never.pml 
(Spin Version 6.5.0 -- 17 July 2019)
	+ Partial Order Reduction

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

State-vector 20 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.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


unreached in proctype A
	never.pml:6, state 2, "-end-"
	(1 of 2 states)
unreached in claim ltl_0
	_spin_nvr.tmp:8, state 8, "-end-"
	(1 of 8 states)

pan: elapsed time 0 seconds

私はエラーが検出されると想定しました。しかし、エラー無しとなりました。

記述したLTLのPromelaコードの確認

以下のコマンドを実行し、記述したLTLからどの様なNever ClaimがPromeralコードとして生成されたかを確認してみます。

$ spin -a never.pml 
ltl ltl_0: (i==0)
$ cat -n _spin_nvr.tmp 
     1	never ltl_0 {    /* !((i==0)) */
     2	accept_init:
     3	T0_init:
     4		do
     5		:: atomic { (! (((i==0)))) -> assert(!(! (((i==0))))) }
     6		od;
     7	accept_all:
     8		skip
     9	}

現状の私の理解は次のとおりです。

  1. 5行目の!(((i==0)))はプロセスAのi = trueが実行されるまでは、成立しないので、do文で実行可能な処理がなくブロックされる。
  2. プロセスAのi = trueが実行されると、Never Claimの!(((i==0)))が成立し、assertが実行されエラーが検出される。

しかし、エラーは検出されませんでした。

LTLのPromelaコードから通常プロセスを作る

現状、私は通常プロセスとNever Claimの違いについて、Never Claimは検証対象のプロセスの1ステップ毎にNever Claimの検証を行う。と理解しています。
そこで、得られたPromelaコードを通常プロセスとして実装した場合、検証漏れはあるかもしれませんが、今回のケースでは網羅的な検証でエラーが無いことになっているので、通常プロセスにしても0件になるのではないかと予想し試すことにしました。

追記したコード

ltlの部分を以下のコードに置き換えます。

active proctype B() {    /* !((i==0)) */
accept_init:
T0_init:
  do
  :: atomic { (! (((i==0)))) -> assert(!(! (((i==0))))) }
  od;
accept_all:
  skip
}

検証の実行

$ spin -run never.pml
pan:1: assertion violated  !( !((i==0))) (at depth 1)
pan: wrote never.pml.trail

(Spin Version 6.5.0 -- 17 July 2019)
Warning: Search not completed
	+ Partial Order Reduction

Full statespace search for:
	never claim         	- (none specified)
	assertion violations	+
	acceptance   cycles 	+ (fairness disabled)
	invalid end states	+

State-vector 20 byte, depth reached 1, errors: 1
        2 states, stored
        0 states, matched
        2 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



pan: elapsed time 0 seconds

なんと、エラーを検出しました。今のPromelaコードの理解としてはこちらの方がしっくりくるのですが、Never Claimの動作理解としては、ここでお手上げとなりました。

状態テーブルに違があるかを確認

他に差異があるかを確認できないかと考えて状態表(-dオプション)を比べて見ましたが、同じでした。

Never Claim

$ ./pan -d
proctype A
	state   1 -(tr   5)-> state   2  [id   0 tp   2] [----G] never.pml:5 => i = 1
	state   2 -(tr   6)-> state   0  [id   1 tp 3500] [--e-L] never.pml:6 => -end-
claim ltl_0
	state   4 -(tr   3)-> state   4  [id   2 tp   2] [-a--G] never.pml:4 => (!((i==0)))

Transition Type: A=atomic; D=d_step; L=local; G=global
Source-State Labels: p=progress; e=end; a=accept;
Note: statement merging was used. Only the first
      stmnt executed in each merge sequence is shown
      (use spin -a -o3 to disable statement merging)

pan: elapsed time 1.72e+07 seconds
pan: rate         0 states/second

通常プロセス

$ ./pan -d
proctype A
	state   1 -(tr   5)-> state   2  [id   0 tp   2] [----G] never.pml:5 => i = 1
	state   2 -(tr   6)-> state   0  [id   1 tp 3500] [--e-L] never.pml:6 => -end-
proctype B
	state   4 -(tr   3)-> state   4  [id   2 tp   2] [-a--G] never.pml:12 => (!((i==0)))

Transition Type: A=atomic; D=d_step; L=local; G=global
Source-State Labels: p=progress; e=end; a=accept;
Note: statement merging was used. Only the first
      stmnt executed in each merge sequence is shown
      (use spin -a -o3 to disable statement merging)

pan: elapsed time 1.72e+07 seconds
pan: rate         0 states/second

結果(手詰まり)

自分は手詰まりとなりました。前回の記事(SPIN:LTLの記述によっては意図した検査にならない? - プログラミングなどなど)のようにデバッグしてみると、Never Claimの遷移処理が走っていますが、どこにも遷移せずにすぐに検証が終了していました。感覚としては、検証時の最初のステップでNever Claimがどこにも移動できないような記述がある時に問題となるケースがありそうです。自分のLTLの記述が悪い感じもありますが。