AlmostThirdRuleReservation.tla

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

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

----

ReservationCountFor(coach) == Cardinality({<<c, _i>> \in ReservedSeats: c = coach})

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)

=============================================================================