[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Asserting an action leads to another action as a property
I am working on a Spec where two actions on some messages should happen in pair (other actions can happen in between). The following is a simplified version of the system.
The system doesn't stop (WF_<<msg>>(Next)) and I want to check the property that for any m, if ActionA(m) happens, eventually ActionB(m) will happen.
I plan to check it with the expression LivenessProperty, but it seems TLA+ does not allow that. Is it possible to express LivenessProperty as a valid temporal formula? Or do I have to use state predicates?
EXTENDS Naturals, Reals
Init == msg = -1
ActionA(m) == /\ msg = -1
/\ msg' = m
ActionB(m) == /\ msg = m
/\ msg' = -1
Next == \E n \in (1 .. 12) : \/ ActionA(n)
Spec == Init /\ [Next]_msg /\ WF_<<msg>>(Next)
LivenessProperty == \A n \in (1 .. 12) : ActionA(n) ~> ActionB(n)