# [tlaplus] Understanding Diameter in TLC

Hi
Can someone explain why is diameter of model state space is 2 with below spec ?
even though i give constant N = 50

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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.