-------------------------- 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