[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
State-constraints and liveness
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)
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.