module bart
sig Seg {next, overlaps: set Seg}
fact {all s: Seg | s in s.overlaps}
fact {all s1, s2: Seg | s1 in s2.overlaps => s2 in s1.overlaps}
sig Train {}
sig GateState {closed: set Seg}
sig TrainState {on: Train ->! Seg, occupied: set Seg}
fact {all x: TrainState |
x.occupied = {s: Seg | some t: Train | t.(x.on) = s}
}
fun Safe (x: TrainState) {all disj ta, tb: Train | ta.(x.on) !in tb.(x.on).overlaps}
fun MayMove (g: GateState, x: TrainState, movers: set Train) {
no movers.(x.on) & g.closed
}
fun TrainsMove (x, x': TrainState, movers: set Train) {
all t: movers | t.(x'.on) in t.(x.on).next
all t: Train - movers | t.(x'.on) = t.(x.on)
}
fun GatePolicy (g: GateState, x: TrainState) {
-- x.occupied.overlaps.~next in g.closed
x.occupied.~next in g.closed
all s1, s2: Seg | some s1.next & s2.next.overlaps => sole (s1+s2 - g.closed)
}
fact {all s: Seg | sole s.next}
assert PolicyWorks {
all x, x': TrainState, g: GateState, movers: set Train |
{MayMove (g, x, movers)
TrainsMove (x, x', movers)
Safe (x)
GatePolicy (g, x)
} => Safe (x')
}
-- has counterexample in scope of 3
check PolicyWorks for 3