/* 
Parallel acknowledgment with retransmission protocol
see, for example:
   A. Tanenbaum, "Computer Networks, Prentice Hall, 1989
or
   A. S. Klusener, "Models and Axioms for a Fragment of Real
                    Time Process Algebra", Ph.D. thesis, 
                    Eindhoven Uinversity of Technology, 1993
or
  F. Vaandrager, "Two Simple Communication Protocols", 
  in J.C.M. Baeten, ed., Applications of Process Algebra, pp.23-44,
  Cambridge University Press, 1990
*/



#include "dtime.h"   /* timed features */

/*PAR time parameters*/
  
#define dK 3
#define dL 3
#define dR 1
#define To 9

#define MAX 8 /*max number of different message contents*/


/*channels*/

chan StoR = [1] of {byte, bit}
chan RtoS = [1] of {bit}


#define ACK 1

 
proctype Sender(chan in, out)
{	
        timer sc;
        byte mt; /* message data */
	bit  sn=0; /* sequence number*/
	
  R_h:	/*unbounded start delay - sending of a new message
        can start in any time slice*/
        udelay(sc); 
        mt = (mt+1)%MAX; /* Input from the upper layer */
	
  S_f:	delay(sc,dK); 
        out!mt,sn; /*send and delay in channel K*/
        set(sc,To-dK); 
        /*modelling peculliarity - the delay along the
        channel K should be subtracted from the timeout period*/
	
  W_s:	do
	:: in?_ ->
           if
           :: atomic{skip; delay(sc, 1); sn=1-sn; goto R_h;}; /*ack is OK*/
           :: atomic{printf("MSC: ACKerr\n");  goto S_f};
           fi;
        :: expire(sc) -> goto S_f;  /*timeout*/
        od;  	
	
}




proctype Receiver(chan in, out)
{
       timer rc;
       show byte mr;   /* received message */
       show byte me=1; /* expexted message*/
       bit rsn, esn=0; /*received and expected sequence number*/
   
  W_f: in?mr,rsn;
       if
       :: rsn == esn -> goto S_h; /*correct message and seq. num */
       :: rsn == 1-esn -> goto S_a; /*correct message, wrong  seq. num */
       :: atomic{printf("MSC: MSGerr\n"); goto W_f;};
       fi;
          
  S_h: /*Out!mr*/ /* output to the upper layer */
 
       /* expected message received */
       assert(mr == me);     
       
       delay(rc,dR); /*message processing delay*/
       atomic{esn = 1-esn; me = (me+1)%MAX};
              
  S_a: atomic{delay(rc, dL); out!ACK}; /*send and delay in channel L*/
       atomic{delay(rc, 1); goto W_f;}; 
}	



init
{    
    atomic{
           run Sender(RtoS, StoR);
           run Receiver(StoR, RtoS);
          }
}