| Indeed, a formula such as [](A => []B) is not well-formed when A is an action. I once suggested an extension of TLA (the temporal logic underlying TLA+) in which such properties could be expressed [1], but it was never adopted. The simplest workaround is to use a state predicate expressing that A has occurred instead of the action A on the left-hand side of the implication. Perhaps your specification already allows you to identify such a predicate, otherwise you can add a history variable VARIABLE AhasOccurred HInit == Init /\ AhasOccurred = FALSE HNext == /\ Next /\ \/ A /\ AhasOccurred’ = TRUE \/ ~A /\ UNCHANGED AhasOccurred HSpec == HInit /\ [][HNext]_<<vars, AhasOccurred>> /\ … and then prove the theorem Spec => [](AhasOccurred => []B). That proof should be straightforward, the main arguments being that A establishes B and that every transition preserves B, assuming that AhasOccurred is true. It will require a suitable invariant. You may notice that this property is subtly different from the one that you wrote in that it only shows that B will be (and remain) true after A has occurred, whereas your original formula claims that B must already be true when A occurs. In my experience, the former is more frequent, but if you really want the latter, you can find a similar way to express it. 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 view this discussion visit https://groups.google.com/d/msgid/tlaplus/65EA190A-869A-4F86-A82C-8568914B3BE1%40gmail.com. |