モデル検査器 Spin の動作実験（Spin の手っ取り早い動かし方）
モデル検査器 Spin の動作実験
1. モデルの作成
まず検査対象のモデルを作成する．モデルは Promela と言う言語で作成する．ここでは，例えば，以下のようなOn とOff を繰り返すトグルスイッチのPromela コードを用意した．このコードを switch.p として適当なフォルダに保存．
switch.p
mtype = {on, off};
mtype sw = on;active proctype P(){
do
::(sw==on) -> sw=off
::(sw==off) -> sw=on
od
}
2. シミュレーション
SPIN はモデル検査器以外にも，シミュレーションとして使うことができる．シミュレーションは以下のように実行する．
> spin -v switch.p
コマンドオプション「-v」は verbose の v, つまり，実行結果に関して「多弁」に語ってくれます．
$ spin -v switch.pml
Starting P with pid 0
warning: never claim not used in random simulation
1: proc 0 (P) line 6 "switch.pml" (state 5) [( (sw==on) )]
2: proc 0 (P) line 7 "switch.pml" (state 2) [sw = off]
3: proc 0 (P) line 10 "switch.pml" (state 6) [.(goto)]
4: proc 0 (P) line 6 "switch.pml" (state 5) [( (sw==off))]
5: proc 0 (P) line 8 "switch.pml" (state 4) [sw = on]
6: proc 0 (P) line 10 "switch.pml" (state 6) [.(goto)]
7: proc 0 (P) line 6 "switch.pml" (state 5) [( (sw==on))]
8: proc 0 (P) line 7 "switch.pml" (state 2) [sw = off]
9: proc 0 (P) line 10 "switch.pml" (state 6) [.(goto)]
10: proc 0 (P) line 6 "switch.pml" (state 5) [( (sw==off))]
11: proc 0 (P) line 8 "switch.pml" (state 4) [sw = on]
12: proc 0 (P) line 10 "switch.pml" (state 6) [.(goto)]
13: proc 0 (P) line 6 "switch.pml" (state 5) [( (sw==on))]
14: proc 0 (P) line 7 "switch.pml" (state 2) [sw = off]
15: proc 0 (P) line 10 "switch.pml" (state 6) [.(goto)]
...
3. モデル検査
SPIN のモデル検査器の実行は NuSMV など他のモデル検査器と比べて少しトリッキーで，多くの手順を踏む．しかし慣れてくるとこれらはなんともなく，また以下に示す手順はXspin を用いると楽になる．SPIN では，モデル検査の実行にはいくつかの手順を踏む．以下にその手順を示す．
3.1. 検証（検証器の作成）
まずモデル検査器を実行するために，モデル検査器の作成を行う．モデル検査器の作成は以下のように「-a」オプションをつけて，先ほどのうえで作成したコードを実行．
> spin -a switch.p
これにより，pan.c というC言語のコード（モデル検査器）が作成される．これを実行するために，以下の通りコンパイルを行う．
> gcc pan.c
> ./a
これにより，モデル検査器が作成された．
3.2. 検証（検査コードの作成）
次に，検査式をもとに，検査コードを作成する．検査コードを作成には、『-f 'LTL式'』と入力する．例えば，以下は「[]p」 という検査式をもとに，検査コードを作成し，それを「safety.ltl」というファイルに書き込む．
> spin -f '[]p' > safety.ltl
これにより，検査コードが生成された．しかし，ここで，検査式中に現れる「p」とモデル中の記述が関連付けられていない．以下のように関連付ける．
#define p (sw==on)
> spin -a -N safety.ltl switch.p
- N は検査式のファイルを読み込む指定をします．
> gcc pan.c
> ./a
3.3.反例の検出
実は，SPIN では，検査式を入植した場合，Never Claim として理解されるため，検査したい性質を表現したい「検査式の否定」を用いる必要がある．つまり，例えば上の場合，LTL式を『![]p』に変更するひつようがある．以下同じ手順を繰り返せばよい．
> spin -f '![]p' > safety.ltl
これを実行すると出力メッセージに以下のようにエラーが検出されたと報告される．
error: 1
swの値は必ずon、offを繰り返すので，エラーが出力されるはずである．エラーが出力された場合，その反例のパスが『promelaのファイル名.tral』ファイルに出力されます・この反例パスをシミュレーションの時のように表示させたい場合は『-t ファイル名』コマンドを入力．
> spin -t -p -g switch.p
