planning1.dl
------------


%Conformant planning.
% a causes f if p; a causes f if ~p; b causes ~f.
% initially ~f; goal f. plan should be: a.
% goal f


time(1).

action(a).
action(b).

fluent(f).
fluent(p).
fluent(ff).
fluent(pp).

initially(ff).

holds(F,1) :- fluent(F),	initially(F).

opp(f,ff).
opp(ff,f).
opp(p,pp).
opp(pp,p).

holds(F, TT)	:- 	fluent(F),
			fluent(FF),
			opp(F,FF),
			time(T),
			TT = T + 1,
			holds(F,T), 
			not holds(FF, TT).

holds(f, TT)	:-	time(T),
			occurs(a,T),
			TT = T + 1,
			holds(p,T).

holds(f, TT)   :-      time(T),
			TT = T +1,
                        occurs(a,T),
                        holds(pp,T).

holds(ff, TT)  :-	time(T),
			TT = T + 1,
			occurs(b,T).

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

%occurs(a,1) | not_occurs(a,1).

%occurs(b,1) | not_occurs(b,1).

%	:-	occurs(a,1),
%		occurs(b,1).

not_occurs(A,T)	:- action(A),	
		   time(T),
		   action(B),
		   A != B,
		   occurs(B,T).

occurs(A,T)	:- action(A),
		   time(T),
		   not not_occurs(A,T).

holds(p,1) | holds(pp, 1).

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

goal_sat :-	holds(f,2).

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

holds(f,1)	:-	goal_sat.
holds(ff,1) 	:-      goal_sat.
holds(p,1)      :-      goal_sat.
holds(pp,1) 	:-      goal_sat.

holds(f,2)      :-      goal_sat.
holds(ff,2) 	:-      goal_sat.
holds(p,2)      :-      goal_sat.
holds(pp,2) 	:-      goal_sat.

%goal_sat ?

***************************************************************
dlv -N=20 planning1.dl > p1-models.tr


dlv [build BEN/Apr  5 2000   gcc 2.95.2 19991024 (release)]

{time(1), action(a), action(b), fluent(f), fluent(p), 
fluent(ff), fluent(pp), initially(ff), 
opp(f,ff), opp(p,pp), opp(ff,f), opp(pp,p), holds(ff,1), 
not_occurs(a,1), occurs(b,1), holds(ff,2), holds(pp,1), holds(pp,2)}

{time(1), action(a), action(b), fluent(f), fluent(p), 
fluent(ff), fluent(pp), initially(ff), opp(f,ff), 
opp(p,pp), opp(ff,f), opp(pp,p), holds(ff,1), 
not_occurs(a,1), occurs(b,1), holds(ff,2), holds(p,1), holds(p,2)}

{time(1), action(a), action(b), fluent(f), fluent(p), 
fluent(ff), fluent(pp), initially(ff), opp(f,ff), 
opp(p,pp), opp(ff,f), opp(pp,p), holds(ff,1), occurs(a,1), 
not_occurs(b,1), holds(ff,2), holds(p,1), holds(pp,1), 
holds(f,2), holds(p,2), holds(pp,2), goal_sat, holds(f,1)}

**************************************************************

vi planning1.dl %removed the comment from the query

dlv -N=20 -FB planning1.dl > p1-answer.tr


dlv [build BEN/Apr  5 2000   gcc 2.95.2 19991024 (release)]

goal_sat is bravely true, evidenced by {time(1), action(a), 
action(b), fluent(f), fluent(p), fluent(ff), fluent(pp), 
initially(ff), opp(f,ff), opp(p,pp), opp(ff,f), opp(pp,p), 
holds(ff,1), occurs(a,1), not_occurs(b,1), 
holds(ff,2), holds(p,1), holds(pp,1), holds(f,2), 
holds(p,2), holds(pp,2), goal_sat, holds(f,1)}


****************************************************************
****************************************************************

planning2.dl
------------



%Conformant planning.
% a causes f if p;  b causes ~f.
% initially ~f; goal f. plan should be: a.
% goal f


time(1).

action(a).
action(b).

fluent(f).
fluent(p).
fluent(ff).
fluent(pp).

initially(ff).

holds(F,1) :- fluent(F),	initially(F).

opp(f,ff).
opp(ff,f).
opp(p,pp).
opp(pp,p).

holds(F, TT)	:- 	fluent(F),
			fluent(FF),
			opp(F,FF),
			time(T),
			TT = T + 1,
			holds(F,T), 
			not holds(FF, TT).

holds(f, TT)	:-	time(T),
			occurs(a,T),
			TT = T + 1,
			holds(p,T).

%holds(f, TT)   :-      time(T),
%			TT = T +1,
%                        occurs(a,T),
%                        holds(pp,T).

holds(ff, TT)  :-	time(T),
			TT = T + 1,
			occurs(b,T).

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

%occurs(a,1) | not_occurs(a,1).

%occurs(b,1) | not_occurs(b,1).

%	:-	occurs(a,1),
%		occurs(b,1).

not_occurs(A,T)	:- action(A),	
		   time(T),
		   action(B),
		   A != B,
		   occurs(B,T).

occurs(A,T)	:- action(A),
		   time(T),
		   not not_occurs(A,T).

holds(p,1) | holds(pp, 1).

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

goal_sat :-	holds(f,2).

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

holds(f,1)	:-	goal_sat.
holds(ff,1) 	:-      goal_sat.
holds(p,1)      :-      goal_sat.
holds(pp,1) 	:-      goal_sat.

holds(f,2)      :-      goal_sat.
holds(ff,2) 	:-      goal_sat.
holds(p,2)      :-      goal_sat.
holds(pp,2) 	:-      goal_sat.

%goal_sat ?

************************************************

dlv -N=20 planning2.dl > p2-models.tr


dlv [build BEN/Apr  5 2000   gcc 2.95.2 19991024 (release)]

{time(1), action(a), action(b), fluent(f), fluent(p), 
fluent(ff), fluent(pp), initially(ff), opp(f,ff), 
opp(p,pp), opp(ff,f), opp(pp,p), holds(ff,1), not_occurs(a,1), 
occurs(b,1), holds(ff,2), holds(p,1), holds(p,2)}

{time(1), action(a), action(b), fluent(f), fluent(p), 
fluent(ff), fluent(pp), initially(ff), opp(f,ff), opp(p,pp), 
opp(ff,f), opp(pp,p), holds(ff,1), occurs(a,1), not_occurs(b,1), 
holds(ff,2), holds(pp,1), holds(pp,2)}

{time(1), action(a), action(b), fluent(f), fluent(p), 
fluent(ff), fluent(pp), initially(ff), opp(f,ff), 
opp(p,pp), opp(ff,f), opp(pp,p), holds(ff,1), not_occurs(a,1), 
occurs(b,1), holds(ff,2), holds(pp,1), holds(pp,2)}

****************************************************************

vi planning2.dl %removed the comment from the query

dlv -N=20 -FB planning2.dl > p2-answer.tr


dlv [build BEN/Apr  5 2000   gcc 2.95.2 19991024 (release)]

goal_sat is bravely false.

****************************************************************

In both planning1.dl and planning2.dl if we 
has at the end

:- not goal_sat

and then ran 
	dlv -N=20 planning1.dl and
	dlv -N=20 planning2.dl 
respectively, then in teh first case we would get
one answer set where goal_sat is true, while in the second
case we will not get any answer set.

****************************************************************