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

*From*: david streader <davidistreader@xxxxxxxxx>*Date*: Wed, 1 May 2019 16:21:07 -0700 (PDT)*References*: <1fa1392c-0ec5-4d9e-b339-f7d1617c5117@googlegroups.com> <8147e0fe-bd5c-4653-8523-ef729b528834@googlegroups.com> <af589ad5-3cf3-4899-8be3-0c74d139b1d8@googlegroups.com> <a0489306-2ba7-4dbe-a7f5-ee1be6faaff3@googlegroups.com>

On Wednesday, 1 May 2019 23:42:30 UTC+12, Jay Parlar wrote:

Strong fairness means an action which is enabled infinitely often will eventually be taken. So it can be disabled and renabled over and over, but as long as it always gets renabled, then it will eventually be taken. Which is essentially what you said.

But if, for example, an action is enabled infinitely often and there are _two_ ways to step out of it (because of non determinism in the action), you are NOT guaranteed that both ways out will eventually be taken.

To guarantee that, you’d have to further subdivide the action, and have strong fairness on the subdivisions.

As an example,

Foo == /\ x = 1

/\ \E y \in {2, 3} : x’ = y

If x is repeatedly toggled between 0 and 1 by some other action, and you have strong fairness on Foo, then you’re guaranteed that the Foo action will eventually take place. But it taking place by always choosing 2 would be valid, there’s no guarantee that eventually it would assign 3 to x in the next state.

My guess is that your PlusCal is being turned into actions which contain non-determinism, and TLC is showing you a trace where only one side of the non-determinism ever occurs.

Many thanks for you time and effort.

I have gutted the specification so it is a lot smaller but some what artificial. Run TLC with a model with CORRUPT_DATA a model value and Message <<9>> plus the property Fin

The problem is, the state graph shows that from the initial state **two distinct steps** are possible. Hence the nondeterminism you mentioned does not apply. Yet with Spec the we get a temporal error with trace looping back to the initial state. But with MySpec == Spec /\ SF_vars(sData/\ pc'["send"]="ssd") the error disappeared hence TLC behaves as if these **two steps are not distinct**.

I have constructed many small examples for teaching and the state graph has so far always agreed with TLC. Consequently I have been using it to help analyses the liveness behaviour of the TLA+ specs.

In this example the state graph and TLC disagree.

Checking the spec by hand I find that I agree with the state Graph and disagree with TLC.

thanks again. david

I hope this helps!

Jay P.

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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.

Visit this group at https://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/d/optout.

**Attachment:
hackStateGraph.png**

**Attachment:
abpHack.tla**

**Follow-Ups**:**[tlaplus] Re: problems debugging liveness errors.***From:*Jay Parlar

**References**:**[tlaplus] problems debugging liveness errors.***From:*david streader

**[tlaplus] problems debugging liveness errors.***From:*Jay Parlar

**[tlaplus] Re: problems debugging liveness errors.***From:*david streader

**[tlaplus] Re: problems debugging liveness errors.***From:*Jay Parlar

- Prev by Date:
**Re: [tlaplus] Dealing with a `pc` variable in refinement?** - Next by Date:
**Re: [tlaplus] Dealing with a `pc` variable in refinement?** - Previous by thread:
**[tlaplus] Re: problems debugging liveness errors.** - Next by thread:
**[tlaplus] Re: problems debugging liveness errors.** - Index(es):