NuSMVチュートリアルメモ
http://nusmv.irst.itc.it/NuSMV/tutorial/index.html
上のURLにあるNuSMVのチュートリアルを読みながらのメモ。ヴァージョン2.4のチュートリアルをダウンロードしたつもりが何故かPDFのタイトルは2.2。
NuSMV 2.2 Tutorial 1. Introduction このチュートリアルはNuSMVの主な機能について説明する 2. Example NuSMVは有限状態モデルを記述できる 同期システムでも非同期システムでもOK 再利用可能なコンポーネントによって記述し易くなっている 単一プロセスの記述を組み合わせて並行プロセスを記述できるから、 普通のプログラミング言語のように簡単 静的型システムを持っている 論理値（0か1） スカラ型 固定長配列 2.1 Synchronous Systems 2.1.1 Single Process Example 変数は前の状態に応じて次の状態の値が割り当てられる 全く値が定義されていない変数は、例えば論理型であれば0か1のどちらかを取り得る 2.1.2 Binary Counter モジュールからインスタンスを生成できる DEFINEキーワードによって、状態を増やさず変数の組み合わせに名前を付けられる 変数の組み合わせであるので当然非決定的な振る舞いはしない # DEFINEと変数追加のもう一つの違いがよくわからない # 変数の型がプライオリに決定されるとか何とか… 2.2 Asynchronous Systems 並行であったり同期的であったりするシステムを記述できる 2.2.1 Inverter Ring processキーワードを付けてインスタンスを生成すれば、 動作するプロセスが非決定的に選択される しかしこのままではプロセスが動かない だからFAIRNESSキーワードを用いてプロセスが動くようにする # しかしあってもなくてもシミュレーション上の動きは変わらないような… # livenessの検証の時にはちょっと変わるかな processキーワードを使わずとも、union演算子によって非決定的な動作は記述できる でもFAIRNESSを使った場合と同じようにはいかない 全てのプロセスが休んでしまったりする 2.2.2 Mutual Exclusion 2.3 Direct Specification INITとTRANSキーワードによって有限状態モデルを直接記述できる しかし、初期状態が空だったり遷移が全写でなかったりと、 論理的な矛盾も許してしまう # VARとASSIGNを使う場合と具体的にどういう違いがあるのかよくわからない… 3. Simulation シミュレーションはモデルがちゃんと出来ているか調べるのに有効 3.1 Trace Strategies NuSMVにおけるシミュレーションは3つのやり方がある 決定的 遷移できる状態の中で一番目が選ばれる ランダム 勝手に非決定的な選択がなされる インタラクティヴ 毎ステップユーザが選択する 選択肢が多すぎると閾値以下の選択肢数になるまで制限される # システムは矛盾を受け入れない（遷移する状態が空だとか）…でも例がよくわからない # インタラクティヴにおいて制限がかかる場合、変な選択肢が避けられる…？ 3.2 Interactive Mode 3.2.1 Choosing an Initial State 初期状態を選ぶには3つの方法がある 現在の状態をそのまま使う（もしあれば） goto_stateコマンドで既存の状態を使う pick_stateコマンドでモデルの初期状態から始める 初めての場合はこれ 全ての状態は何らかの軌跡に属していて、「軌跡番号.状態番号」のように表される 3.2.2 Starting a New Simulation 3.2.3 Specifying Constructions pick_stateにオプション-cを使って式を与えることによって、 初期状態の選択肢を制限することができる この制限は持続しないから持続させるにはsimulationにも同じ指定をする 4. CTL Model Checking NuSMVはCTLとLTLの両方使える 4.1 Computation Tree Logic CTL（計算木論理）は非決定的な遷移を木で表す 有限状態オートマトンのそれぞれの状態が木のノードに対応している CTLではAF, EF, AG, EG, U, AX, EXなどの演算子が使えて入れ子にもできる 反例は常に得られるわけではない 一つのパスを示しても、パスが存在しないことを証明できない 一つのパスを示しても、常に成り立つことを証明できない 4.2 Semaphore Example 二つのプロセスが同時にcritial状態にならないことと、 プロセス1がenteringになったらその後いつかcriticalになることを検証する 後者はループしてしまってfalseになる 5. LTL Model Checking 5.1 Linear Temporal Logic CTLが有限状態オートマトンを木で表したのに対し、 LTL（線形時相論理）は線形の経路として表す LTLとCTLは力が違うが時相演算子の共通点はある F, G, U, X などの演算子が使える LTLには限定記号がないので、全ての経路でtrueならtrueになる 5.2 Semaphore Example 5.3 Past Temporal Operators NuSMVのLTLは過去演算子も使えて便利 O p - 過去に一度pが満たされた H p - これまでずっとpが満たされていた p S q - qが満たされていた時点からpが満たされていた Y p - 前の状態ではpが満たされていた 6. Bounded Model Checking NuSMVにおける有界モデル検査について紹介する 6.1 Checking LTL Specification 0から7までを繰り返すカウンタをモデルとし、 オプション-bmcを付けたうえで、LTL式G (y=4 -> y=6)を検証する yが4の後は5になるので、これはfalseであり、反例が出力される しかし-bmc_lengthを4に指定した場合、反例は出力されない 4回までの遷移ではこの反例を見つけることはできないから 一方LTL式!G F (y=2)を検証する（y=2となることは繰り返されないの意味） ループを検出すれば繰り返されることが明らかになるので、8回の遷移でOK 6.2 Finding Counterexamples 活性の反例はループとなる 時刻kから時刻lにループしていれば、時刻k+1と時刻l+1の状態は等しい インタラクティヴモードにおいて、check_ltlspec_bmc_onepbコマンドを使えば、 反例のループの時刻を細かく指定できる k=9でl=0だと反例は出力されない k=8でl=1でも反例は出力されない k=9でl=1だとOK オプション-lにマイナスを指定すると、ループの長さを直接指定できる オプション-lにXを指定すると、ループ反例は出力されない オプション-lに*を指定すると、どんな長さのループも出力される 6.3 Checking Invariants NuSMVの2.2.2から2ステップだけではない帰納的推論がサポートされるようになった 6.3.1 2-Step Inductive Reasoning NuSMVの有界モデル検査はLTLだけではなくinvariantも検証することができる これには帰納的推論が使われ、次のように行われる (1)全ての初期状態で満たすことを調べる (2)これを満たす状態から導かれる状態で満たすことを調べる 先ほどのカウンタに対してy in (0..12)というinvariantを調べてみると、 y=12の後y=13となってfalseになる 実際はy=12となることはないのでこれは間違った結果 y in (0..7)であればOK y in (0..6)だとy=7という反例が出力され、これは正しい 6.3.2 Complete Invariant Checking インタラクティヴモードでcheck_invar_bmcコマンドを使い、 オプション-a（アルゴリズム）でeen-sorenssonを指定すると、 完全な帰納的推論が行われる 2ステップでは失敗したy in (0..12)もきちんとtrueになる # どういうわけでtrueになるのかよくわからない…
