%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% The dining philosophers in BMAP
%%%% February 2009
%%%% by A. Dovier, A. Formisano, E. Pontelli
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Call :- bmap(9).
%%% leftmost => ~466s
%%% left_fcc => ~378s
%%% left_ffcd => 27h40m
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% It finds a plan that lets all alive at TIME 10
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

philosopher(5).
succ(1,2). succ(2,3). succ(3,4). succ(4,5). succ(5,1). %%% easy to generalize
side(left). side(right).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

agent(X) :- philosopher(Max), interval(X,1,Max).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Fluents
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%% The philosopher X is either hungry (0) or satiated (10)
%%% The level decreases from 10 to 0 at each step

fluent(phil(X),0,10) :- agent(X).

%%% Every hand is either empty (0) or it holds a fork (1)

fluent(hand(X,S),0,1) :- agent(X),side(S).

%%% Every fork is either on the table (0) or held (1)

fluent(fork(X),0,1) :- agent(X).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Actions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

action([X],grasp(S)) :- agent(X),side(S).
action([X],release(S)) :- agent(X),side(S).
action([X],eat) :- agent(X).

%%%%

executable([X],grasp(left),[fork(X) eq 0]) :- agent(X).
executable([X],grasp(right),[fork(Y) eq 0]) :- agent(X),succ(X,Y).
executable([X],release(S), [hand(X,S) eq 1]) :- agent(X),side(S).
executable([X],eat, [hand(X,left) eq 1, hand(X,right) eq 1]) :- agent(X).

%%%%%

causes(hand(X,S) eq 1,[ actocc([X],grasp(S)) ]) :-
       agent(X), side(S).

causes(hand(X,S) eq 0,[actocc([X],release(S)) ]) :-
       agent(X), side(S).

causes(fork(X) eq 1, [actocc([X],grasp(left))]) :-
        agent(X).
causes(fork(Y) eq 1, [actocc([X],grasp(right))]) :-
       agent(X), succ(X,Y).
causes(fork(X) eq 0, [actocc([X],release(left))]) :-
       agent(X).
causes(fork(Y) eq 0, [actocc([X],release(right))]) :-
       agent(X), succ(X,Y).

causes(phil(X) eq 10, [actocc([X],eat)]) :-
       agent(X).

%%%%%

caused([hand(X,S) eq 0, phil(X)^(-1) gt 0], phil(X) eq phil(X)^(-1) -1) :- agent(X),side(S).

%%%%%

concurrency_constraint(actocc([X],grasp(right)) * actocc([Y],grasp(left)) eq 0) :-
   agent(X), agent(Y), succ(X,Y).

%%%%%

initially(phil(X) eq 0) :- agent(X).
initially(hand(X,S) eq 0) :- agent(X), side(S).
initially(fork(X) eq 0)  :- agent(X).

%%%%%%

goal(phil(X) gt 0) :- agent(X).

%%%% Uncomment some of them to run faster

%holds(phil(5) eq 10,3).
%holds(phil(3) eq 10,5).
%holds(phil(1) eq 10,6).
%holds(phil(2) eq 10,9).
%holds(phil(4) eq 10,9).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%