// the basic version, N philosophers byte fork[4]; process phil_0 { state think, one, eat, finish; init think; trans think -> one {guard fork[0] == 0; effect fork[0] = 1;}, one -> eat {effect fork[1] = 1;}, eat -> finish {effect fork[0] = 0; }, finish -> think {effect fork[1] = 0; }; } process phil_1 { state think, one, eat, finish; init think; trans think -> one {effect fork[1] = 1;}, one -> eat {guard fork[2] == 0; effect fork[2] = 1;}, eat -> finish {effect fork[1] = 0; }, finish -> think {effect fork[2] = 0; }; } process phil_2 { state think, one, eat, finish; init think; trans think -> one {guard fork[2] == 0; effect fork[2] = 1;}, one -> eat {guard fork[3] == 0; effect fork[3] = 1;}, eat -> finish {effect fork[2] = 0; }, finish -> think {effect fork[3] = 0; }; } process phil_3 { state think, one, eat, finish; init think; trans think -> one {guard fork[3] == 0; effect fork[3] = 1;}, one -> eat {guard fork[0] == 0; effect fork[0] = 1;}, eat -> finish {effect fork[3] = 0; }, finish -> think {effect fork[0] = 0; }; } system async;