-- 
-- Dining Philosophers in Rapide, Version 1
-- 
-- Claudio Garcia
--


-------- Types for parameters ----------------
  
   type PhilosopherId is integer;
   type Chopstick is integer;


---------------- Table type. -----------------
-- Chopsticks are released one by one.
-- This may result in a deadlock situation.

type Table(numPhils : integer) is interface

  action in  StickRequested(n : Chopstick; id: PhilosopherId),
             StickRecovered(n : Chopstick);
  action out ReleaseStick(n : Chopstick; id: PhilosopherId);

behavior

  action  FreeStick(n : Chopstick);

begin

  start =>  for i: integer in 0..(numPhils-1) do
              FreeStick(i);
            end for;;

  (?a : Chopstick; ?i : PhilosopherId) 
  StickRequested(?a, ?i) ~ FreeStick(?a) ||> ReleaseStick(?a, ?i);;

  (?a : ChopStick)
  StickRecovered(?a) ||>  FreeStick(?a);;
                       
end Table;


type Philosopher is interface

  action  out RequestStick(n: Chopstick; id: PhilosopherId),
              PutDownStick(n : Chopstick);
          in  StickReceived(n : Chopstick; id: PhilosopherId);
                          
end;


-- Philosopher module generator
-- Receives as instantiation parameters an id number and
-- the total number of philospohers in the table.
--
-- Deadlock in this version is possible but very unlikely because both
-- left and right chopsticks are requested simultaneously. This diminishes
-- the chance of having interleaved RequestStick events from different 
-- philosophers at the table object, a necessary condition for deadlock.
--
module  newPhilosopher(id: PhilosopherId; numPhils:integer) return Philosopher is

 ACTION Hungry(),
        Think(),
        Eat();

parallel  
   when Start
   do
      Hungry();
   end;
   ||
   when Hungry
   do
      RequestStick(id, id);                      -- request left chopstick
   end;
   ||
   when Hungry
   do
      RequestStick((id+1) mod numPhils, id);     -- request right chopstick
   end;
   ||
   when
      StickReceived(id, id) ~                    --received left chopstick
      StickReceived((id+1) mod numPhils, id)     --received right chopstick
   do
      Eat();
   end;
   ||
   when
      Eat 
   do
      PutDownStick(id);
      PutDownStick((id+1) mod numPhils);
      Think();
   end;
end;


-- Dining system architecture. Instantiates the different components and 
-- connects them together. 

architecture diners1() is

   num_philosophers : integer is 5;

   Ph : array(PhilosopherId, Philosopher) is (
                                         0 is newPhilosopher(0, num_philosophers),
                                         1 is newPhilosopher(1, num_philosophers),
                                         2 is newPhilosopher(2, num_philosophers),
                                         3 is newPhilosopher(3, num_philosophers),
                                         4 is newPhilosopher(4, num_philosophers)
                                     );
				
   Ta: Table(num_philosophers);        

connect

   (?a : Chopstick; ?i : PhilosopherId) Ta.ReleaseStick(?a, ?i)
    to
    Ph[?i].StickReceived(?a, ?i);

    for j : PhilosopherId in 0..num_philosophers-1
      generate

       (?a : Chopstick; ?i : PhilosopherId) Ph[j].RequestStick(?a, ?i)
        to
        Ta.StickRequested(?a, ?i);

       (?a : Chopstick )Ph[j].PutDownStick(?a)
        to
        Ta.StickRecovered(?a);

    end;

end architecture diners1;