Five philosophers share five forks around a table; each needs both neighbouring forks to eat. The Chandy–Misra solution passes forks on request and marks them clean or dirty so that nobody starves. This example derives, from a recorded trace, every request, every fork hand-over, and every meal.
Run it in the playground · Source
Given who is hungry in each step of a trace and who holds which fork, which fork requests are sent, which forks change hands, and which philosopher eats in which slot using which forks?
The example does not search for a schedule. It reasons over a fixed trace and derives what the protocol says must happen in it.
left_fork(dp_P3, dp_F23). right_fork(dp_P3, dp_F34).
slot(dp_C0, dp_s1, 1). after_sends(dp_C0, dp_C1). after_eat(dp_C1, dp_C2).
hungry(dp_C0, dp_P1). hungry(dp_C0, dp_P3).
start_state(dp_C0, dp_F23, dp_P2, dp_Dirty).
Philosopher P3 sits between forks F23 and F34. In configuration C0, P1 and P3 are hungry, and fork F23 starts with P2, dirty.
request(C, P, Q, F) :-
hungry(C, P), left_fork(P, F), start_state(C, F, Q, _cleanliness), (Q \= P).
send_fork(C, Q, P, F) :-
request(C, P, Q, F), start_state(C, F, Q, dp_Dirty).
meal(M, P, N, S) :-
after_sends(C, Cs), slot(C, S, N), hungry(C, P), meal_handle(P, N, M),
left_fork(P, Lf), right_fork(P, Rf),
after_send_state(Cs, Lf, P, _leftcleanliness),
after_send_state(Cs, Rf, P, _rightcleanliness).
A hungry philosopher requests a fork someone else holds. The holder sends it if the fork is dirty, meaning it has been used since it was received. A meal happens when, after the sends, the philosopher holds both forks.
eyeprolog examples/dining-philosophers.pl
dp_type(dp_mP3_1, dp_Meal).
dp_philosopher(dp_mP3_1, dp_P3).
dp_mealNo(dp_mP3_1, 1).
dp_inSlot(dp_mP3_1, dp_s1).
dp_usesFork(dp_mP3_1, dp_F23).
dp_usesFork(dp_mP3_1, dp_F34).
P3’s first meal is in slot s1, with forks F23 and F34. The full output has 350 answers: 26 requests, 26 fork sends, and 15 meals (three for each philosopher), each described by several facts.
eyeprolog --proof examples/dining-philosophers.pl
step(after_send_state(dp_C1, dp_F23, dp_P3, dp_Clean),
rule(135),
['Cs' = dp_C1, 'F' = dp_F23, 'P' = dp_P3, 'C' = dp_C0],
[after_sends(dp_C0, dp_C1), send_fork(dp_C0, dp_P2, dp_P3, dp_F23)]).
P3 holds F23 after the sends, clean, because P2 sent it in C0. That hand-over is one of the premises of P3’s first meal, together with the slot, the hunger fact, and P3 already holding F34.
eyeprolog --proof examples/dining-philosophers.pl > dining-philosophers.why.pl
eyeprolog --check-proof dining-philosophers.why.pl examples/dining-philosophers.pl
condition('C1', resolution, ok, 539).
condition('C4', coverage, ok, 1070).
condition('C7', relevance, ok, 899).
verdict(checked).
All 539 rule steps replay against the program and the 10 built-in \= tests
are recomputed. Every one of the 350 claims is covered, and nothing is taken
on trust.
hungry(dp_C0, dp_P3). Which requests, sends, and meals disappear?dp_Dirty to dp_Clean. Is
the fork still sent?--goal 'dp_philosopher(M, dp_P5)' to list P5’s meals.Learn more in The Art of EyeProlog, Chapter 14 (knowledge engineering).