#define IF if :: 
#define FI :: else fi

#define FOR(i,l,h)       i = l ; do :: i < h -> 
#define ENDFOR(i,l,h)    ; i++ :: i >= h -> break od

/* ********************************************************************* */

#define TEMP        252     /* Temporary value */
#define NULL        254     /* Undefined value of lastUID */
#define OTHERS      0       /* Value that is not relevant any more */

#define mkindex(n,a,b)  ( (n * a) + b )
#define first(n,sumindex)  (sumindex / n)
#define second(n,sumindex) (sumindex % n)

#define MaxSeq      3       /* How many messages to check*/

#define Reset  u=0;v=0;m=0
#define Resetscratch  FOR(k,1,4) scratch[k] = 0 ENDFOR(k,1,4) ; k = 0

#define NeeduidSend(u)   Needuidchan[u] = 1
#define AcceptSend(u,v)  Acceptchan[mkindex(3,u,v)] = 1
#define SendSend(m,u)    Sendchan[mkindex(4,m,u)] = 1
#define AckSend(u)       Ackchan[u] = 1
#define CleanupSend(u)   Cleanupchan[u] = 1

inline NeeduidReceive(x) {  
           x = 0;
           FOR(i,1,3)
               if :: 1 :: Needuidchan[i] -> x = i ; break fi
           ENDFOR(i,1,3) ; i = 0
       }

inline AcceptReceive(x,y) {  
           x = 0;
           FOR(i,1,12)
               if :: 1 :: Acceptchan[i] -> x = i ; break fi
           ENDFOR(i,1,12) ; i = 0 ;
           y = second(3,x) ; x = first(3,x)
       }

inline SendReceive(x,y) {  
           x = 0;
           FOR(i,1,16)
               if :: 1 :: Sendchan[i] -> x = i ; break fi
           ENDFOR(i,1,16) ; i = 0 ;
           y = second(4,x) ; x = first(4,x)
       }

inline AckReceive(x) {  
           x = 0;
           FOR(i,1,4)
               if :: 1 :: Ackchan[i] -> x = i ; break fi
           ENDFOR(i,1,4) ; i = 0
       }

inline CleanupReceive(x) {  
           x = 0;
           FOR(i,1,4)
               if :: 1 :: Cleanupchan[i] -> x = i ; break fi
           ENDFOR(i,1,4) ; i = 0
       }
 
#define liveacc(x) ((x == SaccUID) || (x == RaccUID))
#define livemsg(x) ((x == RmsgUID) || (x == SmsgUID) || (x == RlastUID))

#define newacc(x) ( (x == OldRaccUID) -> RaccUID : OTHERS )
#define newmsg(x) ( (x == OldSmsgUID) -> SmsgUID :                       \
                           ( (x == OldRlastUID) -> RlastUID : OTHERS ) )

inline Clearchannels() {
           FOR(i,1,3)
               IF ( !liveacc(i)) ->
                    Needuidchan[i] = 0 ;
                    FOR(j,1,4) Acceptchan[mkindex(3,j,i)] = 0 ENDFOR(j,1,4)
               FI
           ENDFOR(i,1,3) ;
           FOR(i,1,4)
               IF ( ! livemsg(i)) ->
                    FOR(j,1,3) Acceptchan[mkindex(3,i,j)] = 0 ENDFOR(j,1,3) ;
                    FOR(j,0,4) Sendchan[mkindex(4,j,i)] = 0 ENDFOR(j,0,4) ;
                    Ackchan[i] = 0 ;
                    Cleanupchan[i] = 0
               FI
           ENDFOR(i,1,4) ; i = 0 ; j = 0;
       }        

inline CHGchannelsacc() {
           Resetscratch;
           FOR(i,1,3)
               IF Needuidchan[i] -> scratch[newacc(i)] = 1 FI
           ENDFOR(i,1,3) ; 
           FOR(i,1,3) Needuidchan[i] = scratch[i] ENDFOR(i,1,3) ; 
           Resetscratch;
           FOR(i,1,4)
               Resetscratch;
               FOR(j,1,3)
                   IF Acceptchan[mkindex(3,i,j)] -> scratch[newacc(j)] = 1 FI
               ENDFOR(j,1,3) ; 
               FOR(j,1,3) Acceptchan[mkindex(3,i,j)] = scratch[j] ENDFOR(j,1,3)
           ENDFOR(i,1,4) ; 
           Resetscratch ; i = 0
      }
           
