11 lines
119 B
Plaintext
11 lines
119 B
Plaintext
---- MODULE Test ----
|
|
EXTENDS Naturals
|
|
|
|
VARIABLE x
|
|
|
|
Init == x = 0
|
|
Next == x' = x + 1
|
|
|
|
Spec == Init /\ [][Next]_x
|
|
====:
|