Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
-------------------------- MODULE SuccessiveReservation --------------------------
EXTENDS Naturals, FiniteSets, Sequences, TLC
VARIABLE reservations
Coaches == 1..2
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100
70PercentCoachOccupation == (70 * Cardinality(SeatNumbers)) \div 100
ReservedSeats == UNION reservations
FreeSeats == Seats \ ReservedSeats
----
SameCoach(seats) == \E someCoach \in Coaches: \A <<coach, _i>> \in seats: coach = someCoach
\* < operator for pairs
a \prec b == \/ a[1] < b[1]
\/ a[1] = b[1] /\ a[2] < b[2]
SequenceSeatsStrategy(seats, count) ==
/\ Cardinality(seats) = count
/\ SameCoach(seats)
/\ ~(\E s \in FreeSeats \ seats: \E t \in seats: s \prec t)
/\ reservations' = reservations \union {seats}
----
Reserve(seatCount) ==
/\ Cardinality(UNION reservations) + seatCount <= 70PercentTrainOccupation
/\ \E seats \in SUBSET FreeSeats: SequenceSeatsStrategy(seats, seatCount)
----
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