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