%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% This is a collection of general axioms for action theories %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Input Variables:

#domain step(S;S1;S2).
#domain fluent(Fl;Fl1;Fl2;Fl3).
#domain atomic(A;A0;A1;A2).       % atomic actions  SIMPLY ACTIONS??
#domain sequence(Seq;Seq1).       % sequences of atomic actions
#domain index(K;K1;K2;K3).        % index for elements of a sequence.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%   Executing  Defeasible Sequences  %%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% A (defeasible) sequence a = <a0,...a_{n-1}> of actions should be
% recorded as an array of atoms: 
% s(a1,1,a)....s(a_{n},n,a).
% length(a,n). 
% where 
%    s(A,I,Seq) says that A is the Ith element of sequence Seq.
% and where n is the length of the sequence. 

%%  starts(Seq,S)    -  sequence Seq starts at time step S (comes as input)
%%  planned(K,Seq,S) -  K'th component of sequence Seq is planned to occur at S
%%  o(K,Seq,S)       -  K'th component of sequence Seq occurs at  S
%%  ends(K,Seq,S)    -  the K'th component of sequence Seq ends at S
%%  ends(Seq,S)      -  sequence Seq ends at S

planned(1,Seq,S) :-          % execution of Seq starts with a 
          starts(Seq,S).     % plan to execute Seq's first component.

planned(K+1,Seq,S+1) :-      % Execution of K+1th component of Seq is planned 
           length(Seq,K1),   % immediately after the end of execution of ith
           K < K1,           % component
           o(K,Seq,S).

ends(K,Seq,S+1) :-           % Since components are atomic actions their executon 
          o(K,Seq,S).        % takes one step.

ends(Seq,S+1) :-             % execution of a sequence ends together with execution
          length(Seq,K),     % of its last component.
          o(K,Seq,S).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%       Axioms for Intentions        %%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

o(A,S) :- 
       planned(A,S),
       not -o(A,S).

planned(A,S+1) :-
            planned(A,S),
            not o(A,S),
            not -planned(A,S+1).

%%%%%%%   Since I could't come up with a good schema for 
%%%%%%%   naming elements of the sequence I duplicate
%%%%%%%   the above axioms.

o(K,Seq,S) :- 
       planned(K,Seq,S),
       not -o(K,Seq,S).

planned(K,Seq,S+1) :-
       planned(K,Seq,S),
       not o(K,Seq,S),
       not -planned(K,Seq,S+1).

% and add

o(A,S) :- 
      o(K,Seq,S),
      s(A,K,Seq).

-o(K,Seq,S) :-
      s(A,K,Seq),
      -o(A,S). 
      
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%              Inertia               %%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

h(Fl,S+1) :- 
      h(Fl,S),
      not -h(Fl,S+1). 

-h(Fl,S+1) :- 
      -h(Fl,S),
      not h(Fl,S+1). 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%           Reality  Check           %%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

o(A,S) :-
       hpd(A,S).

:- obs(Fl,S,f),
   h(Fl,S).

:- obs(Fl,S,t),
   -h(Fl,S).

%%%%%%%  Initial Situation %%%%%%

h(Fl,1) :- 
       obs(Fl,1,t).

-h(Fl,S) :- 
       obs(Fl,1,f).