resource dining_server
   op take_forks(i : int), put_forks(i : int)
body dining_server(num_phil : int)
   write("dining server for", num_phil, "philosophers is alive")
   type states = enum(thinking, hungry, eating)
   var state[1:num_phil] : states := ([num_phil] thinking)

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

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

   process serving
      do true ->   # no explicit hungry state
         in take_forks(i) st state[left(i)] ~= eating
               and state[right(i)] ~= eating ->
            state[i] := eating
         [] put_forks(i) -> state[i] := thinking
         ni
      od
   end serving
end dining_server