22 lines
600 B
Text
22 lines
600 B
Text
--------------------------- MODULE SimpleProgram_ch8 ---------------------------
|
|
|
|
EXTENDS Integers
|
|
VARIABLES i, pc
|
|
|
|
Init == (pc = "start") /\ (i = 0)
|
|
|
|
Pick == /\ pc = "start"
|
|
/\ i' \in 0..1000
|
|
/\ pc' = "middle"
|
|
|
|
Add1 == /\ pc = "middle"
|
|
/\ i' = i + 1
|
|
/\ pc' = "done"
|
|
|
|
Next == Pick \/ Add1
|
|
|
|
Spec == Init /\ [][Next]_<<pc, i>>
|
|
=============================================================================
|
|
\* Modification History
|
|
\* Last modified Mon Feb 03 15:18:32 CET 2025 by fredericmarand
|
|
\* Created Mon Feb 03 09:48:31 CET 2025 by fredericmarand
|