Skip to content

Instantly share code, notes, and snippets.

@sadraskol

sadraskol/FirstSpecification.tla

Created December 16, 2020 10:13
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/e42a7e62550694fc90f46083e205b255 to your computer and use it in GitHub Desktop.
Save sadraskol/e42a7e62550694fc90f46083e205b255 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
FirstSpecification.tla
-------------------------- MODULE FirstSpecification --------------------------
EXTENDS Naturals
VARIABLE reservations
Coaches == { "A", "B" }
SeatNumbers == 1..10
Seats == Coaches \X SeatNumbers
----
Reserve == reservations' = reservations \union {{<<"A", 1>>}}
----
Init == reservations = {}
Next == Reserve
=============================================================================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment