
module main {
    type philosopher_state_t = {idle, thinking, waiting, eating};
    type chopstick_state_t = {free, taken};

    var phil1, phil2, phil3, phil4, phil5 : philosopher_state_t;
    var chopstick1, chopstick2, chopstick3, chopstick4, chopstick5 : chopstick_state_t;

    init {
        phil1 := thinking;
        phil2 := thinking;
        phil3 := thinking;
        phil4 := thinking;
        phil5 := thinking;

        chopstick1 := free;
        chopstick2 := free;
        chopstick3 := free;
        chopstick4 := free;
        chopstick5 := free;
    }

    next {
        // Philosopher 1
        if (phil1 = eating) {
            phil1' := thinking;
        } else if (phil1 = thinking & chopstick1 = free & chopstick5 = free) {
            phil1' := eating;
        } else if (phil1 = thinking & (chopstick1 != free | chopstick5 != free)) {
            phil1' := waiting;
        } else if (phil1 = waiting & chopstick1 = free & chopstick5 = free) {
            phil1' := eating;
        } else if (phil1 = waiting & (chopstick1 != free | chopstick5 != free)) {
            phil1' := waiting;
        } else {
            phil1' := phil1;
        }

        // Update chopstick states
        chopstick1' := if (phil1' = eating) then taken else free;
        chopstick5' := if (phil1' = eating) then taken else free;

        // Similar updates needed for other philosophers and chopsticks
    }

    define deadlock :=
        (phil1 = waiting & !(chopstick1 = free & chopstick5 = free)) &
        (phil2 = waiting & !(chopstick2 = free & chopstick1 = free)) &
        (phil3 = waiting & !(chopstick3 = free & chopstick2 = free)) &
        (phil4 = waiting & !(chopstick4 = free & chopstick3 = free)) &
        (phil5 = waiting & !(chopstick5 = free & chopstick4 = free));

    property deadlock_possible {
        always (deadlock -> false)
    }
}