Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
-------------------------- MODULE DullReservation --------------------------
EXTENDS Naturals, FiniteSets
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100
----
Reserve(seatCount) ==
/\ Cardinality(UNION reservations) + seatCount <= 70PercentTrainOccupation
/\ \E seats \in SUBSET 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
=============================================================================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment