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

[Philip White <philip@xxxxxxxxxxxxx>]

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.