Copy the following tiny text, either by
clicking on the
Copy
button below it, or by your usual method of copying
text.
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
Then paste the text into the module editor as
the body of specification SimpleProgram
.