[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Asserting an action leads to another action as a property
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.
> On 22 Sep 2017, at 22:04, ross.y...@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...@xxxxxxxxxxxxxxxx.
> 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.