| Alloy
model: declarations |
|
|
|
|
|
|
|
|
|
|
| model
Bart { |
|||||||||
| domain {Segment, Connector, Gate, Train} |
|||||||||
| state Segments { |
|||||||||
| from, to: Segment -> Connector! |
|||||||||
| overlaps: Segment -> Segment |
|||||||||
| gate: Segment! -> Gate? |
|||||||||
| partition Open, Closed: Gate |
|||||||||
| on: Train -> Segment! |
|||||||||
| succ: Segment -> Segment |
|||||||||
| conflicts: Segment -> Segment |
|||||||||
| } |
|||||||||
