Skip to content

Instantly share code, notes, and snippets.

@lemmy
Last active December 24, 2022 04:28
Show Gist options
  • Save lemmy/a2f598aceea5b74a2eaa811d35c53573 to your computer and use it in GitHub Desktop.
Save lemmy/a2f598aceea5b74a2eaa811d35c53573 to your computer and use it in GitHub Desktop.
INIT Init
NEXT Next
INVARIANT Inv
---- MODULE Simple ----
VARIABLE v, n
Init ==
/\ v \in {TRUE, FALSE}
/\ n = 0
Next ==
/\ v' \in {TRUE, FALSE}
/\ n' = n + 1
Inv ==
/\ n = 3
/\ v = TRUE
====================
@lemmy
Copy link
Author

lemmy commented Dec 24, 2022

Counterexample ends in a state s.t. n = 3 /\ v = FALSE.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment