#option --dlp --true-negation --totalize-negations
%
% bw.lp -- Blocks world planning (the Sussman Anomaly example)
%
% Adopted from a satplan representation by Tomi Janhunen for
% "instantiate -c t=<time steps> bw.lp | gnt2"
%
% Predicates that implement the operator MOVE(X,Y,Z,T):
%
% object(X,T)      -- object X is moved at time step T
% source(Y,T)      -- the object to be moved is on Y at time step T
% destination(Z,T) -- after the move at time step the object is on Z
%
% Fluents (predicates that describe state):
%
% on(X,Y,T)        -- object X is on Y at time step T
% clear(X,T)       -- no object is X at time step T

% Domain predicates (which are used to determine which
% instances of the clauses are actually needed):

time(0..t).

movable(a).
movable(b).
movable(c).
fixed(table).
block(X) :- movable(X).
block(X) :- fixed(X).

% Hide some atoms; not to be listed when a model is printed

hide time(T).
hide block(X).
hide movable(X).
hide fixed(X).

% Initial state

on(a,b,0).
on(b,table,0).
on(c,table,0).

-on(a,X,0) :- block(X), X != b.
-on(b,X,0) :- block(X), X != table.
-on(c,X,0) :- block(X), X != table.
-on(X,b,0) :- block(X), X != a.
-on(X,table,0) :- block(X), X != b, X != c.

clear(a,0).
clear(c,0).
-clear(b,0).
-clear(table,0).

% Final state

on(b,c,t).
on(c,a,t).
on(a,table,t).

% Hide further atoms

hide on(X,Y,T).
hide clear(X,T).
hide source(X,T).

% Effects of an action are implied by the action

-object(X,T) | -destination(Y,T) | on(X,Y,T+1) :-
	movable(X), block(Y), X != Y, time(T), time(T+1).

-object(X,T) | -source(Y,T) | -on(X,Y,T+1) :-
	movable(X), block(Y), X != Y, time(T), time(T+1).

-source(X,T) | clear(X,T+1) :-
	movable(X), time(T), time(T+1).

-destination(X,T) | -clear(X,T+1) :-
	movable(X), time(T), time(T+1).

% Preconditions of an action are implied by the action

-object(X,T) | -source(Y,T) | on(X,Y,T) :-
	movable(X), block(Y), X != Y, time(T), T < t.

-object(X,T) | clear(X,T) :-
	movable(X), time(T), T < t.

-destination(X,T) | clear(X,T) :-
	movable(X), time(T), T < t.

% Frame axioms; positive persistence

destination(X,T) | -clear(X,T) | clear(X,T+1) :-
	movable(X), time(T), time(T+1).

object(X,T) | -on(X,Y,T) | on(X,Y,T+1) :-
	movable(X), block(Y), X != Y, time(T), time(T+1).

% Frame axioms; negative persistence

source(X,T) | clear(X,T) | -clear(X,T+1) :-
	movable(X), time(T), time(T+1).

object(X,T) | on(X,Y,T) | -on(X,Y,T+1) :-
	movable(X), block(Y), X != Y, time(T), time(T+1).

destination(Y,T) | on(X,Y,T) | -on(X,Y,T+1) :-
	movable(X), block(Y), X != Y, time(T), time(T+1).
	
% Some action occurs every time

{ object(X,T): movable(X) } :- time(T), T < t.
{ source(X,T): block(X) } :- time(T), T < t.
{ destination(X,T): block(X) } :- time(T), T < t.

% Exclusivity: only one action occurs at a time

-object(X,T) | -object(Y,T) :-
	movable(X), movable(Y), X !=Y, time(T), T < t.

-source(X,T) | -source(Y,T) :-
	block(X), block(Y), X != Y, time(T), T < t.

-destination(X,T) | -destination(Y,T) :-
	block(X), block(Y), X != Y, time(T), T < t.

% Reasonable moves (object, source and destination are distinct)

-object(X,T) | -source(X,T) :-
	movable(X), time(T), T < t.

-object(X,T) | -destination(X,T) :-
	movable(X), time(T), T < t.

-source(X,T) | -destination(X,T) :-
	movable(X), time(T), T < t.

% On-axioms: antisymmetry and irreflexivity

-on(X,Y,T) | -on(Y,X,T) :-
	block(X), block(Y), X != Y, time(T).

-on(X,X,T) :-
	block(X), time(T).

% Only one thing on movables

-on(X,Y,T) | -on(Z,Y,T) :-
	movable(X), movable(Y), movable(Z), X != Y, X != Z, Y != Z, time(T).

% Movables are only on one thing

-on(X,Y,T) | -on(X,Z,T) :-
	movable(X), block(Y), block(Z), X != Y, X != Z, Y != Z, time(T).

% Movables can't be both clear and have something on them

-on(X,Y,T) | -clear(Y,T) :-
	movable(X), movable(Y), time(T).

% Fixed things are never on anything

-on(X,Y,T) :-
	fixed(X), block(Y), time(T).