mirror of
https://github.com/johndoe6345789/tla_visualiser.git
synced 2026-04-25 06:05:03 +00:00
21 lines
454 B
Plaintext
21 lines
454 B
Plaintext
---------------------------- MODULE SimpleCounter ----------------------------
|
|
(* A simple counter specification for testing TLA+ Visualiser *)
|
|
|
|
EXTENDS Naturals
|
|
|
|
VARIABLE counter
|
|
|
|
Init == counter = 0
|
|
|
|
Increment == counter' = counter + 1
|
|
|
|
Decrement == counter' = counter - 1
|
|
|
|
Next == Increment \/ Decrement
|
|
|
|
Spec == Init /\ [][Next]_counter
|
|
|
|
TypeInvariant == counter \in Nat
|
|
|
|
=============================================================================
|