HiCan someone explain why is diameter of model state space is 2 with below spec ?even though i give constant N = 50EXTENDS 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 a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/StDY-tKh3Ls/unsubscribe.
To unsubscribe from this group and all its topics, 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.