% All messages d are (once they have been read through action r1)
% inevitably sent through action s4, if not permanently lost (via
% internal action i).
%
% Essentially this is the same property as the one in
% "read_then_eventually_send.mcf", but it adds a fairness assumption
% (a message is not lost infinitely often).

nu X.
(
[true]X

&&

forall d:D.
             ([r1(d)]( nu Y. mu Z. ([(!s4(d)) && (!i)]Z && [i]Y) ) )
)
