Dining Philosophers (2)

package dp is

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;

end dp;


package body dp is

task body phil_1 is
   done : Boolean;
begin
   loop
      fork_2.up;
      fork_1.up;     --event[{phil_1_eating}]
      fork_2.down;   --eventb[{phil_1_not_eating}]
      fork_1.down;
      exit when done;
   end loop;
end phil_1;

task body phil_2 is
   done : Boolean;
begin
   loop
      fork_1.up;
      fork_2.up;     --event[{phil_2_eating}]
      fork_1.down;   --eventb[{phil_2_not_eating}]
      fork_2.down;
      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;

end dp;