Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
-------------------------- MODULE LessDullReservation --------------------------
EXTENDS Naturals, FiniteSets
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
70PercentTrainOccupation == (70 * Cardinality(Seats)) \div 100
----
Reserve == /\ Cardinality(UNION reservations) < 70PercentTrainOccupation
/\ \E singleSeat \in Seats: reservations' = reservations \union {{singleSeat}}
----
Init == reservations = {}
Next == Reserve
----
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