inline CHGchannelsmsg() {
           Resetscratch;
           FOR(j,1,3)
               Resetscratch;
               FOR(i,1,4)
                   IF Acceptchan[mkindex(3,i,j)] -> scratch[newmsg(i)] = 1 FI
               ENDFOR(i,1,4) ; 
               FOR(i,1,4) Acceptchan[mkindex(3,i,j)] = scratch[i] ENDFOR(i,1,4)
           ENDFOR(j,1,3) ; 
           Resetscratch;
           FOR(i,0,4)
               Resetscratch;
               FOR(j,1,4)
                   IF Sendchan[mkindex(4,i,j)] -> scratch[newmsg(j)] = 1 FI
               ENDFOR(j,1,4) ; 
               FOR(j,1,4) Sendchan[mkindex(4,i,j)] = scratch[j] ENDFOR(j,1,4)
           ENDFOR(i,0,4) ; 
           Resetscratch;
           FOR(i,1,4)
               IF Ackchan[i] -> scratch[newmsg(i)] = 1 FI
           ENDFOR(i,1,4) ; 
           FOR(i,1,4) Ackchan[i] = scratch[i] ENDFOR(i,1,4) ; 
           Resetscratch;
           FOR(i,1,4)
               IF Cleanupchan[i] -> scratch[newmsg(i)] = 1 FI
           ENDFOR(i,1,4) ; 
           FOR(i,1,4) Cleanupchan[i] = scratch[i] ENDFOR(i,1,4) ;
           Resetscratch ; i = 0 ; j = 0
      }
           
inline NewSaccUID() { d_step {
           OldRaccUID = RaccUID;
           RaccUID = 2 ;        
           SaccUID = TEMP ;     
           CHGchannelsacc() ;     
           Clearchannels() ;      
           SaccUID = 1 ;        
           OldRaccUID = 0       
        } }

inline NewRmsgUID() { d_step {
           OldSmsgUID = SmsgUID;
           OldRlastUID = RlastUID;                                           
           if                                                                
           :: (RlastUID == NULL) -> SmsgUID = 2
           :: else if                                                        
                   :: (SmsgUID == RlastUID) -> SmsgUID = 2 ; RlastUID = 2    
                   :: (SmsgUID != RlastUID) -> SmsgUID = 2 ; RlastUID = 3    
                   fi                                                        
           fi ;                                                              
           RmsgUID = TEMP ;                                                  
           CHGchannelsmsg() ;                                                  
           Clearchannels() ;                                                   
           RmsgUID = 1 ;                                                     
           OldSmsgUID = 0 ;                                                  
           OldRlastUID = 0                                                   
        } }

inline GotoSidle()  {
                  SnextMsg < MaxSeq -> SnextMsg++ ; /* get next message */
                  NewSaccUID() ;                    /* get fresh UID*/
                  goto Sneeduid
           } 

inline Scrash() { atomic {
              do                        /* lose some input msgs */
              :: SnextMsg < MaxSeq -> SnextMsg++ 
              :: skip -> break
              od
              } ; 
              atomic { GotoSidle() }
            } 

inline GotoRidle()  {
                  NewRmsgUID() ;                    /* get fresh UID*/
                  goto Ridle
            }

inline Rcrash() { atomic {
              RlastUID = NULL ;
              GotoRidle()
            } }


    byte    SaccUID = 1,   /* UID used to get new sequence number */
            SmsgUID = 2,   /* UID used as sequence number */
            SnextMsg = 0;  /* The message to be transmitted */

    byte    RaccUID = 2,   /* UID used to get new sequence number */
            RmsgUID = 1,   /* UID used as sequence number */
            RlastUID = 3,  /* rembembers last sequence number */
            RexpMsg = 0;   /* The message to be received */

    byte    OldRaccUID , OldSmsgUID , OldRlastUID ;  /* scratch */

    bit     Needuidchan[3];
    bit     Acceptchan[12];
    bit     Sendchan[16];
    bit     Ackchan[4];
    bit     Cleanupchan[4];

    bit     scratch[4];


