_monitor(dining_server)
   op hungry_and_get_forks(i : int), finished_eating(i : int)
   op  check_left_fork_down(i : int; check_very_hungry : bool)
   op check_right_fork_down(i : int; check_very_hungry : bool)
_body(dining_server)
   type states = enum(thinking, hungry, very_hungry, eating)
   var num_phils : int := 5; getarg(2, num_phils)
   var state[1:num_phils] : states := ([num_phils] thinking)
   _condvar1(self, 1:num_phils)

   procedure left(i : int) returns lft : int
      if i=1 -> lft := num_phils [] else -> lft := i-1 fi
   end left

   procedure right(i : int) returns rgh : int
      if i=num_phils -> rgh := 1 [] else -> rgh := i+1 fi
   end right

   procedure see_if_very_hungry(k : int)
      if state[k] = hungry and state[left(k)] != very_hungry and
            state[right(k)] != very_hungry ->
         state[k] := very_hungry
         write("*** at age", age(), "philosopher", k, "is VERY HUNGRY")
      fi
   end see_if_very_hungry

   procedure test(k : int; check_very_hungry: bool)
      if state[left(k)] != eating and state[left(k)] != very_hungry and
            (state[k] = hungry or state[k] = very_hungry) and
            state[right(k)] != very_hungry and state[right(k)] != eating ->
         state[k] := eating
         write("*** at age", age(), "philosopher", k, "may eat")
      [] check_very_hungry ->
         see_if_very_hungry(k) /* simplistic naive check for starvation */
      fi
   end test

   _proc(hungry_and_get_forks(i))
      state[i] := hungry
      test(i, false)
      if state[i] != eating -> _wait(self[i]) fi
   _proc_end

   _proc(finished_eating(i))
      state[i] := thinking
   _proc_end

/*
 * Cannot _signal() in a procedure (undefined m_bozo); must be a _proc().
 * But we cannot change this procedure into an internal _proc() by putting
 * the op below the body because a _proc() that calls a _proc() results in
 * a nested call to the same monitor so deadlock!
 *
 * procedure check_fork_down(i : int; check_very_hungry : bool)
 *    test(i, check_very_hungry)
 *    if state[i] = eating -> _signal(self[i]) fi
 * end check_fork_down
 */

   _proc(check_left_fork_down(i, check_very_hungry))
      /* check_fork_down(left(i)) */
      test(left(i), check_very_hungry)
      if state[left(i)] = eating -> _signal(self[left(i)]) fi
   _proc_end

   _proc(check_right_fork_down(i, check_very_hungry))
      /* check_fork_down(right(i)) */
      test(right(i), check_very_hungry)
      if state[right(i)] = eating -> _signal(self[right(i)]) fi
   _proc_end
_monitor_end