The Dining Philosophers in Rapide 
     =================================
                VERSION 1.
     by Claudio Garcia (Updated: 7/31/97/lp, 4/1/98/jjk)

This is a Rapide model of the classic resource allocation problem of
the Dining Philosphers due to Dijkstra. In our model, diners1.rpd,
there are two types of components, a type of round table at which a
number of philosophers can sit, and a type of philosopher.

To understand the architecture, first scan the interface types, then
see how the objects of those types are connected in the architecture.

The Table interface is parameterized by the number of philosophers ---
it is a type constructor, each instance of which is a type of table
object, e.g., the type of tables for one philosopher, two
philosophers, etc.  A table controls and dispenses the chopsticks by
means of its interface actions. The behavior of tables is specified by
the reactive rules in the behavior part. Essentially, a table will
release a chopstick to a requestor when the chopstick becomes free
(i.e., is initially free, or is recovered).

The rule,

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

will trigger whenever a chopstick ?a is requested by something denoted
by ?i (the architecture connections will show that ?a, ?i have to be
bound to ids for a Chopstick and a Philosopher) AND ?a is free (AND is
expressed as ~). "?a is free" if an event FreeStick(?a) has been
generated and not yet used to trigger a rule (see Architecture LRM for
semantics of behavior rules -- an event can only be used once to
trigger any given rule.)  When the rule triggers it generates an out
event, ReleaseStick with the bindings of ?a, ?i.

A Chopstick gets to be free again according to this rule:

  (?a : Chopstick)
  StickRecovered(?a) ||> FreeStick(?a);; 

Note that FreeStick is an internal event of the Table types (i.e., is
declared in the behavior part), which means that it is not visible at
the architecture level.

The philosopher interface type specifies philosopher objects.  They
can perform two activities: they can generate RequestStick and
PutDownStick events (out actions), and they can receive StickReceived
events (an in action). These events carry an Id for a chopstick.
Philosophers are generated by a simple module generator,
newPhilosopher, which takes the Id and the number of philosophers as
parameters, and generates a module containing instances of the
concurrent processes. These processes define the activities of
philosophers: i.e., when they generate RequestStick and PutDownStick
events, and when they generate certain internal events such as
thinking and eating. A philosopher must acquire two chopsticks in
order to eat rice.

NOTE: we could have used behavior rules in the philosopher interface,
as we did for Tables, but we would have to introduce the number of
philosophers as a parameter, and this is an implementation detail
which should not appear in the interface. So we illustrate the use of
module generators (which, generally, can contain more complex programs
than interface behaviors).

The architecture, diners1(), contains one table and an array of 5
philosophers.  Philosophers (i.e., the objects generated by the
newPhilosopher module generator) have an Id number which
differentiates them from their colleagues. The table associates two
chopsticks with each philosopher by means of chopstick Ids (actually
all Ids are integers anyway!). The Ids encode the model of a chopstick
being placed to the left and to the right of each philosopher, In
diners1, philosphers and the table interact through actions defined in
their interfaces. These actions are wired together at the CONNECT
section of the architecture.  An example connection rule is:

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

which is a point-to-point communication between the Table and the
requesting Philosophers. It connects the Philosopher's out action,
RequestStick to the Table's in action, StickRequested for all the
Philosophers. Whenever a Philosopher generates RequestStick events,
the Table will receive StickRequested events with the same parameter
bindings.

We use a generate statement to define the connections between the
interface actions of each philosopher in the array and the in actions
of the Table --- a "fan-in" of 5 rules; the generate is an iterative
statement that defines the set of connections that are instances of
its connection rules for each value of the iteration parameter.

If we look at the connection rules in diners1, we see that every
chopstick is shared by the two philosophers adjacent to it.  The
chopsticks a given philospher is allowed to acquire and release by
means of the connections between their interfaces and the table are
the ones corresponding to her number and the next one
(e.g. philosopher 1 can acquire sticks 1 and 2).  Philosophers are
thus competing for the chopsticks, and deadlock will occur if all
philosophers get StickReceived events for their left chopstick
simultaneously or their right chopstick simultaneously.  

NOTE: "simultaneously" has a particular meaning since time is not
represented in this model. We discuss this meaning in later examples
of formal constraints.

Now that we have viewed the behaviors of each type of component and
the connections between them, we can reason about how the whole system
behaves.

When a philosopher gets hungry she requests a pair of chopsticks to
the Table object. To do this she has to issue separate requests for
her left and her right sticks. In this first version, left and right
sticks are requested concurrently (see the processes in the
newPhilosopher module generator). This characteristic makes it
difficult to have interleaved single requests from different
philosophers, thus diminishing the probability of deadlock.

When diners1 is executed, the Philosophers activity is triggered by
their Start events, which then generates events to the table,
etc. Philosophers are active for only one cycle of eating and
thinking; it is easy to change this so they continue to cycle, but we
don`t do it to keep our posets small.

The poset we include with this first example (diners1.log) shows that
all Eat events are causally related. This is just one of many possible
behaviors of our system. If you execute the model several times, and
view the resulting posets you will find out that events may be related
in different ways on different executions. In this particular example
it is possible to have Eat events organized in a single dependency
line, or they may appear on different and independent threads of
control. This difference occurs because the execution of a Rapide
model is non-deterministic. Events which are not forced to be causally
ordered by the architecture may appear at different simulation times
on different executions, thereby producing different causal
relationships for each run.

Analyzing the architecture of our system we see that since all
philosophers share a chopstick with their immediate neighbors, there
will always be a causal relationship between immediate neighbors Eat
events. Non-adjacent philosopher's Eat events can occur independently,
provided that their common neighbor Eat event occurs after their
own. You can check which Eat event belongs to which philosopher by
using pov and clicking (with the shift button down) on any of the
ReleaseStick events which preceed Eat events.  This will present you
with some useful event information, including the Philosopher Id
number as Parameter #1.