module diningPhilosophers {
    type philosopherId = { A, B, C, D, E };
    type chopstickId = { X, Y, Z, W, V };

    var phil1, phil2, phil3, phil4, phil5 : philosopherId;
    var chopstick1, chopstick2, chopstick3, chopstick4, chopstick5 : chopstickId;
    var bowl : boolean;

    init {
        phil1 = A; phil2 = B; phil3 = C; phil4 = D; phil5 = E;
        chopstick1 = X; chopstick2 = Y; chopstick3 = Z; chopstick4 = W; chopstick5 = V;
        bowl = true;
    }

    next {
        // philosopher A
        if (phil1 == A) {
            if (bowl && chopstick1 == X && chopstick5 == V) {
                chopstick1 = V; chopstick5 = X; bowl = false;
            }
            phil1 = B;
        }
        // philosopher B
        if (phil2 == B) {
            if (bowl && chopstick1 == V && chopstick2 == X) {
                chopstick1 = X; chopstick2 = V; bowl = false;
            }
            phil2 = C;
        }
        // philosopher C
        if (phil3 == C) {
            if (bowl && chopstick2 == V && chopstick3 == X) {
                chopstick2 = X; chopstick3 = V; bowl = false;
            }
            phil3 = D;
        }
        // philosopher D
        if (phil4 == D) {
            if (bowl && chopstick3 == V && chopstick4 == X) {
                chopstick3 = X; chopstick4 = V; bowl = false;
            }
            phil4 = E;
        }
        // philosopher E
        if (phil5 == E) {
            if (bowl && chopstick4 == V && chopstick5 == X) {
                chopstick4 = X; chopstick5 = V; bowl = false;
            }
            phil5 = A;
        }
    }

    property no_deadlock: !(phil1 == A && phil2 == B && phil3 == C && phil4 == D && phil5 == E &&
                           chopstick1 == V && chopstick2 == X && chopstick3 == V && chopstick4 == X && chopstick5 == V);
}
