Skip to content

Instantly share code, notes, and snippets.

@kbastani

kbastani/tla.tla

Created Feb 24, 2017
Embed
What would you like to do?
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