% Blocks' world adopted from Ilkka Niemelä's representation
% (c) Tomi Janhunen
%
% usage: lparse -ck=<number of time steps> bw.lp | smodels 0

%%% Points of time %%%

time(0..k).

hide time(T).

%%% Initial situation %%%

on(a,b,0). on(b,c,0). on(c,f,0). on(d,f,0).
clear(a,0). clear(d,0).

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

%%% Final situation (after at most k actions) %%%

:- not on(b,a,k).

%%% Domain/auxiliary predicates %%%

block(a). block(b).  block(c). block(d).
object(X) :- block(X).

% The floor which cannot be moved, is never clear, and holds several blocks

object(f).

% Define objects that can hold blocks

can_hold(f,T) :- time(T).
can_hold(Z,T) :- clear(Z,T), block(Z), time(T).

% Triples of objects that are potentially subject to move operations

diff(X,Y,Z) :- X!=Z, X!=Y, Y!=Z, block(X), object(Y;Z).

hide block(X).
hide object(X).
hide can_hold(Z,T).
hide diff(X,Y,Z).

%%% Operator MOVE(X,Y,Z,T) %%%

move(X,Y,Z,T) :- clear(X,T), on(X,Y,T), can_hold(Z,T),
	not denied_move(X,Y,Z,T), diff(X,Y,Z), time(T), T<k.

on(X,Z,T+1) :- move(X,Y,Z,T), diff(X,Y,Z), time(T;T+1).

clear(Y,T+1) :- move(X,Y,Z,T), diff(X,Y,Z), Y!=f, time(T;T+1).

%%% Frame Axioms %%%

on(X,Y,T+1) :- on(X,Y,T), not remove_on(X,Y,T),
	block(X), object(Y), time(T;T+1).

remove_on(X,Y,T) :- move(X,Y,Z,T), diff(X,Y,Z), time(T), T<k.

clear(X,T+1) :- clear(X,T), not remove_clear(X,T),
	block(X), time(T;T+1).

remove_clear(Z,T) :- move(X,Y,Z,T), diff(X,Y,Z), Z!=f, time(T), T<k.

hide remove_on(X,Y,T).
hide remove_clear(X,T).

%%% Exceptions to obtain a linear order %%%

denied_move(X1,Y1,Z1,T) :- move(X2,Y2,Z2,T),
	diff(X1,Y1,Z1), diff(X2,Y2,Z2), X1!=X2, time(T), T<k.

denied_move(X1,Y1,Z1,T) :- move(X2,Y2,Z2,T),
	diff(X1,Y1,Z1), diff(X2,Y2,Z2), Y1!=Y2, time(T), T<k.

denied_move(X1,Y1,Z1,T) :- move(X2,Y2,Z2,T),
	diff(X1,Y1,Z1), diff(X2,Y2,Z2), Z1!=Z2, time(T), T<k.

% Self exceptions (to represent the NOOP operator)

denied_move(X,Y,Z,T) :- not move(X,Y,Z,T),
	diff(X,Y,Z), time(T), T<k.

hide denied_move(X,Y,Z,T).