[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/23b85ae8-4dc3-424c-9efd-eb041e636b88n%40googlegroups.com.