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. */
      fork_holder[ left_fork] == NOONE ->
      fork_holder[ left_fork] = ONE;

      assert(fork_holder[ left_fork] == ONE);

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

      assert(fork_holder[right_fork] == ONE);

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

      /* Drop forks. */
      fork_holder[ left_fork] = NOONE;
      fork_holder[right_fork] = NOONE;
   od
}

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

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

      assert(fork_holder[ left_fork] == TWO);

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

      assert(fork_holder[right_fork] == TWO);

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

      /* Drop forks. */
      fork_holder[ left_fork] = NOONE;
      fork_holder[right_fork] = NOONE;
   od
}

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

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

      assert(fork_holder[ left_fork] == THREE);

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

      assert(fork_holder[right_fork] == THREE);

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

      /* Drop forks. */
      fork_holder[ left_fork] = NOONE;
      fork_holder[right_fork] = NOONE;
   od
}