holds(on(c,a),s0).
holds(ontable(a),s0).
holds(ontable(b),s0).
holds(clear(c),s0).
holds(clear(b),s0).
holds(handempty,s0).

% Effetti dell'azione move(X,Y,Z) (Post)

% holds(clear(Y),do1(move(X,Y,Z),S)).
% holds(on(X,Z),do1(move(X,Y,Z),S)).


% Clausola che esprime le precondizioni dell'azione move(X,Y,Z) (Pre)

% pact(move(X,Y,Z),S):-holds(clear(X),S),holds(clear(Z),S),holds(on(X,Y),S),X\=Z.

% Clausola per esprimere le condizioni di frame (FA)

% holds(V,do1(move(X,Y,Z),S)):-holds(V,S),V\=clear(Z),V\=on(X,Y).

% Clausola per esprimere la raggiungibilità di uno stato (Meta-assioma)

poss(s0).
poss(do1(A,S)):-poss(S),pact(A,S).


% Clausola per esprimere le precondizioni dell'azione stack(X,Y) (Pre)
pact(stack(X,Y),S):-holds(clear(Y),S),holds(holding(X),S),X\=Y.


% Effetti dell'azione stack(X,Y) (Post)
holds(on(X,Y),do1(stack(X,Y),S)).
holds(handempty,do1(stack(X,Y),S)).
holds(clear(X),do1(stack(X,Y),S)).


% Clausola per esprimere le condizioni di frame di stack(X,Y) (FA)
holds(V,do1(stack(X,Y),S)):-holds(V,S),V\=clear(Y),V\=holding(X).


% Clausola per esprimere le precondizioni dell'azione unstack(X,Y) (Pre)
pact(unstack(X,Y),S):-holds(on(X,Y),S),holds(handempty,S),holds(clear(X),S),X\=Y.


% Effetti dell'azione unstack(X,Y) (Post)
holds(clear(Y),do1(unstack(X,Y),S)).
holds(holding(X),do1(unstack(X,Y),S)).


% Clausola per esprimere le condizioni di frame di unstack(X,Y) (FA)
holds(V,do1(unstack(X,Y),S)):-holds(V,S),V\=on(X,Y),V\=handempty,V\=clear(X).


% Clausola per esprimere le precondizioni dell'azione putdown(X) (Pre)
pact(putdown(X),S):-holds(holding(X),S).


% Effetti dell'azione putdown(X,Y) (Post)
holds(ontable(X),do1(putdown(X),S)).
holds(handempty,do1(putdown(X),S)).
holds(clear(X),do1(putdown(X),S)).


% Clausola per esprimere le condizioni di frame di putdown(X,Y) (FA)
holds(V,do1(putdown(X),S)):-holds(V,S),V\=holding(X).


% Clausola per esprimere le precondizioni dell'azione pickup(X) (Pre)
pact(pickup(X),S):-holds(ontable(X),S),holds(handempty,S),holds(clear(X),S).


% Effetti dell'azione pickup(X,Y) (Post)
holds(holding(X),do1(pickup(X),S)).


% Clausola per esprimere le condizioni di frame di pickup(X,Y) (FA)
holds(V,do1(pickup(X),S)):-holds(V,S),V\=ontable(X),V\=handempty,V\=clear(X).