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;