CorrectReservation.tla

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

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