| The error message says: Non-constant TAKE, WITNESS, or HAVE for temporal goal so this restriction was an explicit design decision. (Not sure if it is documented anywhere ...) Even with the explicit SUFFICES construct, your proof is likely to be doomed: at some point you'll have to apply temporal logic reasoning (the PTL method), and as a rule of thumb, in all temporal steps the context should only contain "boxed" assumptions, i.e., all assumptions A should be equivalent to []A. This is true for constant formulas A, formulas []A, <>[]A, WF_v(A) etc., but not for Spec, which will contain an initial state predicate. If you continue your proof attempt, you'll find that PTL warns about "non-[] assumption" and fails. Invariant proofs should be written in the form THEOREM Spec => []Invariant <1>1. Init => Invariant <1>2. Invariant /\ [][Next]_v => Invariant' <1>. QED BY <1>1, <1>2, PTL DEF Spec In particular, the context of the QED step is empty, so all its assumptions are "boxed". 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/30EB506E-5FC5-4B2C-B21D-EB577C63BEA6%40gmail.com. |