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

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


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


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.