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

Re: [tlaplus] Understanding Diameter in TLC



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



On Friday, 20 November 2020 at 01:37:08 UTC-8 thisismy...@xxxxxxxxx wrote:
This problem is interesting because TLCGet("level") < 3 assertion never fails though I can use TLC to generate more than 3 error trace steps.

On Thu 19 Nov, 2020, 3:09 PM thisismy...@xxxxxxxxx <thisismy...@xxxxxxxxx wrote:
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 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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/23b85ae8-4dc3-424c-9efd-eb041e636b88n%40googlegroups.com.

--
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/44891dc0-72b5-4cb6-8aeb-34f0f9293700n%40googlegroups.com.

Attachment: image_1.png
Description: PNG image

Attachment: image_2.png
Description: PNG image