Dining Philosophers

From Lyra

This is dining philosopher example in the Introduction.

The philosopher process can be modeled using the following Lyra module.

module philosopher(in lget, in rget, in lret, in rret)
{
   fsm
   {
       init think:
           when (lget, rget)
               goto eat;

       state eat:
           when (lret, rret)
               goto think;
   }
}

The fork process can be modeled using the following module.

module fork(out get, out ret)
{
   fsm
   {
       init free:
           when (get)
               goto inuse;

       state inuse:
           when (ret)
               goto free;
   }
}

The toplevel module which instantiates the philosophers and the forks.

module toplevel
{
   rendv g1, g2, g3, g4, g5;
   rendv r1, r2, r3, r4, r5;

   philosopher p1(g1, g2, r1, r2);
   philosopher p2(g2, g3, r2, r3);
   philosopher p3(g3, g4, r3, r4);
   philosopher p4(g4, g5, r4, r5);
   philosopher p5(g5, g1, r5, r1);

   fork f1(g1, r1);
   fork f2(g2, r2);
   fork f3(g3, r3);
   fork f4(g4, r4);
   fork f5(g5, r5);
}