% There is a path along which a message (after reading through
% action r1) can be lost infinitely often (through c3).
%
% This property is true for the alternating bit protocol, because there is
% no fairness assumption.
%
% Note: e as parameter of c3 means an error is communicated, hence a message
% was lost.
%
% This requires that c4 and c7 are removed from the hide set in cabp.mcrl2
% before running mcrl22lps and lps2pbes.

<true*>(exists d:DATA .<r1(d)>(nu X. mu Y. (<c7(ae)>X || <!c4(ce) && !s2(d)>Y)))
