モデルチェッカ.NuSMVの勉強をしています.
他の人の書いたコードを読んで気になった所等のメモを残します.

文法

case

条件を書いて,コロンの後ろに条件を満たす場合の値を書く.
num ".." numで範囲指定もできる

next(state) :=
  case
    var = 0       : 1; -- var=0の時,stateを1に
    var in  1..10 : 2; -- varが 1〜10の時,stateを2に
    var in 11..20 : 3; -- varが12〜20の時,stateを3に
    1             : 0; -- otherwise 0
  esac;

な感じ.

ツール

elisp SMV-mode

ここから取ってくる.
emacsで予約語等がカラーで表示されて,少し幸せになれる.