Dining Philosophers (4)

package dp is

task phil_1;
task phil_2;
task phil_3;
task phil_4;

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

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

task fork_3 is
   entry up;
   entry down;
end fork_3;

task fork_4 is
   entry up;
   entry down;
end fork_4;

end dp;


package body dp is

task body phil_1 is
   done : Boolean;
begin
   loop
      -- avoid deadlock;  we need to do this because otherwise, we
      -- can't use SPIN to check other properties
      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_3.up;
      fork_2.up;     --event[{phil_2_eating}]
      fork_3.down;   --eventb[{phil_2_not_eating}]
      fork_2.down;
      exit when done;
   end loop;
end phil_2;

task body phil_3 is
   done : Boolean;
begin
   loop
      fork_4.up;
      fork_3.up;
      fork_4.down;
      fork_3.down;
      exit when done;
   end loop;
end phil_3;

task body phil_4 is
   done : Boolean;
begin
   loop
      fork_1.up;
      fork_4.up;
      fork_1.down;
      fork_4.down;
      exit when done;
   end loop;
end phil_4;

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 fork_3 is
   done : Boolean;
begin
   loop
      accept up;
      accept down;
      exit when done;
   end loop;
end fork_3;

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

end dp;