| Your fairness condition requires that some message must be received as long as there is some message in the network. If you want to say that any message in the network must eventually be received, you have to write something like
\A m \in Response : WF_vars(RcvResponse(m))
where Response is the (constant) set of all possible response messages that may exist at some point. Of course, for TLC to be able to handle that condition, this should be a finite (and not too big) set.
Stephan
Hi there,
I'm modeling the network as a set "network" and I add and remove messages from this set. There is an action called "RcvResponse(m)" that removes a message "m", whose type is "response". I am trying to set a fairness condition for this action, something like: WF_vars(\E m \in network : RcvResponse(m)) But when checking liveness I got this problem: it might be possible that a message "m" remains in the network and is never removed, because new messages with the same type "response" can be added, thus creating a cycle. How can I guarantee that every message once added will be eventually removed (using the fairness conditions)? Thanks. Regards, Pedro -- Pedro Yuri Arbs Paiva Engenheiro Eletrônico
Instituto Tecnológico de Aeronáutica (T-16)
(+55) 12 98106-4129
--
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.
|