Clingo ASP cargo problem

lp

%*
Init(At(C1, SFO) ∧ At(C2, JFK ) ∧ At(P1, SFO) ∧ At(P2, JFK )
	∧ Cargo(C1) ∧ Cargo(C2) ∧ Plane(P1) ∧ Plane(P2)
	∧ Airport(JFK ) ∧ Airport(SFO))

Goal(At(C1, JFK ) ∧ At(C2, SFO))

Action(Load(c, p, a),
	PRECOND: At(c, a) ∧ At(p, a) ∧ Cargo(c) ∧ Plane(p) ∧ Airport(a)
	EFFECT: ¬ At(c, a) ∧ In(c, p))

Action(Unload(c, p, a),
	PRECOND: In(c, p) ∧ At(p, a) ∧ Cargo(c) ∧ Plane(p) ∧ Airport(a)
	EFFECT: At(c, a) ∧ ¬ In(c, p))

Action(Fly(p, from, to),
	PRECOND: At(p, from) ∧ Plane(p) ∧ Airport(from) ∧ Airport(to)
	EFFECT: ¬ At(p, from) ∧ At(p, to))
*%

%*

in(C, P), il cargo C è nell'aero P.
at(X, A), l'oggetto X (sia aereo che cargo) è all'aereoporto A. 

*%

%% DEFINE

% The DEFINE sections expresses additional concepts and connects the GENERATE and TEST parts.

#include <incmode>.

#program base.

cargo(c1; c2).

plane(p1; p2).

airport(jfk; sfo).

init(in(c1,sfo)). % il cargo c1 è nell'aereoporto sfo.
init(in(c2,jfk)). % il cargo c2 è nell'aereoporto jfk.
init(at(p1,sfo)). % l'aereo p1 è nell'aereoporto sfo.
init(at(p2,jfk)). % l'aereo p2 è nell'aereoporto jfk.

goal(at(c1,jfk)). % il cargo c1 è nell'aereoporto jfk.
goal(at(c2,sfo)). % il cargo c2 è nell'aereporto sfo.

holds(F, 0) :- init(F).

%% GENERATE

% The GENERATE parts defines a large collection of answer sets that could be seen as potential solutions.
% Choice rules are typically the main members of the GENERATE part of the program.

#program step(t).

%0 { load(C, P, A, t): cargo(C), plane(P), airport(A) } 1.
%0 { unload(C, P, A, t): cargo(C), plane(P), airport(A) } 1.
%0 { fly(P, FROM, TO, t): plane(P), airport(FROM), airport(TO), FROM != TO } 1.

%1 { load(C, P, A, t): cargo(C), plane(P), airport(A); unload(C, P, A, t): cargo(C), plane(P), airport(A); fly(P, FROM, TO, t): plane(P), airport(FROM), airport(TO), FROM != TO}.

%{ load(C, P, A, t): cargo(C), plane(P), airport(A); unload(C, P, A, t): cargo(C), plane(P), airport(A); fly(P, FROM, TO, t): plane(P), airport(FROM), airport(TO), FROM != TO} = 1.

0 { load(C, P, A, t): cargo(C), plane(P), airport(A) } 1.% :- goal(t - 1), t <= n. 
0 { unload(C, P, A, t): cargo(C), plane(P), airport(A) } 1.% :- goal(t - 1), t <= n.
0 { fly(P, FROM, TO, t): plane(P), airport(FROM), airport(TO), FROM != TO } 1.%:- goal(t - 1), t <= n. 

holds(F, t) :- holds(F, t - 1), not -holds(F, t).
-holds(F, t) :- -holds(F, t - 1), not holds(F, t).

% Azione Load.
% Se effettuo una azione di load di un cargo sull'aereoplano, il cargo P si troverà sull'aereo P.
holds(in(C, P), t) :- cargo(C), plane(P), load(C, P, A, t).
-holds(at(C, A), t) :- cargo(C), airport(A), load(C, P, A, t).

% Azione Unload.
% 
holds(at(C, A), t) :- cargo(C), airport(A), unload(C, P, A, t).
-holds(in(C, P), t) :- cargo(C), plane(P), unload(C, P, A, t).

% Azione Fly.
% 
holds(at(P, TO), t) :- fly(P, FROM, TO, t).
-holds(at(P, FROM), t) :- fly(P, FROM, TO, t).

%% TEST

% The TEST part consists of rules that eliminate the answer sets of the GENERATE part that do not correspond to solutions.
% Constraints often form the TEST section of a program.

% Constraints su load.
% Escludo l'azione di load al tempo t se il cargo C si trova nell'aereoporto A1 al tempo t - 1 e l'aereo P si trova nell'aereoporto A2 e A1 è diverso da A2.
:- load(C, P, A, t), holds(at(C, A1), t - 1), holds(at(P, A2), t - 1), A1 != A2.
% Escludo l'azione di load al tempo t se il cargo C non si trova nello stesso aereoporto dell'aereo P.
:- load(C, P, A, t), holds(at(C, A1), t - 1), A != A1.
% Escludo l'azione di load al tempo t se l'aereo P non si trova nello stesso aereoporto del cargo C.
:- load(C, P, A, t), holds(at(P, A2), t - 1), A != A2.
% Escludo l'azione di load al tempo t se ho già caricato al tempo t - 1 senza aver prima scaricato.
:- load(C, P, A, t), holds(in(_, P), t - 1).
% Escludo l'azione di load al tempo t se al tempo t - 1 ho caricato lo stesso cargo.
:- load(C, P, A, t), holds(in(C, _), t - 1).

% Constraints su unload.
% Escludo l'azione di unload se l'aereo P non si trova nell'aereoporto A.
:- unload(C, P, A, t), not holds(at(P, A), t - 1).
% Escludo l'azione di unload se il cargo C non è un su P.
:- unload(C, P, A, t), not holds(in(C, P), t - 1).

% Constraints su fly.
% Se l'aereo P non si trova nell'aereoporto FROM, allora non può volare dall'aereoporto FROM all'aereoporto TO.
:- fly(P, FROM, TO, t), not holds(at(P, FROM), t - 1).

% Numero massimo di azioni ogni istante.
%:- 0 {load(C, P, A, t): cargo(C), plane(P), airport(P) ; unload(C, P, A, t): cargo(C), plane(P), airport(P); fly(C, P, A, t): cargo(C), plane(P), airport(P) } 1.
:- 2 {load(_, _, _, t); unload(_, _, _, t); fly(_, _, _, t)}.

#program check(t).

:- query(t), goal(F), not holds(F, t).
%:- goal(n).

%% OUTPUT

#show load/4.
#show fly/4.
#show unload/4.

%_minimize(1, t) :- goal(t).