NuSMV Version 2 の使い方メモ

まず、~kam/sysverif/simple.smv を見て概要を理解してください。
同じファイルは、授業ホームページにも置いてあります。
http://logic.cs.tsukuba.ac.jp/~kam/sysverif/simple.smv

この入力ファイルについての説明を以下に書きます。

* 入力ファイルの基本構成は以下の通り。

  ----------------------------------------------------
  MODULE モジュール名
  VAR 
     変数1の定義 (定義の終わりに ; を書く)
     変数2の定義
     ...
     (定義の順番は適当でよい)
  ASSIGN
     初期状態における変数1の値を決める式  (式の終わりに ; を書く)
     初期状態における変数2の値を決める式
     次の瞬間における変数1の値を決める式
     次の瞬間における変数2の値を決める式
     ...
     (式の順番は適当でよい)
  LTLSEPC 仕様1   (CTL仕様を書くときは、「SPEC 仕様1」と書く)
  LTLSEPC 仕様2
  ...
     (仕様の順番は適当でよいが、その順番にモデル検査が実行され
     出力がでてくる)
  ----------------------------------------------------

* モデルの1つの状態は、「各変数がどういう値を取るか」で決まる。

   ex1.smv では、

      request変数が TRUE か FALSE か、
      status 変数が ready  か busy か、

  なので、合計で4通りの状態がある。

      状態1. request=FALSE, status=ready
      状態2. request=FALSE, status=busy
      状態3. request=TRUE, status=ready
      状態4. request=TRUE, status=busy

* モデルの「遷移」(transition、1つの状態から次の状態への移動)は、
  ASSIGN以下の文で決まる。これは、「次の状態における変数がどうなる
  か」を記述したものである。

  初期値 
     init(status) := ready;
  次の状態での値 
     next(status) :=  ...

* 場合分けの式は case で書く。
      case
        B1: busy;
        B2: {ready,busy};
      esac;
    ここで B1, B2 は boolean 型の式である。

* 変数の値は、1つとは限らない。つまり、
  複数の状態を1度にあらわしたいことがあるので、
  その場合は集合を使う。

     next(status) = {ready,busy};

* LTL の仕様は LTLSPEC というキーワードの後に書く。

   G, F, X, (..U..)   時相論理の記号
   ->  ならば
   &   かつ
   |   または
   !   でない

   原子命題は、真偽値を取る変数そのものや、等式など。
       boolean型の変数は、それ単独で論理式になる。
          たとえば、request
       等式は、論理式になる。
          たとえば、status=busy や request

* CTL の仕様は SPEC というキーワードの後に書く。
   AG, AF, EG, EF, AX, EX, A[..U..], E[..U..]


* case 文がわかりにくいようなので、補足する。

  next(x) := 
    case
      e1: a1;
      e2: a2;
      e3: a3;
      TRUE: b;
    esac;

  このようなcase式では、e1,e2,e3 は真理値(TRUE か FALSE)を
  取る式であり、next(x) の値は、

     もし、今の瞬間の e1 の値が TRUE なら、a になり、
     そうでなくて、もし、今の瞬間の e2 の値が TRUE なら、a2 になり、
     そうでなくて、もし、今の瞬間の e3 の値が TRUE なら、a3 になり、
     そうでなければ、b になる。

  ということを表している。
  
  最後の TRUE: b; という部分は、C言語の switch 文でいうところの
  default のケースに相当する。

  上記のように、case式の中身は上から順番に処理されることに注意されたい。