global Parameters
   var check_very_hungry : bool := false
   var num_phils : int := 5, run_time : int := 60
body Parameters
   getarg(1, check_very_hungry); getarg(2, num_phils); getarg(3, run_time)
end Parameters

_monitor(dining_server)
   import Parameters
   op take_forks(i : int), put_forks(i : int)
_body(dining_server)
   type states = enum(thinking, hungry, very_hungry, eating)
   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 can_eat(k : int; do_very_hungry_check: bool)
         returns allowed_to_eat : 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 ->
         allowed_to_eat := true
         write("*** at age", age(), "philosopher", k, "may eat")
      [] else ->
         allowed_to_eat := false
         /* simplistic naive check for starvation */
         if do_very_hungry_check -> see_if_very_hungry(k) fi
      fi
   end can_eat

   _proc(take_forks(i))
      state[i] := hungry
      do not can_eat(i, false) -> _wait(self[i]) od
      state[i] := eating
   _proc_end

   _proc(put_forks(i))
      state[i] := thinking
      if can_eat(left(i), check_very_hungry)  -> _signal(self[left(i)])  fi
      if can_eat(right(i), check_very_hungry) -> _signal(self[right(i)]) fi
   _proc_end
_monitor_end