#define NULL        0       /* Undefined value of lastUID */
#define MaxSeq      10     /* How many messages to check*/
#define ChanSize    2       /* channel size */

chan Needuidchan = [ChanSize] of { byte };
chan Acceptchan = [ChanSize] of { byte , byte };
chan Sendchan = [ChanSize] of { byte , byte };
chan Ackchan = [ChanSize] of { byte };
chan Cleanupchan = [ChanSize] of { byte };

active proctype Sender() {   
    byte    SaccUID,       /* UID used to get new sequence number */
            SmsgUID,       /* UID used as sequence number */
            SnextMsg;      /* The message to be transmitted */
    byte    u,v;           /* Used to receive parameters of messages */

Sidle:    SnextMsg < MaxSeq ->          /* get next message to send*/
                     SnextMsg++ ;    
          SaccUID < MaxSeq ->           /* get fresh UID*/
                     SaccUID++ ;       

Sneeduid: do
          :: Needuidchan! SaccUID       /* (re)transmit first packet */
          :: Acceptchan? u, v ->        /* on reception of accept message */
                if
                :: v == SaccUID ->      /* if correct uid start sending */
                      SmsgUID = u ; break      
                :: else ->              /* otherwise send cleanup */
                      Cleanupchan ! u     
                fi
          :: Ackchan? u ->              /* on a spurious ack */
                Cleanupchan ! u         /* reply with cleanup */
          :: goto Scrash                /* crash */
          od;

Ssend:    do
          :: Sendchan!SnextMsg,SmsgUID   /* (re)transmit message */
          :: Ackchan? u ->               /* on reception of ack */
                if
                :: (u == SmsgUID) ->     /* if correct uid */
                       Cleanupchan!u;    /* send cleanup and restart */
                       goto Sidle     
                :: else -> Cleanupchan!u /* otherwise send cleanup */
                fi
          :: Acceptchan? u,v ->          /* if spurious accept */
                if
                :: (u != SmsgUID) ->     /* if old, send cleanup */
                       Cleanupchan!u
                :: else -> skip          /* if current, do nothing */
                fi
          :: goto Scrash                  /* crash */
          od ;

Scrash:   do                             /* lose some input msgs */
          :: SnextMsg < MaxSeq -> SnextMsg++ 
          :: skip -> break
          od;
          goto Sidle
}

active proctype Receiver()  {
    byte    RaccUID,     /* UID used to ge new sequence number */
            RmsgUID,     /* UID used as sequence number */
            RlastUID,    /* rembembers last sequence number */
            RexpMsg;     /* The message to be received */
    byte    m,u,v;       /* Used to receive parameters of messages */

Ridle:   RmsgUID < MaxSeq -> RmsgUID++ ; /* get fresh sequence number */
         do
         :: Needuidchan? RaccUID ->      /* when needuid arrives */
                           break         /* start sending accept */
         :: Sendchan?m,u ->              /* spurious send */
              if                         /* if old uid arrives */
              :: (u != RlastUID) -> Ackchan!u   /* send ack */ 
              :: else -> skip                
              fi
         :: Cleanupchan?u -> skip        /* ignore cleanup */
         :: goto Rcrash                  /* crash */
         od;

Raccept: do
         :: Acceptchan! RmsgUID,RaccUID  /* (re)transmit msg 2 */
         :: Sendchan ? m,u ->            /* on reception of send */
              if                        
              :: (u == RmsgUID) ->         /* if correct uid */
                    RlastUID = u;          /* remember uid */
                    assert( m >= RexpMsg ); /* check ordering */
                    RexpMsg = m+1; break   /* update expected Msg */
              :: (u != RmsgUID && u != RlastUID) ->  /* if old uid */
                                        Ackchan!u    /* send ack */
              :: else -> skip                      
              fi
         :: Needuidchan? v -> skip          /* ignore needuid */
         :: Cleanupchan? u -> 
                if
                :: (u == RmsgUID) ->        /* on cleanup */
                      RlastUID = NULL;      /* clean RlastUID */
                      goto Ridle
                :: else -> skip
                fi
         :: goto Rcrash                     /* crash */
         od;

Rack:    do
         :: Ackchan!RlastUID                /* (re)transmit ack */
         :: Cleanupchan?u ->                /* when cleanup arrives */
                   if
                   :: (u == RlastUID) ->    /* if current uid */
                         RlastUID = NULL;   /* restart */
                         goto Ridle
                   :: else -> skip          /* else skip */
                   fi
         :: Sendchan ? m , u ->             /* spurious send msg */
                   if
                   :: (u != RlastUID) ->    /* if old uid */
                         Ackchan!u          /* send ack */
                   :: else -> skip
                   fi
         :: Needuidchan? v -> skip          /* ignore needuid */
         :: goto Rcrash                     /* crash */
         od;

Rcrash:  RlastUID=NULL;
         goto Ridle
}