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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 29 Nov 2023 09:32:45 +0100*References*: <70c9b443-a61d-4c1e-9bde-ab7304339361n@googlegroups.com>

The class of temporal formulas that TLC can handle is described in section 14.2.4 of Specifying Systems. In particular, your quantifiers should range over constant-level expressions, not over the variables O and S. Looking at your specification, I see several antipatterns: - O and S are declared as variables but do not seem to be changed by the actions. In contrast, you write formulas such as \E o \in O: \/ o.owner = 0 => o' = [o EXCEPT !.participate = o.oid] Here, the value of O in the successor state is not determined by the action, but you attempt to modify o. Since o is introduced using the quantifier \E, it is a constant-level _expression_, so o' = o, and assuming that o.oid is different from o.participate, the formula is simply contradictory. (Note also that the lone disjunction symbol is superfluous.) - The property that you are trying to verify is of the form \E vars : F => <>G so it is true if F is false in the initial state for some value of vars. Looking at the initial condition, we have o1 \in O, s1 \in S, and o1.oid \notin s1.cnfl, which makes the property trivially true. I encourage you to start with a small specification and to validate that specification using simulation and checking invariants that you expect to be true and that you expect to be false before starting to verify liveness properties for larger specifications. 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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3EA4D780-39A9-4FBE-8618-F3F3500E78A2%40gmail.com. |

**Follow-Ups**:**Re: [tlaplus] How to fix "TLC cannot handle the temporal formula"?***From:*myeongjin son

**References**:**[tlaplus] How to fix "TLC cannot handle the temporal formula"?***From:*myeongjin son

- Prev by Date:
**[tlaplus] How to fix "TLC cannot handle the temporal formula"?** - Next by Date:
**Re: [tlaplus] How to fix "TLC cannot handle the temporal formula"?** - Previous by thread:
**[tlaplus] How to fix "TLC cannot handle the temporal formula"?** - Next by thread:
**Re: [tlaplus] How to fix "TLC cannot handle the temporal formula"?** - Index(es):