モデルチェッカ．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で予約語等がカラーで表示されて，少し幸せになれる．
