# NuSMV 超入門 NuSMV をインストールして、簡単なモデルを書いて、それをバッチモードと対話モードで動かします。 ## インストール [NuSMV の公式サイトのダウンロードページ](https://nusmv.fbk.eu/downloads.html)に行って、バイナリを取ってきます。適当なところで展開してください。`bin` ディレクトリの中に NuSMV の実行可能バイナリがあります。 ## モデルを書く NuSMV が読み込める形で、有限状態マシンを書きます。ここでは簡単に、変数 `v1` と `v2` があって、`v1` は 1 と 2、`v2` は 3 と 4 を交互に繰り返すようなモデルを書きます。図にすると以下のような感じです。 ![simplefsm](https://hackmd.io/_uploads/HklshyD2p.png) 以下のような内容のファイルを `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 さんのかき氷の形式検証のツイート](https://twitter.com/MasWag/status/1532183190697172992)などを参考にしてください。 あと自分が NuSMV を使うきっかけになった [Mahout の例](https://github.com/ushitora-anqou/mahout/blob/bb08eb5bc3fa3c9079e009c15f02ba50465463fe/mahout.smv)などもどうぞ。
Last changed by  
 
anqou
474

Read more

Mahout: OCaml で Mastodon 用 K8s operator を書いて、NuSMV でモデル検査した

OCaml で Mastodon 用の Kubernetes operator を書きました。

2/28/2024
2023 年振り返り

Waq という ActivityPub の実装を書いていました。詳細はこちらの記事をどうぞ。

12/31/2023
OCaml で Discord 音楽ボットを書く

OCaml で Discord

12/1/2023
ISUCON 13 で 18,673 点でした

ISUCON 13 に「[a, b, u] <- 3σ」というチームで出ていました。最終スコアが 18,673 点で、公式発表のページで上から数えると 113 位くらいでした。

11/26/2023
Read more from anqou
Published on HackMD