Re: [tlaplus] Asserting an action leads to another action as a property

[Stephan Merz <stepha...@xxxxxxxxx>]

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