\begin{verbatim}


%% block2-1.sm
%%
%% This program further modifies block2-0.sm in the way
%% executable is defined. In this program sets are used
%% in the definitions of executability.
%% This will take us to our next step when we want to
%% plan in presence of incomplete information.

 const length=5.
 time(1..length).


 block(a).
 block(b).
 block(c).
 block(table).

 initially(on(c,a)).
 initially(on(a,table)).
 initially(on(b,table)).
 initially(clear(c)).
 initially(clear(b)).
%initially(clear(table)).

 finally(on(b,c)).
 finally(on(a,b)).

not_goal(T):-
        time(T),
        literal(X),
        finally(X),
        not holds(X,T).

goal(T) :-
        time(T),
        not not_goal(T).


exists_plan :-
        goal(length).

:- not exists_plan.

%Defining sets

set(s1(X,Z))  :-
    block(X),
    block(Z).

set(s2).

set(s3(X,Y))     :-
    block(X),
    block(Y).

set(s4(X,Y))    :-
    block(X),
    block(Y).


% Definition of fluents & actions

fluent(on(X,Y)) :-
        block(X),
        block(Y).

fluent(clear(X)) :-
    block(X).

%action(puton(X,Y,Z)) :-
%        neq(X,Y),
%        neq(X,Z),
%        neq(Z,X),
%        block(X),
%        block(Y),
%        block(Z).

action(puton(X,Y)) :-
        neq(X,Y),
        block(X),
        block(Y).

%Effects of actions and executability conditions.

%  ;; Define step for placing one block on another.
%  (:action puton
%            :parameters (?X ?Y ?Z)
%            :precondition (and (on ?X ?Z) (clear ?X) (clear ?Y)
%                                (not (= ?Y ?Z)) (not (= ?X ?Z))
%                                (not (= ?X ?Y)) (not (= ?X Table)))
%            :effect
%            (and (on ?X ?Y) (not (on ?X ?Z))
%                  (when (not (= ?Z Table)) (clear ?Z))
%                  (when (not (= ?Y Table)) (not (clear ?Y))))))


%executable(puton(X,Y), T)   :-
%        block(X),
%        block(Y),
%        neq(X,Y),
%        neq(X,table),
%        neq(Y,table),
%        time(T),
%        T < length,
%        holds(clear(X), T),
%        holds(clear(Y), T).

exec(puton(X,Y), s3(X,Y)  )  :-
        block(X),
        block(Y),
        neq(X,Y),
        neq(X,table),
        neq(Y,table).

in(clear(X),s3(X,Y))    :-
        block(X),
        block(Y).

in(clear(Y),s3(X,Y))    :-
        block(X),
        block(Y).



%executable(puton(X,Y), T)   :-
%        block(X),
%        block(Y),
%        neq(X,Y),
%        eq(Y,table),
%        time(T),
%        T < length,
%        holds(clear(X), T).

exec(puton(X,Y), s4(X,Y)  )  :-
        block(X),
        block(Y),
        neq(X,Y),
        eq(Y,table).

in(clear(X),s4(X,Y))        :-
        block(X),
        block(Y).

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

%not_executable(A,T)         :-
%        action(A),
%        time(T),
%        set(S),
%        literal(L),
%        exec(A,S),
%        in(L,S),
%        not holds(L, T).

%executable(A,T)             :-
%        action(A),
%        time(T),
%        T < length,
%        not not_executable(A,T).

executable(A,T)             :-
        action(A),
        time(T),
        set(S),
        T < length,
        exec(A,S),
        holds_set(S,T).


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


causes(puton(X,Y), on(X,Y), s2) :-
        block(X),
        block(Y),
        neq(X,Y),
        neq(X,table).

causes(puton(X,Y), neg(on(X,Z)), s1(X,Z)) :-
        block(X),
        block(Y),
        block(Z),
        neq(X,Y),
        neq(X,Z),
        neq(Z,Y).

in(on(X,Z), s1(X,Z)  ) :-
        block(X),
        block(Z),
        neq(X,Z).


%%
%% The above two rules encode causal rules of the form
%% a causes f  if l_1, .. l_n
%% by writing
%% causes(a, f, s), and in(l_1, s), ..., in(l_n, s)
%%

causes(puton(X,Y), clear(Z), s1(X,Z)) :-
        block(X),
        block(Y),
        block(Z),
        neq(X,Y),
        neq(X,Z),
        neq(Z,Y),
        neq(Z,table),
        neq(X,table).

causes(puton(X,Y), neg(clear(Y)), s2) :-
        block(X),
        block(Y),
        neq(X,Y),
        neq(Y,table),
        neq(X,table).

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


literal(G)  :-
    fluent(G).

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

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

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


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

not_holds_set(S, T)   :-
    set(S),
    time(T),
    literal(L),
    in(L,S),
    not holds(L,T).

holds_set(S, T)        :-
    set(S),
    time(T),
    not not_holds_set(S,T).


holds(F, 1) :-
    literal(F),
    initially(F).


holds(F, T+1)   :-
    literal(F),
    time(T),
    set(S),
    T < length,
    action(A),
    executable(A,T),
    occurs(A,T),
    causes(A,F,S),
    holds_set(S,T).

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


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

possible(A,T)   :-
    action(A),
    time(T),
    executable(A,T),
    not goal(T).

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

occurs(A,T) :-
    action(A),
    time(T),
    possible(A,T),
    not not_occurs(A,T).

not_occurs(A,T) :-
    action(A),
    action(AA),
    neq(A,AA),
    time(T),
    occurs(AA,T).


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

 hide time(T).
 hide action(A).
 hide causes(A,F,S).
 hide initially(F).
 hide contrary(F,G).
 hide fluent(F).
 hide literal(L).
 hide executable(A,T).
 hide holds(F,T).
 hide not_occurs(A,T).
 hide possible(A,T).
 hide possible1(A,T).
 hide possible2(A,T).
 hide block(X).
 hide exists_plan.
 hide finally(X).
 hide goal(T).
 hide not_goal(T).
 hide set(S).
 hide in(X,Y).
 hide holds_set(X,Y).
 hide not_holds_set(X,Y).
 hide exec(A,S).
% hide not_executable(A,T).

\end{verbatim}