Dining Philosophers with Host (2)

package dph is

N : constant integer := 2;             -- number of philosophers
type phil_range is range 0 .. (N - 1); -- range for # of philosophers eating

task phil_1;
task phil_2;

task fork_1 is
   entry up;
   entry down;
end fork_1;

task fork_2 is
   entry up;
   entry down;
end fork_2;

task host is
   entry enter;
   entry leave;
end host;

end dph;


package body dph is

task body phil_1 is
   done : Boolean;
begin
   loop
      host.enter;
      -- unlike for the other dining philosophers, we don't avoid deadlock
      -- by having phil_1 pick up fork_1 first here.  That's because the host
      -- task is supposed to avoid the deadlock
      fork_2.up;
      fork_1.up;     --event[{phil_1_eating}]
      fork_2.down;   --eventb[{phil_1_not_eating}]
      fork_1.down;
      host.leave;
      exit when done;
   end loop;
end phil_1;

task body phil_2 is
   done : Boolean;
begin
   loop
      host.enter;
      fork_1.up;
      fork_2.up;     --event[{phil_2_eating}]
      fork_1.down;   --eventb[{phil_2_not_eating}]
      fork_2.down;
      host.leave;
      exit when done;
   end loop;
end phil_2;

task body fork_1 is
   done : Boolean;
begin
   loop
      accept up;
      accept down;
      exit when done;
   end loop;
end fork_1;

task body fork_2 is
   done : Boolean;
begin
   loop
      accept up;
      accept down;
      exit when done;
   end loop;
end fork_2;

task body host is
   done : Boolean;
   count : phil_range;
begin
   count := 0;   --event[{count=0}]
   loop
      select
         when count < phil_range'Last =>
            accept enter;         --eventb[{countis<1}]
            count := count + 1;   --event[{countinc}]
            null;
      or
         accept leave;
         count := count - 1;      --event[{countdec}]
         null;
      end select;
      exit when done;
   end loop; 
end host; 

end dph;