付録A.5 の小さなケーススタディの鉄道のスイッチングです。 かなり久しぶりになってしまいました。スイッチングポリシーのチェックをやってみました。 現在 Train が占有している Segment へ入る信号を全て侵入禁止にするという厳しい条件でやってみました…

付録A.5 の小さなケーススタディの鉄道のスイッチングです。 A.5.2 (c), (d), (e), (f) open util/ordering [TrainState] sig Segment { next: lone Segment, overlaps: some Segment } sig Train {} sig TrainState { on: Train -> one Segment, occupied: …