>>36

まず、明示されてないものはチェックできないでしょうね。

また、有限状態機械では表せない場合には、
今のモデルチェッキングを超える方法が
必要でしょうね。