%%% A test HYPROLOG test program
%%% - dining philosophers 
%%%
%%% Finding different paths in a graph with constraints.
%%%
%%% (c) Henning Christiansen 2008
%%%
%%% The example is explained in the following reference
%%% as example 3.2
%%%
%%% H. Christiansen.
%%% Executable specifications for hypothesis-based reasoning with
%%% Prolog and Constraint Handling Rules,
%%% Journal of Applied Logic, to appear 2008 or -09.
%%% Preliminary version available at
%%% http://www.ruc.dk/~henning/publications/HypoReason2008_HC.pdf

%%% The dining philosophers problem was introduced by E.W.Dijkstra (1071) as a 
%%% prototype problem for process synchronisation and also considered in the lit- 
%%% erature on abduction. We use here a formulation inspired by Gavanelli & al's
%%% CLIMA-IV paper. Consider 
%%% (here) five philosophers sitting at a round table with one chopstick placed 
%%% between each two philosophers. In order to eat, a philosopher needs two chop- 
%%% sticks which he can take from the table and but back afterwards. Clearly, no 
%%% two neigbouring philosophers can eat at the same time. We use the following 
%%% constraint solver to indicate the overall conditions.

abducibles        chop_in_use/3, % chop_in_use(ChopId, PhilosopherId, Time)
                  chop_free/2,   % chop_free(ChopId, Time)
                  eating/3.      % used to store and output result only



chop_in_use(C,Ph,Tx), chop_free(C,Ty) ==> true | (Tx=Ty ; dif(Tx,Ty) ).

chop_in_use(C,Phx,T), chop_in_use(C,Phy,T) ==> Phx=Phy.

%%% The first integrity constraint above allows to take a chopstick which is free at time t 
%%% to be used by a philosopher starting from t; the second one states that only 
%%% one philosopher can use a given chopstick at any given time. 

%%% Test by the following.
%%% For simplicity, it is assumed that each philosopher wants to eat just once. 
%%% Now the following query defines the initial setup at time t0 and poses the 
%%% philosophersÕ desire to eat.

q:-
  chop_free(c1,t0), chop_free(c2,t0), chop_free(c3,t0),
      chop_free(c4,t0), chop_free(c5,t0),  
  phil(ph1), phil(ph2), phil(ph3), phil(ph4), phil(ph5). 

%%% The sequence of actions performed by each philosopher is described by the 
%%% following prolog rule. 


phil(P):-
    compute_needed_chops(P,C1,C2),
    chop_in_use(C1,P,T1), chop_in_use(C2,P,T1),
    eat(T1,T2),   eating(P,T1,T2),
    chop_free(C1,T2), chop_free(C2,T2).
    

%%% The following prolog facts describe the positioning around the table and a 
%%% simple implementation of time, indicating possible successive Ôeating intervalsÕ. 

eat(t0,t1).
eat(t1,t2).
eat(t2,t3).
eat(t3,t4).
eat(t4,t5).
eat(t5,t6).

% 

compute_needed_chops(ph1,c1,c2).
compute_needed_chops(ph2,c2,c3).
compute_needed_chops(ph3,c3,c4).
compute_needed_chops(ph4,c4,c5).
compute_needed_chops(ph5,c5,c1).

/**********

First

?- q.

....
eating(ph5,t4,t5),
eating(ph4,t3,t4),
eating(ph3,t2,t3),
eating(ph2,t1,t2),
eating(ph1,t0,t1) ? ;


5th solution:

....
eating(ph5,t1,t2),
eating(ph4,t0,t1),
eating(ph3,t2,t3),
eating(ph2,t1,t2),
eating(ph1,t0,t1) ? 

**********/