はぁー、「有限状態機械(FSM)」っすか。

明示的にあるいは本質的に、FSMとして表現されていない部分は、
仕様検証の対象外になるんでしょーか。疑問ばっかりですんません。