:- set_flag(output_options, [depth(full)]).
%%%%%%%%% parameters %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
size(6,6).
start(3,3).
%%%%%%%%% implementation part %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%% flux related axioms %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
poss(move(_,_),_).
state_update(Z,move(Xp,Yp),Zp) :- holds(at(X,Y),Z),
update(Z,[at(Xp,Yp)],[at(X,Y),notVis(Xp,Yp)],Zp).
%%%%%%%%% flux interpreter for ALP %%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- local reference(state).
run(P,S) :- init(Z), setval(state, Z-s0), call(P),
getval(state, _-S).
?(not F) :- getval(state,Z-_), \+ holds(F,Z).
?(F) :- getval(state,Z-_), holds(F,Z).
do(A) :- getval(state,Z-S), poss(A,Z), state_update(Z,A,Z1),
setval(state,Z1-do(A,S)).
%%%%%%%%% special flux %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
holds(F, [F|_]).
holds(F, Z) :- Z=[F1|Z1], F\==F1, holds(F, Z1).
holds(F, [F|Z], Z).
holds(F, Z, [F1|Zp]) :- Z=[F1|Z1], F\==F1, holds(F, Z1, Zp).
minus_(Z, [], Z).
minus_(Z, [F|Fs], Zp) :-
(\+ holds(F, Z) -> Z1=Z ; holds(F, Z, Z1)),
minus_(Z1, Fs, Zp).
plus_(Z, [], Z).
plus_(Z, [F|Fs], Zp) :-
(\+ holds(F, Z) -> Z1=[F|Z] ; holds(F, Z), Z1=Z),
plus_(Z1, Fs, Zp).
update(Z1, ThetaP, ThetaN, Z2) :-
minus_(Z1, ThetaN, Z), plus_(Z, ThetaP, Z2).