clear;


agent Spec = accept.'deliver.Spec;

set L = {sendA,sendB,delAckA,delAckB,deliverA,deliverB,ackA,ackB,timeout};
agent Impl = (Sender|Receiver|Medium|Timeout)\L;





agent Sender = SendEatA;

agent SendEatA = accept.CA;
agent CA = delAckB.CA + sendB.CA + delAckA.CA + sendA.CA + SA;
agent SA = 'sendA.( delAckA.SendEatB + timeout.RA );
agent RA = delAckB.RA + sendB.RA + delAckA.SendEatB + SA;

agent SendEatB = accept.CB;
agent CB = delAckB.CB + sendB.CB + delAckA.CB + sendA.CB + SB;
agent SB = 'sendB.( delAckB.SendEatA + timeout.RB );
agent RB = delAckB.SendEatA + sendB.RB + delAckA.RB + SB;





agent Medium = MT | MB;
agent MT = sendA.'deliverA.MT + sendB.'deliverB.MT;
agent MB = ackA.'delAckA.MB + ackB.'delAckB.MB;




agent Receiver = DA;

agent DA = deliverB.DA + deliverA.GA;
agent GA = 'deliver.'ackA.DB;

agent DB = deliverA.DB + deliverB.GB;
agent GB = 'deliver.'ackB.DA;




agent Timeout = 'timeout.Timeout;




deadlocks(Impl);
eq(Spec,Impl);