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