[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Fairness condition for messages

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.


Pedro Yuri Arbs Paiva
Engenheiro Eletrônico
Instituto Tecnológico de Aeronáutica (T-16)
(+55) 12 98106-4129