mtype = {packet,reply};
 init{
 chan ch1send =[0] of {int,int,mtype,int};
 chan ch2send = [0] of {int,int,mtype,int};
 chan ch1recv = [0] of {int,int,mtype,int};
 chan ch2recv=[0] of {int,int,mtype,int};

 run Sender(1,1,ch1send);
 run Sender (2,2,ch2send);
 run Net (ch1send,ch2send,ch1recv,ch2recv);
 run Receiver(ch1recv);
 run Receiver(ch2recv);
 }

 proctype Sender (int sender; int receiver; chan ch){
 int count=0;
 int confirm;
 mtype porr;
 do
 ::(count<10) ->
 porr=packet;
 ch!sender,receiver,porr,count
 if
 ::timeout -> ch!sender,receiver,porr,count
 ::ch?sender,receiver,porr,confirm; count=confirm;
 fi
 ::else-> break
 od
 }

 proctype Net (chan ch1send; chan ch2send; chan ch1recv; chan ch2recv){
 int sender;
 int receiver;
 int data;
 int who;
 chan out;
 int count1;
 int count2;
 mtype porr;

 if
 ::who=1
 ::who=2
 fi
 do
 ::if
 ::(who==1 && count1<10) ->
     if
     ::ch1send?sender,receiver,porr,data;out=ch1recv;who=1
     ::ch1recv?sender,receiver,porr,data;out=ch1send; count1=data
     fi
 ::(who==2 && count2<10) ->
     if
     ::ch2send?sender,receiver,porr,data;out=ch2recv;who=2
     ::ch2recv?sender,receiver,porr,data; out= ch2send; count2=data
     fi
 fi;

 if
 ::(count1==10 && who!=2)-> who=2;
 ::(count2==10 && who!=1)-> who=1;
 ::else->skip
 fi

 if
 ::(porr==packet)->
     if
     ::out!sender,receiver,porr,data
	 ::out!sender,receiver,porr,data
     ::(data!=9)->skip
     fi
 ::(porr==reply)->
     if
     ::out!sender,receiver,porr,data
	 ::out!sender,receiver,porr,data
     ::(data!=10)->skip
     fi
 fi;

 if
 ::(count1==10 && count2==10)->break
 ::else->skip
 fi

 od
 }

 proctype Receiver (chan ch){
 int sender;
 int receiver;
 int data=0;
 mtype porr;

 do
 ::(data<10)->
     ch?sender,receiver,porr,data
     porr=reply;
     data=data+1
     ch!sender,receiver,porr,data
 ::else->break
 od
 }