SPIN,C言語,デバッグ:State Vectorと変数
「SpinIntro.pdf」の「SPIN's Basic Data Structures」を見ると状態ベクトル(State vecot)は全ての変数を保持している旨の記載があります。また、PanのCompile-Time Optionsには状態ベクトルをダンプするオプション(SDUMP)について記載があります。
コンパイルオプションを指定して状態ベクトルを出力させてみたのですが、読み方がわからず、私は読み方の情報も探せませんでした。ちょうどpanのソースはC言語なので変数の部分に着目してデバッグしてみました。
使用したソースは以下となります。
使用したソースから検証器の実行まで
ソース 2p.pml
byte a; active proctype p() { a = 170; /* 0xaa = -86 */ } byte b; active proctype q() { b = 187; /* 0xbb = -69 */ }
検証器の生成
検証器の生成時に-o2オプションを使用しています。今回使用したソースでは、-o2オプションを使用しないと変数a,bが状態ベクトルに含まれてきませんでした。これは、aとbを書き込みにのみ使用しているためと思われます。
$ spin -a -o2 2p.pml
実行結果
今回のケースではStateとVectorが同じ値になりました。(NOCOMPの効果?)
^が変数aとbの部分となります。顕著な変化があるのは以下の部分となります。
- New state 1 でStateが変化しています。0から-69になっている部分がbの部分でb = 187 によるものです。
- New state 3 でStateが変化しています。0から-86になっている部分がaの部分でa = 170 によるものです。
$ ./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,
^a^b
Pr: 1 Tr: 3
0: proc 1 exec 3, 1 to 2, b = 187 non-accepting [tau=0]
1: Down - program non-accepting [pids 1-0]
New state 1
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,
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,
^a^^^b
1: proc 1 PreSelected (tau=32)
Pr: 1 Tr: 4
1: proc 1 exec 4, 2 to 0, -end- non-accepting [tau=32]
2: Down - program non-accepting [pids 0-0]
New state 2
State: 1,0,0,0,0,0,20,0,0,-69,0,0,0,0,0,0,0,8,0,0,
Vector: 1,0,0,0,0,0,20,0,0,-69,0,0,0,0,0,0,0,8,0,0,
^a^^^b
Pr: 0 Tr: 5
2: proc 0 exec 5, 1 to 2, a = 170 non-accepting [tau=0]
3: Down - program non-accepting [pids 0-0]
New state 3
State: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
Vector: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
^^^a^^^b
Pr: 0 Tr: 6
3: proc 0 exec 6, 2 to 0, -end- non-accepting [tau=0]
4: Down - program non-accepting [pids -1-0]
New state 4
State: 0,0,0,0,0,0,10,0,-86,-69,
Vector: 0,0,0,0,0,0,10,0,-86,-69,
^^^a^^^b
4: no move [II=-1, tau=0, boq=-1]
4: Up - program
4: proc 0 reverses 6, 2 to 0
-end- [abit=0,adepth=0,tau=0,0]
3: Up - program
3: proc 0 reverses 5, 1 to 2
a = 170 [abit=0,adepth=0,tau=0,0]
2: Up - program
2: proc 1 reverses 4, 2 to 0
-end- [abit=0,adepth=0,tau=0,32]
1: Up - program
1: proc 1 reverses 3, 1 to 2
b = 187 [abit=0,adepth=0,tau=32,0]
Pr: 0 Tr: 5
0: proc 0 exec 5, 1 to 2, a = 170 non-accepting [tau=0]
1: Down - program non-accepting [pids 1-0]
New state 5
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,
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,
^a^^^b
Pr: 1 Tr: 3
1: proc 1 exec 3, 1 to 2, b = 187 non-accepting [tau=0]
2: Down - program non-accepting [pids 1-0]
New state 6
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,
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,
^^^a^^^b
2: proc 1 PreSelected (tau=32)
Pr: 1 Tr: 4
2: proc 1 exec 4, 2 to 0, -end- non-accepting [tau=32]
3: Down - program non-accepting [pids 0-0]
Old state 3
State: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
Vector: 1,0,0,0,0,0,20,0,-86,-69,0,0,0,0,0,0,0,16,0,0,
^^^a^^^b
3: Up - program
3: proc 1 reverses 4, 2 to 0
-end- [abit=0,adepth=0,tau=0,32]
2: Up - program
2: proc 1 reverses 3, 1 to 2
b = 187 [abit=0,adepth=0,tau=32,0]
Pr: 0 Tr: 6
1: Up - program
1: proc 0 reverses 5, 1 to 2
a = 170 [abit=0,adepth=0,tau=0,0]
(Spin Version 6.4.9 -- 17 December 2018)
+ Partial Order Reduction
+ FullStack Matching
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 28 byte, depth reached 4, errors: 0
7 states, stored
1 states, matched
0 matches within stack
8 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
stackframes: 2/0
stats: fa 0, fh 0, zh 0, zn 0 - check 3 holds 2
stack stats: puts 0, probes 0, zaps 0
128.730 memory usage (Mbyte)
unreached in proctype p
(0 of 2 states)
unreached in proctype q
(0 of 2 states)
pan: elapsed time 0 seconds
State の出力部分をGDBで調べる
実際にデバッグした際はmainから調べるなどトライ&エラーしていますが、以下の説明ではその辺りは省略しています。
pan実行時のState:...部分を出力しているdumpstate関数にブレークポイントを設定することからデバッグを始めています。
$ gdb ./pan
GNU gdb (Ubuntu 8.1-0ubuntu3) 8.1.0.20180409-git
Copyright (C) 2018 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law. Type "show copying"
and "show warranty" for details.
This GDB was configured as "x86_64-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<http://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
<http://www.gnu.org/software/gdb/documentation/>.
For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from ./pan...done.
(gdb) break dumpstate <-- トライ&エラーでこの関数でState: ...の部分が出力されいることを予め調べています。
Breakpoint 1 at 0xa050: file pan.c, line 11346.
(gdb) run
Starting program: /home/makoto/blog/13/pan
0: Down - program non-accepting [pids 1-0]
New state 0
Breakpoint 1, dumpstate (wasnew=-1, v=0x55555576d1e0 <now> "\002", n=28, tag=1) at pan.c:11346
11346 printf(" State: ");
(gdb) until
11351 for (i = 0; i < vsize; i++)
(gdb)
11352 printf("%d,", ((char *)&now)[i]); <-- ここでコンマセパレートで出力されています。
(gdb)
11351 for (i = 0; i < vsize; i++)
(gdb)
11354 printf("\n Vector: ");
(gdb)
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,
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
出力されているのは、nowの値のようです。
11355 for (i = 0; i < n; i++)
(gdb) ptype now <-- nowの型を調べます。
type = struct State {
unsigned char _nr_pr;
unsigned char _nr_qs;
unsigned char _a_t;
unsigned char _cnt[2];
unsigned short _vsz;
unsigned char a; <-- 変数a
unsigned char b; <-- 変数b
unsigned char sv[1024];
}
(gdb) l 11352
11347 #if !defined(NOCOMP) && !defined(HC)
11348 for (i = 0; i < vsize; i++) printf("%d%s,",
11349 ((char *)&now)[i], Mask[i]?"*":"");
11350 #else
11351 for (i = 0; i < vsize; i++)
11352 printf("%d,", ((char *)&now)[i]); <-- NOCOMPを定義しているのでこのルートを通ります。
11353 #endif
11354 printf("\n Vector: ");
11355 for (i = 0; i < n; i++)
11356 printf("%d,", v[i]);
(gdb) continue
Continuing.
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,
Pr: 1 Tr: 3
0: proc 1 exec 3, 1 to 2, b = 187 non-accepting [tau=0]
1: Down - program non-accepting [pids 1-0]
New state 1
Breakpoint 1, dumpstate (wasnew=-1, v=0x55555576d1e0 <now> "\002", n=28, tag=2) at pan.c:11346
^^^^^^^^^^^^2回目のブレークなので、b=187が実行された後となります。
11346 printf(" State: ");
(gdb) p now
$1 = {_nr_pr = 2 '\002', _nr_qs = 0 '\000', _a_t = 0 '\000', _cnt = "\000", _vsz = 28, a = 0 '\000',
b = 187 '\273',
sv = "\000\000\000\000\000\000\000\b\000\000\000\000\000\000\001\021", '\000' <repeats 1007 times>}
-> nowの中身を見るとbは187となっています。
(gdb) until
11351 for (i = 0; i < vsize; i++)
(gdb)
11352 printf("%d,", ((char *)&now)[i]);
(gdb)
11351 for (i = 0; i < vsize; i++)
(gdb)
11354 printf("\n Vector: ");
(gdb)
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,
^^^^^^^^^^^^^^^^^^^^^^^
+0,1,2,3,4,5, 6,7,8, 9
-> 9個目がbの場所となります。詳細を調べてみます。
11355 for (i = 0; i < n; i++)
(gdb) printf "%d\n", (char)187
-69
(gdb) p (char *)(&now.b) - (char *)&now <-- nowの先頭とnow.bの差を確認する。
$9 = 9
(gdb) x/16x &now
+0 +1 +2 +3 +4 +5 +6 +7
0x55555576d1e0 <now>: 0x02 0x00 0x00 0x00 0x00 0x00 0x1c 0x00
+8 +9
0x55555576d1e8 <now+8>: 0x00 0xbb 0x00 0x00 0x00 0x00 0x00 0x00状態aとbを保持したState型の変数nowがコンマセパレートで出力されていました。
