View source

This is dining philosopher example in the [[Introduction to Lyra#Example: Dining Philosophers|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;<br/>
        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;<br/>
        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;<br/>
    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);<br/>
    fork f1(g1, r1);
    fork f2(g2, r2);
    fork f3(g3, r3);
    fork f4(g4, r4);
    fork f5(g5, r5);
 }