[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.

I'm using a state-constraint with TLC, as I described in a previous message: https://groups.google.com/d/msg/tlaplus/nfd1H-tZbe8/eCV3DNKZOicJ 

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,