Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
-------------------------- MODULE DullReservation --------------------------
EXTENDS Naturals
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
----
Reserve == reservations' = reservations \union {{<<"A", 1>>}}
----
Init == reservations = {}
Next == Reserve
----
TypeCheck == reservations \in SUBSET SUBSET Seats
=============================================================================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment