// the number of philosophers
#define N  2
#define N2 4 // 2*N

// the number of available tokens and the states of the forks
byte c = N-1;
bool f[N] = true;

mtype = { GET, PUT };

// the channels between the philosophers and the coin pool
chan crequest[N] = [1] of { mtype };
chan creply[N]   = [1] of { mtype };

// the channels between the philosophers and the forks
chan frequest[N2] = [1] of { mtype };
chan freply[N2]   = [1] of { mtype };

// select a request channel i suitable for coin number c
// may return N, if no channel is suitable
inline selectReq(i, c)
{
  atomic {
  i = 0;
  do
    :: i == N || (c == 0 && crequest[i] ? [ PUT ]) -> break;
    :: i == N || (c > 0 && nempty(crequest[i]))   -> break;
    :: i < N -> i = i+1;
  od;
  if
    :: i == N ->
       i = 0;
       do
         :: i == N || (c == 0 && crequest[i] ? [ PUT ]) -> break;
         :: i == N || (c > 0 && nempty(crequest[i]))   -> break;
         :: i < N && ((c == 0 && !crequest[i] ? [ PUT ]) || 
                      (c > 0 && empty(crequest[i]))) -> i = i+1;
       od;
    :: else -> skip;
  fi;
  }
}

// select a request channel i suitable for coin number c
// runs until a suitable channel is available
inline selectRequest(i, c)
{
  selectReq(i, c);
  do 
  :: i < N -> break;
  :: else  -> selectReq(i, c);
  od;
}

// the pool of coins
proctype coins()
{	 
  byte i;
  do :: true ->
    selectRequest(i, c);
    if
    :: crequest[i] ? GET ->
       c = c-1;
       creply[i] ! GET;
    :: crequest[i] ? PUT ->
       c = c+1;
    fi;
  od;
}

// fork i
proctype fork(byte i)
{
  skip;
}

// philosopher i
proctype philosopher(byte i)
{
  eating: skip;
}

// create N philosophers and N forks and 1 coin pool
init
{
  atomic
  {
    byte i = 0;
    do 
      :: i < N -> run philosopher(i); run fork(i); i = i+1;
      :: else -> break;
    od;
    run coins();
  }
}