Thanks a lot. That solves the problem.
在 2017年9月23日星期六 UTC-4上午2:45:50，Stephan Merz写道：
Hello,
F ~> G is a well-formed formula only when F and G are temporal formulas (including state predicates), so your formula is not syntactically valid. You'd have to write
\A n \in 1 .. 12 : msg=n ~> msg=-1
In more complicated situations you may have to record additional state in order to be able to identify which action took place.
Regards,
Stephan
> On 22 Sep 2017, at 22:04, ross...@xxxxxxxxx wrote:
>
> 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)
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.