mtype { NOONE, ONE, TWO, THREE };   /* Symbols, used as fork-owner values. */

/* Global shared values */
mtype fork_holder[3] = NOONE;

active proctype philosopher1()
{
   int  left_fork = 0;
   int right_fork = 1;

   do
   :: /* Grab left fork. */
      atomic {
        fork_holder[ left_fork] == NOONE ->
        fork_holder[ left_fork] = ONE;
      }

      /* Grab right fork. */
      atomic {
        fork_holder[right_fork] == NOONE ->
        fork_holder[right_fork] = ONE;
      }

      printf("Philosopher 1 eating.\n");

      /* Drop forks in opposite order of acquisition. */
      fork_holder[right_fork] = NOONE;
      fork_holder[ left_fork] = NOONE;
   od
}

active proctype philosopher2()
{
   int  left_fork = 1;
   int right_fork = 2;

   do
   :: /* Grab left fork. */
      atomic {
        fork_holder[ left_fork] == NOONE ->
        fork_holder[ left_fork] = TWO;
      }

      /* Grab right fork. */
      atomic {
        fork_holder[right_fork] == NOONE ->
        fork_holder[right_fork] = TWO;
      }

      printf("Philosopher 2 eating.\n");

      /* Drop forks in opposite order of acquisition. */
      fork_holder[right_fork] = NOONE;
      fork_holder[ left_fork] = NOONE;
   od
}

active proctype philosopher3()
{
   int  left_fork = 2;
   int right_fork = 0;

   do
   :: /* Grab left fork. */
      atomic {
        fork_holder[ left_fork] == NOONE ->
        fork_holder[ left_fork] = THREE;
      }

      /* Grab right fork. */
      atomic {
        fork_holder[right_fork] == NOONE ->
        fork_holder[right_fork] = THREE;
      }

      printf("Philosopher 3 eating.\n");

      /* Drop forks in opposite order of acquisition. */
      fork_holder[right_fork] = NOONE;
      fork_holder[ left_fork] = NOONE;
   od
}