SPIN:状態の探索(2プロセス)

今回は2プロセスが動作するサンプルモデルを作成して状態空間の探索を追ってみました。前回と同じように読み解けるかと思いきや、よくわからない動きを見ることとなりました。

使用したソースは以下となります。

使用したソースから検証器の実行まで

単に2プロセスが動作するできるだけ単純になるような以下のソースを用意しました。

ソース 2p.pml

byte a;
active proctype p()
{
  a = 170; /* 0xaa = -86 */
}

byte b;
active proctype q()
{
  b = 187; /* 0xbb = -69 */
}

検証器の生成

$ spin -a -o2 2p.pml

検証器のコンパイル

$ gcc -w -g3 -DVERBOSE -DSDUMP -DNOCOMP -DNOREDUCE pan.c -o pan

実行結果

$ ./pan | cat -n
     1	0: Down - program non-accepting [pids 1-0]
     2		New state 0
     3		 State: 2,0,0,0,0,0,28,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,1,9,0,0,
     4		Vector: 2,0,0,0,0,0,28,0,0,0,0,0,0,0,0,0,0,8,0,0,0,0,0,0,1,9,0,0,
     5	Pr: 1 Tr: 3
     6	  0: proc 1 exec 3, 1 to 2, b = 187   non-accepting [tau=0]
     7	1: Down - program non-accepting [pids 1-0]
     8		New state 1
     9		 State: 2,0,0,0,0,0,28,0,0,-69,0,0,0,0,0,0,0,8,0,0,0,0,0,0,1,17,0,0,
    10		Vector: 2,0,0,0,0,0,28,0,0,-69,0,0,0,0,0,0,0,8,0,0,0,0,0,0,1,17,0,0,
    11	Pr: 1 Tr: 4
    12	  1: proc 1 exec 4, 2 to 0, -end-   non-accepting [tau=0]
    13	2: Down - program non-accepting [pids 0-0]
    14		New state 2
    15		 State: 1,0,0,0,0,0,20,0,0,-69,0,0,0,0,0,0,0,8,0,0,
    16		Vector: 1,0,0,0,0,0,20,0,0,-69,0,0,0,0,0,0,0,8,0,0,
    17	Pr: 0 Tr: 5
    18	  2: proc 0 exec 5, 1 to 2, a = 170   non-accepting [tau=0]
    19	3: Down - program non-accepting [pids 0-0]
    20		New state 3
    21		 State: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
    22		Vector: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
    23	Pr: 0 Tr: 6
    24	  3: proc 0 exec 6, 2 to 0, -end-   non-accepting [tau=0]
    25	4: Down - program non-accepting [pids -1-0]
    26		New state 4
    27		 State: 0,0,0,0,0,0,10,0,-86,-69,
    28		Vector: 0,0,0,0,0,0,10,0,-86,-69,
    29	  4: no move [II=-1, tau=0, boq=-1]
    30	4: Up - program
    31	  4: proc 0 reverses 6, 2 to 0
    32		-end- [abit=0,adepth=0,tau=0,0]
    33	3: Up - program
    34	  3: proc 0 reverses 5, 1 to 2
    35		a = 170 [abit=0,adepth=0,tau=0,0]
    36	2: Up - program
    37	  2: proc 1 reverses 4, 2 to 0
    38		-end- [abit=0,adepth=0,tau=0,0]
    39	Pr: 0 Tr: 5
    40	  1: proc 0 exec 5, 1 to 2, a = 170   non-accepting [tau=0]
    41	2: Down - program non-accepting [pids 1-0]
    42		New state 5
    43		 State: 2,0,0,0,0,0,28,0,-86,-69,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,17,0,0,
    44		Vector: 2,0,0,0,0,0,28,0,-86,-69,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,17,0,0,
    45	Pr: 1 Tr: 4
    46	  2: proc 1 exec 4, 2 to 0, -end-   non-accepting [tau=0]
    47	3: Down - program non-accepting [pids 0-0]
    48		Old state 3
    49		 State: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
    50		Vector: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
    51	3: Up - program
    52	  3: proc 1 reverses 4, 2 to 0
    53		-end- [abit=0,adepth=0,tau=0,0]
    54	Pr: 0 Tr: 6
    55	2: Up - program
    56	  2: proc 0 reverses 5, 1 to 2
    57		a = 170 [abit=0,adepth=0,tau=0,0]
    58	1: Up - program
    59	  1: proc 1 reverses 3, 1 to 2
    60		b = 187 [abit=0,adepth=0,tau=0,0]
    61	Pr: 0 Tr: 5
    62	  0: proc 0 exec 5, 1 to 2, a = 170   non-accepting [tau=0]
    63	1: Down - program non-accepting [pids 1-0]
    64		New state 6
    65		 State: 2,0,0,0,0,0,28,0,-86,0,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,9,0,0,
    66		Vector: 2,0,0,0,0,0,28,0,-86,0,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,9,0,0,
    67	Pr: 1 Tr: 3
    68	  1: proc 1 exec 3, 1 to 2, b = 187   non-accepting [tau=0]
    69	2: Down - program non-accepting [pids 1-0]
    70		Old state 5
    71		 State: 2,0,0,0,0,0,28,0,-86,-69,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,17,0,0,
    72		Vector: 2,0,0,0,0,0,28,0,-86,-69,0,0,0,0,0,0,0,16,0,0,0,0,0,0,1,17,0,0,
    73	2: Up - program
    74	  2: proc 1 reverses 3, 1 to 2
    75		b = 187 [abit=0,adepth=0,tau=0,0]
    76	Pr: 0 Tr: 6
    77	1: Up - program
    78	  1: proc 0 reverses 5, 1 to 2
    79		a = 170 [abit=0,adepth=0,tau=0,0]
    80	
    81	(Spin Version 6.4.9 -- 17 December 2018)
    82		+ FullStack Matching
    83	
    84	Full statespace search for:
    85		never claim         	- (none specified)
    86		assertion violations	+
    87		acceptance   cycles 	- (not selected)
    88		invalid end states	+
    89	
    90	State-vector 28 byte, depth reached 4, errors: 0
    91	        7 states, stored
    92	        2 states, matched
    93	        0 matches within stack
    94	        9 transitions (= stored+matched)
    95	        0 atomic steps
    96	hash conflicts:         0 (resolved)
    97	stackframes: 2/0
    98	
    99	stats: fa 0, fh 0, zh 0, zn 0 - check 0 holds 0
   100	stack stats: puts 0, probes 0, zaps 0
   101	  128.730	memory usage (Mbyte)
   102	
   103	unreached in proctype p
   104		(0 of 2 states)
   105	unreached in proctype q
   106		(0 of 2 states)
   107	
   108	pan: elapsed time 0 seconds

結果のグラフ化

上記結果を読み解いていくと前回は出てこなかった以下のパターンが54, 76行目に出てきます。「Pr: 0 Tr: 6」の部分でいきなりスタックを巻き戻し、ぱっと見ると探索を中断しているように見えます。

    51	3: Up - program
    52	  3: proc 1 reverses 4, 2 to 0
    53		-end- [abit=0,adepth=0,tau=0,0]
    54	Pr: 0 Tr: 6
    55	2: Up - program
    56	  2: proc 0 reverses 5, 1 to 2
    57		a = 170 [abit=0,adepth=0,tau=0,0]

    73	2: Up - program
    74	  2: proc 1 reverses 3, 1 to 2
    75		b = 187 [abit=0,adepth=0,tau=0,0]
    76	Pr: 0 Tr: 6
    77	1: Up - program
    78	  1: proc 0 reverses 5, 1 to 2
    79		a = 170 [abit=0,adepth=0,tau=0,0]

グラフ化したものが以下になります。「Pr: 0 Tr: 6」以降の部分は赤で表示させています。
ともに新規状態としても良さそうですが、なぜなんでしょうかね。

グラフ