AlternatingBitProtocolWithTimeouts{

    /*           msgs                    msgr
        Sender --------> LossyChannel ---------> Receiver
               <--------              <---------
                 acks                    ackr

        Each package sent by Sender is a pair: (bit, message).

    */

    define timeout 10;

    buffer int msgs size = 2;
    buffer int msgr size = 2;
    buffer int acks size = 1;
    buffer int ackr size = 1;
    
    process Sender{

        stateset S1, S2, S3;

        var int ou, r, s;

	to S1: { s = 0; }

        from S1 to S2:
              {}                           /* next:o */

        from S2 to S3:
              { 
                put(msgs,ou);
                put(msgs,s); 
              }                            /* ->mesg:o:s */

        from S3 to S2:
	      when (lenght(acks) == 0)
              delay [timeout, timeout]:urgent
	      {}                           /* receive, timeout */

        from S3 to S2:
              when (get(acks, r) && r!=s ) /* receive, <-ack, r!=s */
	      {}

        from S3 to S1:
              when (get(acks, r) && r==s)  /* receive, <-ack, r==s */
	      { s = 1 - s; }
   }

    process Receiver{

	stateset S1, S2;
        var int i, a, e;

	to S1: { e = 0; }

        from S1 to S2: 
              when ( get(msgr, i))
              {}                   /* receive, <-mesg:i */

        from S2 to S1:
             when ( get(msgr, a) && (a!=e) )
              { put(ackr, a); }    /* <-mesg:a, ->ack, a!=e */	      

        from S2 to S1: 
              when ( get(msgr, a) && (a==e) )
              { put(ackr, a); 
                e = 1 - e;    
              }                    /* <-mesg:a, ->ack, a==e, e=1-e, accept:i */
   }

    process LossyChan{
  
	stateset S1;
        var int m, n;

	to S1: {}
	
        from S1 to S1:
              when (get (msgs, m) && get(msgs, n))
	      { put(msgr, m); 
                put(msgr, n); }      
                                     /* reliable transmission from S to R */

        from S1 to S1:
              when (get (msgs, m) && get(msgs, n))   
	      {}                     /* loosing of the message from S */
             
        from S1 to S1:
              when (get (ackr, n)) 
	      { put(acks, n); }      /* reliable transmission from R to S */
              
        from S1 to S1:
              when (get (ackr, n))
	      {}                     /* loosing of the message from R */
  }
 
  main 
      { Sender || LossyChan || Receiver }
}