Asserting an action leads to another action as a property

[ross.y...@xxxxxxxxx]

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
VARIABLES msg

Init == msg = -1

ActionA(m) == /\ msg = -1
              /\ msg' = m
ActionB(m) == /\ msg = m
              /\ msg' = -1
        
Next == \E n \in (1 .. 12) : \/ ActionA(n)
                             \/ ActionB(n)
        
Spec == Init /\ [][Next]_msg /\ WF_<<msg>>(Next)

LivenessProperty == \A n \in (1 .. 12) : ActionA(n) ~> ActionB(n)