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

/* Philosopher procedure.
 * num: philosopher's number
 * smaller_fork: the fork the philosopher needs which has the smaller number
 * bigger_fork: the second the philosopher needs which has the bigger number
 * Requirement: smaller_fork < bigger_fork
 */
proctype philosopher(int num; int smaller_fork; int bigger_fork) {
   do
   :: /* Grab smaller fork. */
      atomic {
        fork_holder[smaller_fork] == 0 ->
        fork_holder[smaller_fork] = num;
      }

      assert(fork_holder[smaller_fork] == num);

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

      assert(fork_holder[bigger_fork] == num);

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

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

init {
   run philosopher(1, 0, 1); /* Run philosopher 1, smaller fork is 0, bigger fork is 1 */
   run philosopher(2, 1, 2); /* Run philosopher 2, smaller fork is 1, bigger fork is 2 */
   run philosopher(3, 0, 2); /* Run philosopher 3, smaller fork is 0, bigger fork is 2 */
}