active proctype Sender() {   
    byte    i,j,k,m,u,v;            /* Used to receive parameters of messages */

atomic{     Needuidchan[0] = 1;
            FOR(i,0,4) Acceptchan[mkindex(3,i,0)] = 1 ENDFOR(i,0,4) ;
            FOR(i,0,3) Acceptchan[mkindex(3,0,i)] = 1 ENDFOR(i,0,3) ;
            FOR(i,0,4) Sendchan[mkindex(4,i,0)] = 1 ENDFOR(i,0,4) ;
            Ackchan[0] = 1;
            Cleanupchan[0] = 1;
            j = 0 ;
            NewSaccUID()                    /* get fresh UID*/
} 

Sneeduid: do
          :: NeeduidSend(SaccUID)           /* (re)transmit first packet */
          :: atomic { AcceptReceive(u,v) ->
                if
                :: v == SaccUID ->      /* if correct uid start sending */
                      SmsgUID = u ; Reset ; break      
                :: else ->              /* otherwise send cleanup */
                      CleanupSend(u)     
                fi ; Reset
             }
          :: atomic { AckReceive(u) -> CleanupSend(u) ; Reset }
          :: Scrash()               
          od;

Ssend:    do
          :: SendSend(SnextMsg,SmsgUID)          /* (re)transmit message */
          :: atomic { AckReceive(u) ->             
                if
                :: (u == SmsgUID) ->   
                       CleanupSend(u);  
                       GotoSidle()
                :: else -> CleanupSend(u)
                fi ; Reset
             }
          :: atomic { AcceptReceive(u,v) ->    /* if spurious accept */
                IF   (u != SmsgUID) -> CleanupSend(u)  FI ;
             Reset }                       /* if old, send cleanup */
          :: Scrash()         
          od
}


active proctype Receiver()  {
    byte    i,j,k,m,u,v;          /* Used to receive parameters of messages */

  atomic { Needuidchan[0] -> NewRmsgUID() } ;  /* get fresh sequence number */

Ridle:   do
         :: atomic { NeeduidReceive(u)  ->     /* when needuid arrives */
                 RaccUID = u ; Reset ; break }   /* start sending accept */
         :: atomic { SendReceive(m,u)  ->    /* spurious send */
              IF (u != RlastUID) -> AckSend(u)  FI ;
            Reset }                             /* if old uid, send ack */
         :: atomic { CleanupReceive(u) ; Reset }      /* ignore cleanup */
         :: Rcrash()          
         od;

Raccept: do
         :: AcceptSend(RmsgUID,RaccUID)             /* (re)transmit msg 2 */
         :: atomic { SendReceive(m,u) ->   /* on reception of send */
              if                        
              :: (u == RmsgUID) ->         /* if correct uid */
                    RlastUID = u;          /* remember uid */
                    assert( m >= RexpMsg ); /* check ordering */
                    RexpMsg = m+1; Reset ; break /* update expected Msg */
              :: (u != RmsgUID && u != RlastUID) ->  /* if old uid */
                                        AckSend(u)    /* send ack */
              :: else -> skip                      
              fi ; 
              Reset
            }
         :: atomic { NeeduidReceive(u) ; Reset }      /* ignore needuid */
         :: atomic { CleanupReceive(u) ->              /* on cleanup */
                IF (u == RmsgUID) -> RlastUID = NULL; GotoRidle()  FI ;
            Reset }                                   /* clean RlastUID */
         :: Rcrash()
         od;

Rack:    do
         :: AckSend(RmsgUID)              /* (re)transmit ack */
         :: atomic { CleanupReceive(u) ->       /* when cleanup arrives */
             IF (u == RlastUID) -> RlastUID = NULL ; Reset ; GotoRidle() FI ;
            Reset }                        /* if current uid, restart */
         :: atomic { SendReceive(m,u)  ->    /* spurious send msg */
                IF (u != RlastUID) -> AckSend(u)  FI ;
            Reset }                        /* if old uid, send ack */
         :: atomic { NeeduidReceive(u) ; Reset }      /* ignore needuid */
         :: Rcrash()           
         od

}