Skip to content

Instantly share code, notes, and snippets.

@sadraskol
Last active November 12, 2020 21:04
Show Gist options
  • Select an option

  • Save sadraskol/d5615541d766b66f10888faf17263cda to your computer and use it in GitHub Desktop.

Select an option

Save sadraskol/d5615541d766b66f10888faf17263cda to your computer and use it in GitHub Desktop.
-------------------------- 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