Understanding Diameter in TLC

[thisismy...@gmail.com]

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

[Ashish Negi]

This problem is interesting because TLCGet("level") < 3 assertion never fails though I can use TLC to generate more than 3 error trace steps.

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

[thisismy...@gmail.com]

I synced up with Markus Kuppe offline. Thanks Markus for explaining the issue here.

TLCGet("level") is not same as steps that we have reached in state space exploration.

Diameter=2 is the effect of how TLC explores the state space (it doesn't "execute" the spec), which causes the spec to have a diameter of two.  TLC explores the state graph breadth first and not by generating each behavior individually

The Init predicate defines the set of initial states to be all states except those where Fast # Slow.  In other  words, the states excluded by Init are those where Done = TRUE.  Once TLC has generate the initial states and evaluates the next-state relation, it only generate states with Done = TRUE.  We can see this is you visualize the state space.  There is no state with Done = TRUE that is not a successor of an initial state.

See image 1.

If we change Init s.t it only defines a particular states, i.e. F=3/\S=1 for N=4,  TLC generates the state graph below that has a higher diameter. See image 2