% graph nodes
node(N) :- jet(N). node(N) :- junction(N). node(N) :- tank(N).

% useable links are those without stuck valves
useablelink(N1,N2,V) :- link(N1,N2,V), not stuck(V).

% lengths of useable paths (ie w/o stuck valves) to goal, bounded by
% the number of valves
dist(J,0) :- goal(J).
dist(N,DN) :- dist(K,DK), useablelink(N,K,Fv1), DN=DK+1, numValves(NV), DN <= NV.

% minimum distance of a node to the goal node
nodemindist(N,DN) :- node(N), dist(N,DN), not existDnLessThan(N,DN).
existDnLessThan(N,DN) :- dist(N,DN), dist(N,DN1), DN1<DN.

% minimum distance of a full tank to the goal node
fulltankmindist(T,DT) :- tank(T), full(T), nodemindist(T,DT).

% Fail if no full tank can be reached from the goal.
reachablefulltankexists :- fulltankmindist(T,D).
:- not reachablefulltankexists.

% the full tanks and their minimum distances to the goal node, which
% have the minimum distance over all full tanks
bestfulltankdist(T,SD) :- fulltankmindist(T,SD), not existFTLessThan(SD).
existFTLessThan(SD) :- fulltankmindist(Fv1,SD), fulltankmindist(Fv2,SD1), SD1<SD.

goodtank(T) :- bestfulltankdist(T,Fv1).
bestdist(D) :- bestfulltankdist(Fv1,D).

% "Choose" the lexicographically smallest good tank, as any will do.

nbesttank(T) :- goodtank(T), goodtank(T1), T1 < T.
besttank(T) :- goodtank(T), not nbesttank(T).

% Now go back to the goal, starting from the chosen tank.
reached(T,SD) :- bestfulltankdist(T,SD), besttank(T).

% In any step, choose the smallest non-stuck valve among those linking
% the reached node of distance D to other nodes of distance D-1.
nsmallestvalve(V2,D1) :- reached(N,D), D1=D-1, useablelink(N,N1,V1), useablelink(N,N2,V2), V1 < V2, nodemindist(N1,D1), nodemindist(N2,D1).

smallestvalve(V,D1) :- reached(N,D), D1=D-1, useablelink(N,N1,V), nodemindist(N1,D1), not nsmallestvalve(V,D1).

% Reverse order for switching on (moving from tank to jet, starting from 0).
switchon(V,DN) :- smallestvalve(V,D), bestdist(BD), DX=BD-D, DN=DX-1.

% Now choose the smallest node linked by the chosen valve as being reached.
nsmallestnodeforvalve(N1,D1) :- smallestvalve(V,D1), reached(N,D), D1=D-1, useablelink(N,N1,V), useablelink(N,N2,V), N1 > N2.

smallestnodeforvalve(N1,D1) :- smallestvalve(V,D1), reached(N,D), D1=D-1, useablelink(N,N1,V), not nsmallestnodeforvalve(N1,D1).

reached(N,D) :- smallestnodeforvalve(N,D).