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

前回「Pr: 0 Tr: 6」で探索が切れているように見える部分が気になったので、デバッグしてみました。調べられた感じでは、プロセスの削除順序が関係しているようです。一応、「プロセスは生成順序と逆順で消滅する」と記載のある資料を見つけたのでこの記述の動作に該当してそうです。ただ、1次情報までは見つけられませんでした。

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

ソース 2p.pmlを使用しています。検証器の生成とコンパイルも前回と同様となります。

デバッグ

トライ&エラーは省きますが、調べていくとdo_transitとdelprocに行き着きました。

(gdb) break do_transit 
Breakpoint 1 at 0x404d: file pan.c, line 5887.
(gdb) break delproc 
Breakpoint 2 at 0x93c6: file pan.c, line 10440.
(gdb) run 
Starting program: /home/makoto/blog/16_delproc/pan 
0: Down - program non-accepting [pids 1-0]
	New state 0
	 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,
	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,
:
(gdb) c
Continuing.
Pr: 0 Tr: 6 <-- 気になる部分

Breakpoint 2, delproc (sav=1, h=0) at pan.c:10440 <-- h=0はプロセスp
10440	{	int d, i=0;
(gdb) n
10444		if (h+1 != (int) now._nr_pr)
(gdb) 
10445		{	return 0;
(gdb) list 
10440	{	int d, i=0;
10441	#ifndef NOCOMP
10442		int o_vsize = vsize;
10443	#endif
10444		if (h+1 != (int) now._nr_pr)  <-- この条件が成立し
10445		{	return 0;             <-- delprocを抜けている。(プロセスqはまだ生きている。)
10446		}
10447	#ifdef TRIX
10448		#ifdef V_TRIX
10449			printf("%4d: delproc %d -- parent %d\n", depth, h, processes[h]->parent_pid);
(gdb) n
10530	}
(gdb) 
do_transit (t=0x55555576c350, II=0) at pan.c:5910
5910	}
:
(gdb) n
new_state () at pan.c:7126
7126				{	continue;
(gdb) list 
7121	#ifdef INLINE
7122	#include FORWARD_MOVES
7123	P999:			/* jumps here when move succeeds */
7124	#else
7125				if (!(_m = do_transit(t, II)))
7126				{	continue; <-- このルートに入り次の探索に進んでいる。
7127				}
7128	#endif
7129	#ifdef BCS
7130				if (depth > BASE

デバッグ補助

上記をみるとソースにプリプロセスディレクディブが多く含まれてきます。これがあるとかなりソースが読みにくいです。実は、この結果に行き着く際にはpan.cに含まれているコメント「gcc -E -DNOREDUCE -DBITSTATE pan.c > ppan.c」を参考に以下のようにコンパイルしてデバッグしました。

$ gcc -E -DVERBOSE -DSDUMP -DNOCOMP -DNOREDUCE pan.c | indent -sob -st -bli0 | expand | sed '/^#/d' > ppan.c
$ gcc -w -g3 ppan.c -o pan