# Re: [tlaplus] Re: Temporal prop is violated, but error-trace doesn't show it

Jay, thanks, I believe that was the problem.

> On Feb 12, 2019, at 7:43 PM, Jay Parlar <parlar@xxxxxxxxx> wrote:
>
> Philip,
>
> When you say
>
> > I configured the model with 2 symmetrical model values for X (x1, x2).
>
> Do you mean that in the model checker you explicitly marked the set as a symmetry set?
>
> When checking liveness properties, you are not permitted to use symmetry sets. Per the "Symmetry" section of the built-in docs:
>
> "Symmetry sets should not be used when checking liveness properties.  Doing so can make TLC fail to find errors, or to report nonexistent errors."
>
> At least in my build of TLA+, there's also a warning in the model checker when I have a temporal property being checked combined with a set being marked as a symmetry set.
>
> Jay P.
>
>
> On Tuesday, 12 February 2019 22:21:45 UTC-5, Philip White wrote:
> Hello,
>
> I’d like to express a temporal property where, once P is true, P stays true forever, and I want TLC to find me a counterexample. I’m having a problem doing this, and I’m not sure if it’s with me or with TLA Toolbox.
>
> I wrote a minimal test spec that exhibits the problem:
>
> -------------------------------- MODULE demo --------------------------------
> CONSTANT X
>
> Init == readable \in [X -> {FALSE}]
>
> Next == \E x \in X:
>
> ------------------
>
>     \A x \in X:
>
> =============================================================================
>
> I configured the model with 2 symmetrical model values for X (x1, x2).
>
> When I run this, I get non-deterministic behavior from TLC that falls in one of these categories:
> 1) a legitimate violation in a minimum number of steps
> 2) a legitimate violation with unnecessary steps
> 3) a claimed violation but the error trace does not show the violation.
>
> I assume #2 is fine — TLC may not find the minimum path to the violation. Please correct me if I’m wrong.
>
> But #3 concerns me. Here’s an example such run:
>
> State 1 (initial): both values of readable are FALSE.
> State 2: x1 becomes TRUE.
> State 3: x2 becomes TRUE.
> State 4: stuttering.
>
> Why is this happening?
>
> (My own hypothesis: Combined with the non-deterministic behavior, it feels like a race condition, with the error trace showing some successful execution that mistakenly overwrote the failed execution before the Toolbox could show it to me.)
>
> When I reduce my spec to just one value (readable is just a boolean) that alternates between true and false, I cannot reproduce case #3.
>
> Thanks for any insights.
>
> —
> Philip
>
> --
> 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.

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