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