/* Run instructions:
 * spins -DN=4 philosophers.prm
 * prom2lts-seq --deadlock --max=10 --trace=deadlock.gcf philosophers.prm.spins
 * ltsmin-printtrace deadlock.gcf | grep action | cut -d' ' -f12-
 */

#define __instances_philosopher N

#define left forks[L]
#define right forks[R]

mtype = {fork};

chan forks[N] = [1] of {bit};

proctype philosopher(int L; int R) {
    do
    :: left?fork -> right?fork;
        /* eat... */
        left!fork; right!fork
        /* meditation... */
    od
}

init {
    atomic {
        int idx = 0;
        do
        :: idx < N ->
            run philosopher(idx, (idx+1)%N);
            forks[idx]!fork;
            idx++
        :: else ->
            break
        od
    }
}