#define N 3 // the number of nodes
#define M 3 // the maximum number of surplus messages per node

mtype = { MSG, WHITE, BLACK } ;
chan left[N] = [1] of { mtype } ;
chan right[N] = [1] of { mtype } ;
chan token[N] = [1] of { mtype, short } ;

bool passive[N] = false ;
byte termination = 0 ; // 0: no detection
                       // 1: detection process started, 
                       // 2: detection successfully completed

proctype node(byte i)
{
  short counter = 0 ;
  mtype color = WHITE ;
  short tcounter = 0 ;
  mtype tcolor = WHITE ;
  do 
  :: atomic 
     {
       !passive[i] && len(left[(i+N-1)%N]) == 0 && counter < M ->
       left[(i+N-1)%N] ! MSG ;
       counter++ ;
     }
  :: atomic 
     {
       !passive[i] && len(right[(i+1)%N]) == 0 && counter < M ->
       right[(i+1)%N] ! MSG ;
       counter++ ;
     }
  :: atomic 
     {
       left[i] ? MSG ->
       passive[i] = false ;
       counter-- ;
       color = BLACK ;
     }
  :: atomic 
     { 
       right[i] ? MSG ->
       passive[i] = false ;
       counter-- ;
       color = BLACK ;
     }
  :: atomic
     {
       !passive[i] ->
       passive[i] = true ;
     }
  od
}

init
{
  atomic
  {
    byte i = 0;
    do 
      :: i < N -> run node(i) ; i = i+1 ;
      :: else -> break ;
    od
  }
}