#define N 4 // the number of nodes
#define M 2 // the maximum number of messages in a channel
chan c[N] = [M] of { byte } ;

// the states of the processes
mtype = { idle, waiting, leader } ;
mtype s[N] = idle;

// a system with a single message circulating in a ring
proctype p(byte i)
{
  byte start = true;
  byte j;
  do 
    :: i == 0 && start ->
       c[(i+1)%N] ! i;
       start = false;
    :: s[i] == idle && c[i] ? [ j ] ->
       c[i] ? j ;
       c[(i+1)%N] ! j
  od
}

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