Skip to content

Instantly share code, notes, and snippets.

@davebryson

davebryson/counter.tla

Created April 30, 2024 10:45
Show Gist options
  • Save davebryson/367013ce035a2780beacdb61df48cec5 to your computer and use it in GitHub Desktop.
Save davebryson/367013ce035a2780beacdb61df48cec5 to your computer and use it in GitHub Desktop.
Download ZIP
Counter.tla
Raw
counter.tla
---- MODULE counter ----
EXTENDS Naturals
CONSTANT Limit
VARIABLE counter
Init == counter = 1
Terminates == counter = Limit
Next ==
/\ counter < Limit
/\ counter' = counter + 1
Spec ==
/\ Init
/\ [][Next]_counter
(* Invariants *)
TypeOk ==
/\ Limit \in Nat
/\ Limit > 0
WithinLimit == counter <= Limit
(* Propeties *)
\* Safety
AlwaysIncreases == [][counter' > counter]_counter
\* Liveliness
\* Eventually it hits the limit and stays there
ReachLimit == <>[]Terminates
====
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment