nuXmv

Automaton の授業の〆は、nuXmv というモデル検査システムで。元は、CMU の SMVなはずです。

マニュアルから読み始めたんですが...

　　あぁ、だめ。これは...

というわけなので、Tutorial から。でも、いかんせん、80年代からのシステムだから...

　　構文が古くさい

VHDLっぽい? あと、Tutorial は SMV のままなので、nuXmv になって何が良くなったのかわからないという問題が...

MODULE main
VAR
state : {a, b};
ASSIGN
init(state) := a;
next(state) := {a, b};
SPEC AG state=a
SPEC EG state=a
SPEC AF state=a
SPEC EF state=a
SPEC A [ state=a U state=b ]
SPEC E [ state=a U state=b ]

とかで、SPEC どうなるとかやってました。CTL ややこしい。