| -------------------------- MODULE LessDullReservation -------------------------- | |
| EXTENDS Naturals, FiniteSets | |
| VARIABLE reservations | |
| Coaches == { "A", "B" } | |
| SeatNumbers == 1..10 | |
| Seats == Coaches \X SeatNumbers | |
| 70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100 | |
| ---- | |
| Reserve == /\ Cardinality(UNION reservations) < 70PercentTrainOccupation | |
| /\ \E singleSeat \in Seats: reservations' = reservations \union {{singleSeat}} | |
| ---- | |
| Init == reservations = {} | |
| Next == Reserve | |
| ---- | |
| TypeCheck == reservations \in SUBSET SUBSET Seats | |
| AtMost70PercentTrainOccupation == Cardinality(UNION reservations) <= 70PercentTrainOccupation | |
| ============================================================================= |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment