学祭用にエレベーターシステムの状態遷移をNuSMVで記述している。
最終的には6階建ての建物でエレベータは2台、ユーザーは複数人を想定している。
だが、いきなり上記のシステムを書こうとしてムリと判断したので、エレベータ1台でユーザー1人で記述。
そして今日構文エラー等が取れて動くようになった。
学祭までにエレベータやユーザーをモジュールに分割して楽に設定できるようにするのが目標。
ちなみにレベータ1台でユーザー1人での状態数は単純に計算すると、
ユーザーの現在地 7 ユーザーの行き先 6 エレベーターの位置 6 エレベーターの移動状態 3 各ボタン（18個）の状態 2 各ドア（7個）の状態 4 6 * 3 * 6 * 7 * (2^18) * (4^7) = 3 246 995 275 776
3テラの状態数だが、使われる状態はもっと少ないからなんとかなるが、エレベータとユーザーが増えると・・・。
