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

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.