/* Global shared values */
mtype  fork_holder[4] = 0;

proctype odd_philosopher(int num; int left_fork; int right_fork) {
   do
   :: /* Grab left fork. */
      atomic {
        fork_holder[ left_fork] == 0 ->
        fork_holder[ left_fork] = num;
      }

      assert(fork_holder[ left_fork] == num);

      /* Grab right fork. */
      fork_holder[right_fork] == 0 ->
      fork_holder[right_fork] = num;

      assert(fork_holder[right_fork] == num);

      printf("Philosopher %d eating.\n", num);

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

proctype even_philosopher(int num; int left_fork; int right_fork) {
   do
   :: /* Grab left fork. */
      fork_holder[ left_fork] == 0 ->
      fork_holder[ left_fork] = num;

      assert(fork_holder[ left_fork] == num);

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

      assert(fork_holder[right_fork] == num);

      printf("Philosopher %d eating.\n", num);

      /* Drop forks in opposite order of acquisition. */
      fork_holder[right_fork] = 0;
      fork_holder[ left_fork] = 0;
   od
}
init {
   run odd_philosopher(1, 0, 1);
   run even_philosopher(2, 1, 2);
   run odd_philosopher(3, 1, 3);
   run even_philosopher(4, 3, 0);
}