sample alloy model
model Bart {
domain {Segment, Gate, Train}
state Segments {
succ, overlaps : Segment -> Segment
gate : Segment! -> Gate?
partition Open, Closed : Gate
on : Train -> Segment !
}
cond Safety {all s | sole s.overlaps.~on}
inv Policy {all s | sole (s.conflicts + s).gate & Open}
op TrainsMove (ts : Train) {
all t : ts | t.on' in t.on.succ
no (ts.on.gate & Closed)
all t : Train - ts | t.on = t.on’ }
assert PolicyWorks {all t | TrainsMove (t) && Safety -> Safety'}