-------------------------- MODULE DullReservation -------------------------- | |
EXTENDS Naturals, FiniteSets | |
VARIABLE reservations | |
Coaches == { "A", "B" } | |
SeatNumbers == 1..10 | |
Seats == Coaches \X SeatNumbers | |
70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100 | |
ReservedSeats == UNION reservations | |
FreeSeats == Seats \ ReservedSeats | |
---- | |
SameCoach(seats) == \E someCoach \in Coaches: \A <<coach, _rr>> \in seats: coach = someCoach | |
Reserve(seatCount) == | |
/\ Cardinality(UNION reservations) + seatCount <= 70PercentTrainOccupation | |
/\ \E seats \in SUBSET FreeSeats: | |
/\ SameCoach(seats) | |
/\ Cardinality(seats) = seatCount | |
/\ reservations' = reservations \union {seats} | |
---- | |
Init == reservations = {} | |
Next == \E seatCount \in 1..Cardinality(Seats): Reserve(seatCount) | |
---- | |
TypeCheck == reservations \in SUBSET SUBSET Seats | |
AtMost70PercentTrainOccupation == Cardinality(UNION reservations) <= 70PercentTrainOccupation | |
AllReservationAreInTheSameCoach == \A reservation \in reservations: SameCoach(reservation) | |
SeatsCanBeReservedOnce == \A seat \in Seats: | |
Cardinality({reservation \in reservations: seat \in reservation}) <= 1 | |
============================================================================= |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment