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

*From*: Philip White <philip@xxxxxxxxxxxxx>*Date*: Tue, 12 Feb 2019 19:21:39 -0800

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.

**Follow-Ups**:

- Prev by Date:
**[tlaplus] Re: Seeking advice about principles of translating TLA+ spec to real code** - Next by Date:
**[tlaplus] Re: Temporal prop is violated, but error-trace doesn't show it** - Previous by thread:
**[tlaplus] Seeking insights on how to translate TLA+ spec into real code** - Next by thread:
**[tlaplus] Re: Temporal prop is violated, but error-trace doesn't show it** - Index(es):