Asserting an action leads to another action as a property

[ross.y...@gmail.com]

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)

[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

> --
> 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...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Ross Yu]

Thanks a lot. That solves the problem.

在 2017年9月23日星期六 UTC-4上午2:45:50，Stephan Merz写道：