Skip to content

Instantly share code, notes, and snippets.

@sadraskol

sadraskol/LessDullReservation.tla

Created November 12, 2020 21:05
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save sadraskol/f47a858d340f841ad7096f10419bc30a to your computer and use it in GitHub Desktop.
Save sadraskol/f47a858d340f841ad7096f10419bc30a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
LessDullReservation.tla
-------------------------- 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