HackMD
NuSMV 超入門
NuSMV をインストールして、簡単なモデルを書いて、それをバッチモードと対話モードで動かします。
インストール
NuSMV の公式サイトのダウンロードページに行って、バイナリを取ってきます。適当なところで展開してください。bin ディレクトリの中に NuSMV の実行可能バイナリがあります。
モデルを書く
NuSMV が読み込める形で、有限状態マシンを書きます。ここでは簡単に、変数 v1 と v2 があって、v1 は 1 と 2、v2 は 3 と 4 を交互に繰り返すようなモデルを書きます。図にすると以下のような感じです。
- The image was uploaded to a note which you don't have access to
- The note which the image was originally uploaded to has been deleted
以下のような内容のファイルを test.smv という名前で保存します。
MODULE main
VAR
v1 : {1,2};
v2 : {3,4};
ASSIGN
init(v1) := 1;
init(v2) := 3;
next(v1) :=
case
v1 = 1 : 2;
v1 = 2 : 1;
esac;
next(v2) :=
case
v2 = 3 : 4;
v2 = 4 : 3;
esac;
NuSMV に読み込ませてシミュレーションする
NuSMV の対話モードを使って、上で書いたモデルを読み込ませます。-int オプションとファイル名 test.smv を指定して NuSMV を起動します。
$ ./NuSMV -int test.smv
*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:36:56 2015)
*** Enabled addons are: compass
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@list.fbk.eu>.
*** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>>
*** Copyright (c) 2010-2014, Fondazione Bruno Kessler
*** This version of NuSMV is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado
*** This version of NuSMV is linked to the MiniSat SAT solver.
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson
NuSMV >
プロンプトが表示されるので、まず go と打ってモデルを読み込ませます。
NuSMV > go
とりあえずシミュレーションを実行してみて、作ったモデルが意図通りかを確認します。pick_state -i で初期状態を決めます。今は v1 = 1 & v2 = 3 の 1 状態しかないので、その旨が表示されます。
NuSMV > pick_state -i
*************** AVAILABLE STATES *************
================= State =================
0) -------------------------
v1 = 1
v2 = 3
There's only one available state. Press Return to Proceed.
Chosen state is: 0
続いて 1 ステップ状態を進めます。simulate -k 1 -i を使います。-k はステップ数です。進む先は v1 = 2 & v2 = 4 の 1 状態しかないので、やはりその旨が表示されます。
NuSMV > simulate -k 1 -i
******** Simulation Starting From State 1.1 ********
*************** AVAILABLE STATES *************
================= State =================
0) -------------------------
v1 = 2
v2 = 4
There's only one available state. Press Return to Proceed.
Chosen state is: 0
さらにもう 1 ステップ進めると、初期状態に戻ってきます。
NuSMV > simulate -k 1 -i
******** Simulation Starting From State 1.2 ********
*************** AVAILABLE STATES *************
================= State =================
0) -------------------------
v1 = 1
v2 = 3
There's only one available state. Press Return to Proceed.
Chosen state is: 0
うまくできてそうです。
CTL と LTL でモデル検査する
続いて CTL を使ってモデル検査をしてみます。例えば、どんなときも v1 = 1 かつ v2 = 4 になることは絶対にないこと（AG !(v1 = 1 & v2 = 4)）を検査してみます：
NuSMV > check_ctlspec -p "AG !(v1 = 1 & v2 = 4)"
-- specification AG !(v1 = 1 & v2 = 4) is true
続いて、常に v1 = 1 かつ v2 = 3 であること AG (v1 = 1 & v2 = 3) 検査してみます。これは偽なので、反例が表示されます：
NuSMV > check_ctlspec -p "AG (v1 = 1 & v2 = 3)"
-- specification AG (v1 = 1 & v2 = 3) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 3.1 <-
v1 = 1
v2 = 3
-> State: 3.2 <-
v1 = 2
v2 = 4
同様に LTL でもモデル検査できます：
NuSMV > check_ltlspec -p "G !(v1 = 1 & v2 = 4)"
-- specification G !(v1 = 1 & v2 = 4) is true
NuSMV > check_ltlspec -p "G (v1 = 1 & v2 = 3)"
-- specification G (v1 = 1 & v2 = 3) is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-- Loop starts here
-> State: 4.1 <-
v1 = 1
v2 = 3
-> State: 4.2 <-
v1 = 2
v2 = 4
-> State: 4.3 <-
v1 = 1
v2 = 3
対話モードは quit で終了できます。
NuSMV > quit
バッチモードでモデル検査する
NuSMV には対話モードのほかにバッチモードもあります。単にファイル名を指定して NuSMV を起動すると、ファイルに書かれたモデルを読み込み、モデル検査を行います。
先程のモデルにモデル検査を行うための記述を追加します：
MODULE main
VAR
v1 : {1,2};
v2 : {3,4};
ASSIGN
init(v1) := 1;
init(v2) := 3;
next(v1) :=
case
v1 = 1 : 2;
v1 = 2 : 1;
esac;
next(v2) :=
case
v2 = 3 : 4;
v2 = 4 : 3;
esac;
-- 以下を追加
CTLSPEC AG !(v1 = 1 & v2 = 4);
CTLSPEC AG (v1 = 1 & v2 = 3);
LTLSPEC G !(v1 = 1 & v2 = 4);
LTLSPEC G (v1 = 1 & v2 = 3);
NuSMV をバッチモードで起動すると、指定した仕様が検証できたことがわかります。違反する仕様があると、対話モードときと同様に反例を出してくれます：
$ ./NuSMV test.smv
*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:36:56 2015)
*** Enabled addons are: compass
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@list.fbk.eu>.
*** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>>
*** Copyright (c) 2010-2014, Fondazione Bruno Kessler
*** This version of NuSMV is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado
*** This version of NuSMV is linked to the MiniSat SAT solver.
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson
-- specification AG !(v1 = 1 & v2 = 4) is true
-- specification AG (v1 = 1 & v2 = 3) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
v1 = 1
v2 = 3
-> State: 1.2 <-
v1 = 2
v2 = 4
-- specification G !(v1 = 1 & v2 = 4) is true
-- specification G (v1 = 1 & v2 = 3) is false
-- as demonstrated by the following execution sequence
Trace Description: LTL Counterexample
Trace Type: Counterexample
-- Loop starts here
-> State: 2.1 <-
v1 = 1
v2 = 3
-> State: 2.2 <-
v1 = 2
v2 = 4
-> State: 2.3 <-
v1 = 1
v2 = 3
おわり
おわりです。
参考情報
NuSMV 公式のチュートリアルとユーザーマニュアルが詳しいのでオススメです。
- チュートリアル https://nusmv.fbk.eu/tutorials.html
- ユーザーマニュアル https://nusmv.fbk.eu/user-manual.html
NuSMV を使ったモデル検査のもう少し実用的な例は、Masaki Waga さんのかき氷の形式検証のツイートなどを参考にしてください。
あと自分が NuSMV を使うきっかけになった Mahout の例などもどうぞ。
