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.