----------------------------------------------------------------------
-- Dining Philosophers
--
-- synchronisation by protected objects room and fork (1..#phils):
--                room (always less than #phils inside) => deadlock prevention,
--                                                 fork => mutual exclusion;
-- for demo, phils call trace task whenever having seized/released a fork
----------------------------------------------------------------------

with Stringpack; use Stringpack;
procedure Philosophers is

   How_Many : constant Natural := 5;
   subtype Phil_Range is Integer range 0..How_Many-1;
   How_Often : constant Natural := 5;          -- Zahl der Speisungen/Philosoph

   task Trace is --------------------------------------------------------
      entry Up(Where : Phil_Range);
      entry Down(Where : Phil_Range);
   end Trace;

   task body Trace is
      Busy : array(Phil_Range) of Boolean := (others => False);
   begin
      loop
         Outbuffer := Varnull;
         select
            accept Up(Where : Phil_Range)
            do Busy(Where) := True; end Up;
            for J in Phil_Range loop
               if Busy(J) then Outbuffer := Outbuffer & " X";
               else Outbuffer := Outbuffer & " +"; end if;
            end loop;
            Print;
         or
            accept Down(Where : Phil_Range)
         do Busy(Where) := False; end Down;
            for J in Phil_Range loop
               if Busy(J) then Outbuffer := Outbuffer & " X";
               else Outbuffer := Outbuffer & " -"; end if;
            end loop;
            Print;
         or
            terminate;
         end select;
      end loop;
   end Trace;  ----------------------------------------------------------




   protected Room is  ---------------------------------------------------
      entry Enter;
      procedure Leave;
   private
      Present : Natural := 0;
   end Room;

   protected body Room is
      entry Enter when Present < How_Many -1 is
      begin Present := Present +1; end Enter;
      procedure Leave is
      begin Present := Present -1; end Leave;
   end Room;  -----------------------------------------------------------

   protected type Forks is  ---------------------------------------------
      entry Pick_Up;
      procedure Put_Down;
   private
      Free : Boolean := True;
   end Forks;

   protected body Forks is
      entry Pick_Up when Free is
      begin Free := False; end Pick_Up;
      procedure Put_Down is
      begin Free := True; end Put_Down;
   end Forks;

   Fork : array(Phil_Range) of Forks; -----------------------------------

   task type Philosophers (Me : Phil_Range);   --------------------------

   task body Philosophers is
   begin
      for I in 1..How_Often loop
         delay 0.0001; -- think
         Room.Enter;
         Fork(Me).Pick_Up;  --left fork
         Trace.Up(Me);
         Fork((Me + 1) mod How_Many).Pick_Up; --right fork
         Trace.Up((Me + 1) mod How_Many);
         delay 0.0001; -- eat
         Fork(Me).Put_Down;  --left fork
         Trace.Down(Me);
         Fork((Me + 1) mod How_Many).Put_Down; --right fork
         Trace.Down((Me + 1) mod How_Many);
         Room.Leave;
      end loop;
   end Philosophers;

   type A_Philosophers is access Philosophers;
   Philosopher : array(Phil_Range) of A_Philosophers;  ------------------

begin  -----------------------------------------------------------main

   for I in Phil_Range loop Philosopher(I) := new Philosophers(I); end loop;

end Philosophers;  ---------------------------------------------------