Dining Philosophers

Three philosophers sit around a circular table. Each needs both adjacent forks to eat. The spec verifies that no two adjacent philosophers can eat simultaneously.

The spec

Source

// Dining Philosophers - Parameterized version
// 3 philosophers (0, 1, 2) around a table with 3 forks.
// Each philosopher needs both adjacent forks to eat.
// Fork p is between philosopher p and philosopher (p+1)%3.
// Use: No constants needed

module DiningPhilosophers

// 0=thinking, 1=hungry, 2=eating
var philState: Dict[0..2, 0..2]
var fork: Dict[0..2, Bool]  // fork[i] = true means fork i is available

init {
    philState = {p: 0 for p in 0..2};
    fork = {f: true for f in 0..2};
}

// Philosopher gets hungry
action Hungry(p: 0..2) {
    require philState[p] == 0;
    philState = philState | { p: 1 };
}

// Philosopher eats (needs forks p and (p+2)%3)
action Eat(p: 0..2) {
    require philState[p] == 1;
    require fork[p] == true and fork[(p + 2) % 3] == true;
    philState = philState | { p: 2 };
    fork = fork | { p: false, (p + 2) % 3: false };
}

// Philosopher finishes eating
action Done(p: 0..2) {
    require philState[p] == 2;
    philState = philState | { p: 0 };
    fork = fork | { p: true, (p + 2) % 3: true };
}

// Safety: No two adjacent philosophers eating (they share a fork)
invariant NoAdjacentEating {
    all p in 0..2: not (philState[p] == 2 and philState[(p + 1) % 3] == 2)
}

What to notice

• Modular arithmetic. (p + 2) % 3 maps each philosopher to their left fork. With 3 philosophers in a circle, philosopher 0’s left fork is fork 2.
• Multi-key dict update. fork = fork | { p: false, (p + 2) % 3: false } updates two entries in one expression.
• Deadlock expected. This spec can deadlock (all philosophers hungry, no forks available). Use --no-deadlock.

specl check dining-philosophers.specl --no-deadlock