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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Tue, 2 Apr 2019 17:18:28 +0200*References*: <3820dc61-fe5b-4f5d-b82a-ac3a65de140a@googlegroups.com> <1d166954-84ef-4f6c-9261-3b3b94f1b927@googlegroups.com> <6f67ddb2-36f5-46c7-815f-26ee4cdc3fe2@googlegroups.com> <0ecffbef-cc96-4a44-90af-673fe1983522@googlegroups.com> <7263516e-6b52-42dc-9546-8bf1e20058cc@googlegroups.com> <ef421f7d-3e10-4150-b69f-7f373cecff56@googlegroups.com> <8f1f1269-993d-4d86-9c41-78ff32adb2e8@googlegroups.com>

Stepping back a bit, it appears to me that you'd like to check a property of the form A ~> B where A and B are both actions. Such a formula is not syntactically well-formed in TLA (although it is indeed stuttering invariant). TLA allows such a formula to be written only if A and B are temporal formulas, including state predicates. You can work around this limitation by adding variables done_A and done_B that are initialized to FALSE and set to true whenever A and B happen. Then check the property done_A ~> done_B (Since your actual actions take parameters the details are a bit more complicated and you may need to use functions but I think you get the idea.) In practice, you won't actually need to introduce these helper variables because the system state probably already contains enough information to tell you when A and B occurred. The overall idea is to replace the actions by suitable state predicates. Hope this helps, Stephan
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**:**Re: [tlaplus] Re: [noob] Liveness property not violated as expected***From:*Michael Chonewicz

**References**:**[tlaplus] [noob] Liveness property not violated as expected***From:*Michael Chonewicz

**[tlaplus] Re: [noob] Liveness property not violated as expected***From:*Jay Parlar

**[tlaplus] Re: [noob] Liveness property not violated as expected***From:*Michael Chonewicz

**[tlaplus] Re: [noob] Liveness property not violated as expected***From:*Jay Parlar

**[tlaplus] Re: [noob] Liveness property not violated as expected***From:*Michael Chonewicz

**[tlaplus] Re: [noob] Liveness property not violated as expected***From:*Jay Parlar

**[tlaplus] Re: [noob] Liveness property not violated as expected***From:*Michael Chonewicz

- Prev by Date:
**[tlaplus] Re: [noob] Liveness property not violated as expected** - Next by Date:
**Re: [tlaplus] Fumbling Through TLA+** - Previous by thread:
**[tlaplus] Re: [noob] Liveness property not violated as expected** - Next by thread:
**Re: [tlaplus] Re: [noob] Liveness property not violated as expected** - Index(es):