Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
----------------------------- MODULE FinalReservation -----------------------------
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[i]: i \in DOMAIN reservations}
FreeSeats == Seats \ ReservedSeats
----
SameCoach(seats) == \E someCoach \in Coaches: \A <<coach, _i>> \in seats: coach = someCoach
ReservationCountFor(coach) == Cardinality({<<c, _i>> \in ReservedSeats: c = coach})
LeastOccupiedCoach == CHOOSE c \in Coaches: \A x \in Coaches: ReservationCountFor(c) <= ReservationCountFor(x)
LeastOccupiedCoachStrategy(seats, count) ==
/\ \A <<c, _i>> \in seats: c = LeastOccupiedCoach
/\ Cardinality(seats) = count
/\ count <= Cardinality(SeatNumbers)
/\ reservations' = Append(reservations, seats)
----
Reserve(seatCount) ==
/\ Cardinality(ReservedSeats) + seatCount <= 70PercentTrainOccupation
/\ \E seats \in SUBSET FreeSeats: SequenceSeatsStrategy(seats, seatCount)
----
Init == /\ reservations = <<>>
Next == \E seatCount \in 1..Cardinality(Seats): Reserve(seatCount)
----
TypeCheck == \A i \in DOMAIN reservations: reservations[i] \in SUBSET Seats
AtMost70PercentTrainOccupation == Cardinality(ReservedSeats) <= 70PercentTrainOccupation
AllReservationAreInTheSameCoach == \A i \in DOMAIN reservations: SameCoach(reservations[i])
SeatsCanBeReservedOnce == \A seat \in Seats:
Cardinality({i \in DOMAIN reservations: seat \in reservations[i]}) <= 1
----
ReservationCoach(reservation) == (CHOOSE seat \in reservation: TRUE)[1]
LatestReservation == reservations[Len(reservations)]
LatestReservationShouldNotHaveBeenMadeIfAnotherCoachCanReceiveItWhileKeepingUnder70PercentOccupation ==
\/ reservations = <<>>
\/ ReservationCountFor(ReservationCoach(LatestReservation)) <= 70PercentCoachOccupation
\/ ~(\E other \in Coaches: ReservationCountFor(other) + Cardinality(LatestReservation) <= 70PercentCoachOccupation)
=============================================================================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment