モデルチェッカ.NuSMVの勉強をしています.
他の人の書いたコードを読んで気になった所等のメモを残します.
条件を書いて,コロンの後ろに条件を満たす場合の値を書く.
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;
な感じ.
ここから取ってくる.
emacsで予約語等がカラーで表示されて,少し幸せになれる.