Skip to content

Instantly share code, notes, and snippets.

@kbastani

kbastani/tla.tla

Created February 24, 2017 05:38
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 kbastani/9fca0e4e172d9ad2505cd3e0c5b4c067 to your computer and use it in GitHub Desktop.
Save kbastani/9fca0e4e172d9ad2505cd3e0c5b4c067 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
tla.tla
VARIABLE clock
Init == clock \in {0, 1}
Tick == IF clock = 0 THEN clock' = 1 ELSE clock' = 0
Spec == Init /\ [][Tick]_<<clock>>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment