EXTENDS Integers,
TLC \* for debugging
CONSTANTS N
VARIABLES Fast, Slow, Done
TypeOK ==
/\ Fast \in 1..N
/\ Slow \in 1..N
/\ Done \in {TRUE, FALSE}
Init ==
/\ Fast \in 1..N
/\ Slow \in 1..N
/\ Done = FALSE
\* different starting position
/\ Fast # Slow
MovePointers ==
/\ Done = FALSE
/\ Fast' = (Fast + 2) % N
/\ Slow' = (Slow + 1) % N
/\ Done' = (Fast' = Slow')
/\ UNCHANGED <<N>>
Next ==
MovePointers
\* If we are done, hare = tortoise
DetectCycle ==
IF Done = TRUE
THEN Fast = Slow \* make it # to see cycle detected
ELSE Fast # Slow
\* Failure of this invariant shows TLC ran it for cycle of size 42
RunsFor42 ==
IF Done = TRUE
THEN Fast # 42
ELSE 1 = 1
\* Failure of this invariant shows TLC ran it for numbers far apart.
LongCycle ==
IF Done = FALSE
THEN Fast < Slow + 20
ELSE 1 = 1
\* stop after levels/step
-- This invariant never fails
StopTLC ==
TLCGet("level") < 3