spin によるモデル検証。 ただしここでは、モデルを記述するための言語 PROMELA ではなく、検証ツール spin のコマンドライン引数に重点をおいて記述。
最小の PROMELA コードは以下のようになる。
/* ex01.pml */
init {
skip;
}
このコードを検証する spin コマンド呼び出しは以下のようになる。
spin ex01.pml
現在のバージョンで実行すると画面に表示される結果は、
1 process created
で終わり。このコードに対して指定できるオプションとしては -v と -p がある。-v を指定すると、
Starting :init: with pid 0 1: proc 0 (:init:) line 2 "ex01.pml" (state 1) [(1)] 1 process created
と少し詳細な情報が表示される。-p を指定すると、
Starting :init: with pid 0 0: proc - (:root:) creates proc 0 (:init:) 1: proc 0 (:init:) line 2 "ex01.pml" (state 1) [(1)] 1: proc 0 (:init:) terminates 1 process created
とさらに詳しい情報が表示される。
プロセスを生成するコードは以下のようになる。proctype でプロセスの動作を記述し、run で起動する。
/* ex02.pml */
proctype A() {
skip;
}
proctype B() {
skip;
}
init {
run A();
run B();
}
最小構成と比較して指定できるコマンドライン引数が増えるわけではないので、ここはスルー。
プロセスは、各プロセスが共有するグローバル変数と、宣言したプロセス内でのみアクセスできるローカル変数を利用できる。
/* ex03.pml */
byte turn = 0;
proctype A() {
byte a;
a = turn;
turn = a + 1;
}
proctype B() {
byte b;
b = turn + 1;
turn = b;
}
init {
run A();
run B()
}
最小構成から使える -v はここでも指定できるが、さらに -g や -l を指定することで、グローバル変数やローカル変数を 合わせて表示することができる。-v を指定したとき、
spin -v ex03.pml
例えば以下のように表示される。
Starting :init: with pid 0 Starting A with pid 1 1: proc 0 (:init:) line 17 "ex03.pml" (state 1) [(run A())] Starting B with pid 2 2: proc 0 (:init:) line 18 "ex03.pml" (state 2) [(run B())] 3: proc 2 (B) line 12 "ex03.pml" (state 1) [b = (turn+1)] 4: proc 2 (B) line 13 "ex03.pml" (state 2) [turn = b] 5: proc 1 (A) line 6 "ex03.pml" (state 1) [a = turn] 6: proc 1 (A) line 7 "ex03.pml" (state 2) [turn = (a+1)] 3 processes created
ここで、 -g を合わせて指定すると、
spin -v -g ex03.pml
以下のように、グローバル変数である turn の内容がステップごとに表示される。
Starting :init: with pid 0
Starting A with pid 1
1: proc 0 (:init:) line 17 "ex03.pml" (state 1) [(run A())]
turn = 0
Starting B with pid 2
2: proc 0 (:init:) line 18 "ex03.pml" (state 2) [(run B())]
turn = 0
3: proc 1 (A) line 6 "ex03.pml" (state 1) [a = turn]
turn = 0
4: proc 1 (A) line 7 "ex03.pml" (state 2) [turn = (a+1)]
turn = 1
5: proc 2 (B) line 12 "ex03.pml" (state 1) [b = (turn+1)]
turn = 1
6: proc 2 (B) line 13 "ex03.pml" (state 2) [turn = b]
turn = 2
3 processes created
また、-l を合わせて指定した場合は以下のように、各プロセスのローカル変数が表示される。
Starting :init: with pid 0
Starting A with pid 1
1: proc 0 (:init:) line 17 "ex03.pml" (state 1) [(run A())]
Starting B with pid 2
2: proc 0 (:init:) line 18 "ex03.pml" (state 2) [(run B())]
3: proc 2 (B) line 12 "ex03.pml" (state 1) [b = (turn+1)]
B(2):b = 1
4: proc 2 (B) line 13 "ex03.pml" (state 2) [turn = b]
B(2):b = 1
5: proc 1 (A) line 6 "ex03.pml" (state 1) [a = turn]
A(1):a = 1
6: proc 1 (A) line 7 "ex03.pml" (state 2) [turn = (a+1)]
A(1):a = 1
3 processes created
両方 (-l -g) 指定した場合は、両方を表示する。
上の例のように spin をそのまま実行した場合、プロセスの実行順序によって複数の状態を取りうるコードの場合は、 spin の実行ごとにどれか一つの状態遷移を行い、その内容を表示する。 取りうる状態を対話的に選択していく方法として -i が用意されており、 動作を確認しながら、という時には有効であるが、本来の目的であるモデル検証を行う場合には表示される情報量が多すぎ、 全状態を確認するために複数回実行するのは効率が悪い。
コードが取りうるすべての状態を検証するために spin は、PROMELA コードを C コードに変換してコンパイルし、 ネイティブアプリとして実行する形で実行速度を確保している。 そしてモデル検証を自動的に行うため PROMELA コードには状態を確認する命令を置き、 あらかじめ指定した条件に適合しない状態になった場合をエラーとして通知して、後から解析する形としている。
PROMELA コードを C コードに変換してコンパイルし、実行するには、以下のコマンドを順に実行する。
spin -a ex03.pml gcc -o pan pan.c ./pan
結果は以下のように表示される。
hint: this search is more efficient if pan.c is compiled -DSAFETY
(Spin Version 5.1.6 -- 9 May 2008)
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles - (not selected)
invalid end states +
State-vector 12 byte, depth reached 2, errors: 0
3 states, stored
0 states, matched
3 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
2.501 memory usage (Mbyte)
unreached in proctype :init:
(0 of 2 states)
pan: elapsed time 0 seconds
ここで、pan.c をコンパイルする場合にマクロ定義で動作を変更する方法と、 コンパイラで生成されたコマンド ( pan ) に渡すコマンドライン引数、 さらに pan コマンド実行中に検出したエラーを解析するために使用する spin コマンドのコマンドライン引数と、 説明を続けるつもりだったが、今日はここまで。