Hi Chris,
unfortunately, TLC doesn't check arbitrary temporal properties. "Implied temporal formulas" are restricted to "simple temporal formulas", which may only contain action sub formulas of the form WF_v(A), SF_v(A), []<><A>_v or <>[][A]_v (cf. Section 14.2.4, AFAIK this is still true of current versions of TLC). Your subformula HenceforthStuttering is even simpler, but not a "simple temporal formula" in that sense.
I'd suggest that you rewrite your property so that TLC will accept it. For example, try
Spec /\ []<><TRUE>_vars => Liveness
(for your original definition of liveness). In this way, the liveness property will only be evaluated over behaviors that do not end in infinite stuttering.
However, checking liveness properties in the presence of state constraints can be really tricky because the specification may not assert what you think it does. In particular, see section 14.3.5 of the TLA+ book.
Hope this helps,
Stephan
I'm trying to use TLC to check liveness properties for the first time.
My liveness property is a simple leads-to formula:
Liveness == \A id \in Ids : MyProperty(id) ~> SomeOtherProperty(id)
TLC finds counter-examples in which the (temporal) antecedent is satisfied (for some id in some state), but the consequent is never satisfied because the behavior generated by TLC is artificially truncated -- i.e. ends with infinite stuttering -- because of the state-constraint. As the counter-example ends in infinite stuttering, I tried weakening the liveness property to allow that:
HenceforthStuttering == [] UNCHANGED AllVars \* all future steps don't change any variables
Liveness == \A id \in Ids : MyProperty(id) ~> (\/ SomeOtherProperty(id)
\/ HenceforthStuttering) But that's not valid TLA+ because the definition of HenceforthStuttering is not a legal TLA+ formula. The toolbox says:
Parse error: [] followed by action not of the form [A]_v
So I tried:
HenceforthStuttering == [][UNCHANGED AllVars]_AllVars \* all future steps don't change any variables
That parses, but TLC now fails immediately with:
Temporal formulas containing actions must be of forms <>[]A or []<>A.
What am I missing? I did wonder if, rather than weakening the liveness property, there might be a way to change the state-constraint such that it wouldn't cause the liveness property to be artificially violated. But I don't currently see how to do that.
many thanks,
Chris
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
To unsubscribe from this group, send email to tlaplus+u...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus?hl=en.
|