%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% defining time
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

time(0..length).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% inertial rules
% for non-sensing action, whatever holds at (T)
% will hold at (T+1) if it has not been changed
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

holds(F, T+1):-
    time(T),
    literal(F), contrary(F, G),
    holds(F, T),
    not holds(G, T+1).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% action generation: at any moment of time, if the goal
% has not been satisfied, an action might or might not occur
% no parallel execution of actions is allowed
% the special action called null should never occured
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

nocc(A,T):- 
	time(T),  action(A), action(B), 
	neq(A,B), occ(B,T), not goal(T).

occ(A,T):- 
	time(T), T < length, action(A), possible(A,T),         
	not nocc(A,T), not goal(T).

:- time(T), occ(null,T).

:- time(T), fluent(F), holds(F, T), holds(neg(F), T).

action(null).

possible(null, T):- time(T).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% auxiliary axioms
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

literal(G):- fluent(G).
literal(neg(G)):- fluent(G).

contrary(F, neg(F)):- fluent(F).
contrary(neg(F), F):- fluent(F).

leq(T,T):- time(T).
leq(Tb,Te):- time(Tb), time(Te), Tb < Te.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% removing some predicates from the output
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

hide time(T).
hide action(A).
hide caused(F,L).
hide causes(A,F,L).
hide initially(F).
hide contrary(F,G).
hide fluent(F).
hide literal(L).
hide nocc(A,T).
hide goal(L).
hide set(S).
hide in(F,S).
hide leq(T1,T2).
hide possible(A,T).
hide executable(A, T).
%hide holds(F, T).

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