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

*From*: "thisismy...@xxxxxxxxx" <thisismyidashish@xxxxxxxxx>*Date*: Mon, 23 Nov 2020 20:42:22 -0800 (PST)*References*: <23b85ae8-4dc3-424c-9efd-eb041e636b88n@googlegroups.com> <CAMo8VbG6x6ng-0A_joDDnhPbqc28RVLK44dbrunhL9azwLHWUA@mail.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

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.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+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**

**Attachment:
image_2.png**

**References**:**[tlaplus] Understanding Diameter in TLC***From:*thisismy...@xxxxxxxxx

**Re: [tlaplus] Understanding Diameter in TLC***From:*Ashish Negi

- Prev by Date:
**[tlaplus] Re: Specification as part of an agile software delivery process** - Next by Date:
**Re: [tlaplus] Finding Inductive Invariants using TLC and Proving it using TLAPS** - Previous by thread:
**Re: [tlaplus] Understanding Diameter in TLC** - Next by thread:
**[tlaplus] Specification as part of an agile software delivery process** - Index(es):