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

[Philip White <philip@xxxxxxxxxxxxx>]

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 
> VARIABLE readable 
> 
> Init == readable \in [X -> {FALSE}] 
> 
> Next == \E x \in X: 
>         readable' = [readable EXCEPT ![x] = ~@] 
> 
> ------------------ 
> 
> Prop_OnceReadableAlwaysReadable == 
>     \A x \in X: 
>         [](readable[x] => []readable[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.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.