状態遷移を表現するように変更。 open util/ordering[State] as so /* 4日で学ぶモデル検査 システムα 仕様： 変数a 0->1 1->2 2->0と繰り返して変化する。 ただしb=1のときは次の時点でもその値を保ち変化しない。 初期状態は0とする。 変数b 0->1 1->2 2->…

「4日で学ぶモデル検査」より。 愚直にモデリングしてるだけで、これではスイッチがOn,Offされることを 確認できない・・・ open util/ordering[State] as so /* 4日で学ぶモデル検査 システムα */ abstract sig Switch {} one sig On,Off extends Switch {}…