Dining Philosophers with Fork Manager (2)

package dpfm is

type phil_range is range 1 .. 2;

task phil_1;
task phil_2;

task manager is
   entry up_1;
   entry up_2;
   entry down_1;
   entry down_2;
end manager;

end dpfm;


package body dpfm is

task body phil_1 is
   done : Boolean;
begin
   loop
      manager.up_1;     --event[{phil_1_eating}]
      manager.down_1;   --eventb[{phil_1_not_eating}]
      exit when done;
   end loop;
end phil_1;

task body phil_2 is
   done : Boolean;
begin
   loop
      manager.up_2;     --event[{phil_2_eating}]
      manager.down_2;   --eventb[{phil_2_not_eating}]
      exit when done;
   end loop;
end phil_2;

task body manager is
   done : Boolean;
   fork_up : array (phil_range) of boolean;
begin
   for I in phil_range loop
      fork_up(I) := false;
   end loop;
   null;     --eventb[fup1=f,fup2=f]
   loop
      select
         when ((not fork_up(1)) and
               (not fork_up(2))) =>
            accept up_1;           --eventb[{fup1is=f},{fup2is=f}]
            fork_up(1) := true;    --event[{fup1=t}]
            fork_up(2) := true;    --event[{fup2=t}]
            null;
      or
         when ((not fork_up(2)) and
               (not fork_up(1))) =>
            accept up_2;           --eventb[{fup2is=f},{fup1is=f}]
            fork_up(2) := true;    --event[{fup2=t}]
            fork_up(1) := true;    --event[{fup1=t}]
            null;
      or
         when (fork_up(1) and
               fork_up(2)) =>
            accept down_1;          --eventb[{fup1is=t},{fup2is=t}]
            fork_up(1) := false;    --event[{fup1=f}]
            fork_up(2) := false;    --event[{fup2=f}]
            null;
      or
         when (fork_up(2) and
               fork_up(1)) =>
            accept down_2;          --eventb[{fup2is=t},{fup1is=t}]
            fork_up(2) := false;    --event[{fup2=f}]
            fork_up(1) := false;    --event[{fup1=f}]
            null;
      end select;
      exit when done;
   end loop;
end manager;

end dpfm;