1/*
    2
    3   ABDUCTIVE EVENT CALCULUS
    4
    5   MURRAY SHANAHAN
    6
    7   Version 1.15
    8
    9   July 1998
   10
   11   Written for LPA MacProlog 32
   12
   13*/
   14
   15:- include(ec_common).   16
   17/*
   18   This is an abductive meta-interpreter for abduction with negation-as-
   19   failure, with built-in features for handling event calculus queries.
   20   In effect this implements a partial-order planner. not(clipped) facts
   21   correspond to protected links. The planner will also perform
   22   hierarchical decomposition, given definitions of compound events
   23   (happens if happens clauses).
   24
   25   The form of queries is as follows.
   26
   27        abdemo(Goals,Residue)
   28
   29   Goals is a list of atoms. Residue is a pair of [RH,RB], where RH is a
   30   list of happens facts and RB is a list of temporal ordering facts.
   31   Negations is a list of lists of atoms.
   32
   33   Roughly speaking, the above formulae should hold if,
   34
   35        EC and CIRC[Domain] and CIRC[Residue] |= Goals
   36
   37   where EC is the event calculus axioms, CIRC[Domain] is the completion
   38   of initiates, terminates and  releases, and CIRC[Residue] is the
   39   completion of happens. (Note that completion isn't applied to temporal
   40   ordering facts.)
   41
   42   F is expected to be fully bound when we call abdemo(holds_at(F,T)).
   43   It's assumed that all primitive actions (two argument happens) are
   44   in the residue (ie: none are in the program).
   45
   46   Although the interpreter will work with any logic program, the axioms of
   47   the event calculus are compiled in to the meta-level.
   48
   49   The function symbol "neg" is introduced to represent classically
   50   negated fluents. holds_at(neg(F)) corresponds to not holds_at(F)
   51   (with classical "not"). terminates formulae play a role in clipping
   52   positive fluents and initiating negative fluents. Conversely,
   53   initiates formulae play a role in clipping negative fluents and
   54   initiating positive ones.
   55
   56   Computation interleaves search (abdemo) and refinement phases. After each
   57   step of the computation, where a step is an iteration of abdemo or a
   58   refinement, the residue so far plus the remaining goal list entail the goal
   59   state. In other words, these computational steps are also proof steps.
   60
   61   An iterative deepening search strategy is employed, where depth
   62   corresponds to length of plan.
   63*/
   64
   65/* TOP LEVEL */
   66
   67
   68/*
   69   Top level calls to abdemo have to be transformed to the following form.
   70
   71        abdemo_top(Goals,ResidueIn,ResidueOut,NegationsIn,NegationsOut,DepthBound)
   72
   73   The residue has the form [[HA,HC],[BA,BC]], where HA is a list of happens
   74   atoms, HC is the transistive closure of the before-or-equal relation on times
   75   that follows from HA, BA is a list of before atoms, and BC is the transitive
   76   closure of BA.
   77*/
   78first_d(1000).
   79/*
   80%next_d(0). next_d(1).
   81%next_d(2). next_d(4).
   82next_d(32).  next_d(64). next_d(98).
   83next_d(D1, D2):- D1<5,!,D2 is D1+1.
   84next_d(D1, D2):- D1<9,!,D2 is D1+2.
   85next_d(D1, D2):- next_d(D2),D2>D1,!.
   86next_d(D1, D2):- D2 is D1+200.
   87%next_d(D1, D2):- D2 is (D1+7).
   88*/
   89
   90abdemo_special(long,Gs,R):-abdemo_timed(Gs,R).
   91abdemo_special(_,Gs,R):- abdemo(Gs,R).
   92
   93abdemo(Gs,[HA,BA]) :-
   94     init_gensym(t), first_d(D),
   95     abdemo_top(Gs,[[[],[]],[[],[]]],[[HA,HC],[BA,BC]],[],N,D),
   96     write_plan_len(HA,BA).
   97
   98abdemo_timed(Gs,[HA,BA]) :-
   99     ticks(Z1),
  100     abdemo(Gs,[HA,BA]),
  101     write_plan(HA,BA),
  102     ticks(Z2), Z is (Z2-Z1)/60, write('Total time taken '), writenl(Z), nl.
  103
  104
  105abdemo_top(Gs,R1,R3,N1,N3,D) :-
  106     abdemo_id(Gs,R1,R2,N1,N2,D), !, abdemo_cont(R2,R3,N2,N3).
  107
  108
  109/*
  110   abdemo_cont carries out one step of refinement, if necessary. It then
  111   resumes abdemo, but with an initial depth bound equal to the length of
  112   the plan so far. Obviously to start from 1 again would be pointless.
  113*/
  114
  115abdemo_cont([[HA,TC],RB],[[HA,TC],RB],N,N) :- all_executable(HA), !.
  116
  117abdemo_cont([[HA,HC],[BA,BC]],R2,N1,N3) :-
  118     write('Abstract plan: '), write(HA), writenl(BA), nl,
  119     refine([[HA,HC],[BA,BC]],N1,Gs,R1,N2), action_count([[HA,HC],[BA,BC]],D),
  120     abdemo_top(Gs,R1,R2,N2,N3,D).
  121
  122
  123/* abdemo_id is an iterative deepening version of abdemo. */
  124
  125abdemo_id(Gs,R1,R2,N1,N2,D) :-
  126     write(' DMS'), write(D), write(' '), abdemo(Gs,R1,R2,N1,N2,D).
  127
  128abdemo_id(Gs,R1,R2,N1,N2,D1) :- D2 is D1+1, abdemo_id(Gs,R1,R2,N1,N2,D2).
  129
  130
  131all_executable([]).
  132
  133all_executable([happens(A,T1,T2)|R]) :- executable(A), all_executable(R).
  134
  135
  136
  137
  138/* ABDEMO */
  139
  140
  141/*
  142   abdemo/6 is a depth bounded abdemo. It fails if it can't generate a plan
  143   with DepthBound or fewer steps. Calls to abdemo/6 have the following form.
  144
  145        abdemo(Goals,ResidueIn,ResidueOut,
  146             NegationsIn,NegationsOut,DepthBound)
  147
  148*/
  149
  150abdemo(Gs,[[HA,TC1],[BA,TC2]],R,N1,N2,D) :-
  151     trace(on), write('Goals: '), writenl(Gs),
  152     write('Happens: '), writenl(HA),
  153     write('Befores: '), writenl(BA),
  154     write('Nafs: '), writenl(N1), nl, nl, fail.
  155
  156abdemo([],R,R,N,N,D).
  157
  158/*
  159   Now we have two clauses which are meta-level representations of the two
  160   event calculus axioms for holds_at.
  161
  162        holds_at(F,T) <- initially(F) and not clipped(0,F,T)
  163
  164        holds_at(F,T3) <-
  165             happens(A,T1,T2) and T2 < T3 and
  166             initiates(A,F,T1) and not clipped(T1,F,T2)
  167
  168   Note the way the object-level axioms have been compiled into the
  169   meta-level. Note also that happens goals are not resolved against
  170   clauses in the object-level program. Instead, they're put straight into
  171   the residue. Resolving happens goals is the job of the refinement phase.
  172*/
  173
  174abdemo([holds_at(F1,T)|Gs1],R1,R3,N1,N4,D) :-
  175     F1 \= neg(F2), abresolve(initially(F1),R1,Gs2,R1,B),
  176     append(Gs2,Gs1,Gs3), add_neg([clipped(0,F1,T)],N1,N2),
  177     abdemo_naf([clipped(0,F1,T)],R1,R2,N2,N3,D),
  178     abdemo(Gs3,R2,R3,N3,N4,D).
  179
  180/*
  181   The order in which resolution steps are carried out in the next
  182   clause is crucial. We resolve initiates first in order to instantiate 
  183   A, but we don't want to proceed with sub-goals of initiates until
  184   we've added the corresponding happens and before facts to the residue.
  185*/
  186
  187abdemo([holds_at(F1,T3)|Gs1],R1,R6,N1,N5,D) :-
  188     F1 \= neg(F2), abresolve(initiates(A,F1,T1),R1,Gs2,R1,B1),
  189     abresolve(happens(A,T1,T2),R1,[],R2,B2),
  190     check_depth(R2,D),
  191     abresolve(before(T2,T3),R2,[],R3,B3),
  192     append(Gs2,Gs1,Gs3), check_nafs(B2,N1,R3,R4,N1,N2,D),
  193     add_neg([clipped(T1,F1,T3)],N2,N3),
  194     abdemo_naf([clipped(T1,F1,T3)],R4,R5,N3,N4,D),
  195     abdemo(Gs3,R5,R6,N4,N5,D).
  196
  197/*
  198   The next two clauses are a meta-level representation of the two
  199   event calculus axioms for not holds_at.
  200
  201        not holds_at(F,T) <- initiallyn(F) and not declipped(0,F,T)
  202
  203        not holds_at(F,T3) <-
  204             happens(A,T1,T2) and T2 < T3 and
  205             terminates(A,F,T1) and not declipped(T1,F,T2)
  206*/
  207
  208abdemo([holds_at(neg(F),T)|Gs1],R1,R3,N1,N4,D) :-
  209     abresolve(initially(neg(F)),R1,Gs2,R1,B),
  210     append(Gs2,Gs1,Gs3), add_neg([declipped(0,F,T)],N1,N2),
  211     abdemo_naf([declipped(0,F,T)],R1,R2,N2,N3,D),
  212     abdemo(Gs3,R2,R3,N3,N4,D).
  213
  214abdemo([holds_at(neg(F),T3)|Gs1],R1,R6,N1,N5,D) :-
  215     abresolve(terminates(A,F,T1),R1,Gs2,R1,B1),
  216     abresolve(happens(A,T1,T2),R1,[],R2,B2),
  217     check_depth(R2,D),
  218     abresolve(before(T2,T3),R2,[],R3,B3),
  219     append(Gs2,Gs1,Gs3), check_nafs(B2,N1,R3,R4,N1,N2,D),
  220     add_neg([declipped(T1,F,T3)],N2,N3),
  221     abdemo_naf([declipped(T1,F,T3)],R4,R5,N3,N4,D),
  222     abdemo(Gs3,R5,R6,N4,N5,D).
  223
  224/*
  225   The next two clauses cater for happens goals.
  226
  227   Note that happens goals only appear either in the initial goal list or,
  228   in an "expand" goal, as a result of refinement. Note also that these
  229   clauses, because of the way abresolve(happens) works, will ensure sharing
  230   of sub-goals between compound events wherever possible.
  231*/
  232
  233abdemo([happens(A,T1,T2)|Gs],R1,R4,N1,N3,D) :-
  234     !, abresolve(happens(A,T1,T2),R1,[],R2,B), check_depth(R2,D),
  235     check_nafs(B,N1,R2,R3,N1,N2,D), abdemo(Gs,R3,R4,N2,N3,D).
  236
  237abdemo([happens(A,T)|Gs],R1,R4,N1,N3,D) :-
  238     !, abresolve(happens(A,T),R1,[],R2,B), check_depth(R2,D),
  239     check_nafs(B,N1,R2,R3,N1,N2,D), abdemo(Gs,R3,R4,N2,N3,D).
  240
  241/*
  242   The next clause deals with the expansion of compound actions. These appear
  243   as goals of the form expand([happens(A,T1,T2)|Bs]), where happens(A,T1,T2)
  244   is the compound action to be expanded and Bs is a list of "before" goals.
  245   These goals are placed in the goal list by calls to "refine". The various
  246   sub-goals generated by the expansion are treated in a careful order. First,
  247   the compound action's sub-actions are added to the residue. Then the "before"
  248   goals that "refine" took out of the residue are put back (with their newly
  249   skolemised time constants). The holds_at goals are solved next, on the
  250   assumption that they are either guards or supply context for the expansion.
  251   Then other, non event calculus goals are dealt with. Only then, with all the
  252   temporal ordering constraints sorted out, is it safe to tackle not(clipped)
  253   and not(declipped) goals, first those that are part of the compound action
  254   definition, then those recorded in the negations list.
  255*/
  256
  257abdemo([expand([happens(A,T1,T2)|Bs])|Gs1],R1,R8,N1,N8,D) :-
  258     !, axiom(happens(A,T1,T2),Gs2),
  259     add_sub_actions(Gs2,R1,R2,N1,N2,D,Hs),
  260     solve_befores(Bs,R2,R3,N2,N3,D),
  261     abdemo_holds_ats(Gs2,R3,R4,N3,N4,D),
  262     solve_other_goals(Gs2,R4,R5,N4,N5,D),
  263     check_clipping(Gs2,R5,R6,N5,N6,D),
  264     check_sub_action_nafs(Hs,N1,R6,R7,N6,N7,D),
  265     abdemo(Gs1,R7,R8,N7,N8,D).
  266
  267/*
  268   The last two clauses cater for the general case (ie: goals other
  269   than holds_at and happens). They're also used to tackle domain
  270   constraints (ie: holds_at if holds_at clauses).
  271*/
  272
  273abdemo([not(G)|Gs],R1,R3,N1,N4,D) :-
  274     !, abdemo_naf([G],R1,R2,N1,N2,D), add_neg([G],N2,N3),
  275     abdemo(Gs,R2,R3,N3,N4,D).
  276
  277abdemo([G|Gs1],R1,R3,N1,N2,D) :-
  278     abresolve(G,R1,Gs2,R2,B), append(Gs2,Gs1,Gs3),
  279     abdemo(Gs3,R2,R3,N1,N2,D).
  280
  281
  282check_depth(R,D) :- action_count(R,L), L =< D.
  283
  284
  285action_count([[HA,TC],RB],L) :- length(HA,L).
  286
  287
  288
  289
  290/* EXPANSION OF COMPOUND ACTIONS */
  291
  292
  293/* The following collection of predicates are called by abdemo(expand). */
  294
  295
  296abdemo_holds_ats([],R,R,N,N,D).
  297
  298abdemo_holds_ats([holds_at(F,T)|Gs],R1,R3,N1,N3,D) :-
  299     !, abdemo([holds_at(F,T)],R1,R2,N1,N2,D),
  300     abdemo_holds_ats(Gs,R2,R3,N2,N3,D).
  301
  302abdemo_holds_ats([G|Gs],R1,R2,N1,N2,D) :-
  303     abdemo_holds_ats(Gs,R1,R2,N1,N2,D).
  304
  305
  306solve_other_goals([],R,R,N,N,D).
  307
  308solve_other_goals([G|Gs],R1,R3,N1,N3,D) :-
  309     G \= holds_at(F,T), G \= happens(A,T1,T2),
  310     G \= happens(A,T), G \= before(T1,T2),
  311     G \= not(clipped(T1,F,T2)), G \= not(declipped(T1,F,T2)), !,
  312     abdemo([G],R1,R2,N1,N2,D),
  313     solve_other_goals(Gs,R2,R3,N2,N3,D).
  314
  315solve_other_goals([G|Gs],R1,R2,N1,N2,D) :-
  316     solve_other_goals(Gs,R1,R2,N1,N2,D).
  317
  318/*
  319   In its last argument, add_sub_actions accumulates a list of new actions
  320   added to the residue, so that subsequent re-checking of not(clipped) and
  321   not(declipped) goals can be done via check_nafs rather than the less
  322   efficient abdemo_nafs.
  323*/
  324
  325add_sub_actions([],R,R,N,N,D,[]).
  326
  327add_sub_actions([happens(A,T1,T2)|Gs],R1,R3,N1,N3,D,Hs2) :-
  328     !, abresolve(happens(A,T1,T2),R1,[],R2,B), check_depth(R2,D),
  329     add_sub_actions(Gs,R2,R3,N2,N3,D,Hs1), cond_add(B,happens(A,T1,T2),Hs1,Hs2).
  330
  331add_sub_actions([happens(A,T)|Gs],R1,R3,N1,N3,D,Hs2) :-
  332     !, abresolve(happens(A,T),R1,[],R2,B), check_depth(R2,D),
  333     add_sub_actions(Gs,R2,R3,N2,N3,D,Hs1), cond_add(B,happens(A,T,T),Hs1,Hs2).
  334
  335add_sub_actions([before(T1,T2)|Gs],R1,R3,N1,N3,D,Hs) :-
  336     !, abresolve(before(T1,T2),R1,[],R2,B),
  337     add_sub_actions(Gs,R2,R3,N2,N3,D,Hs).
  338
  339add_sub_actions([G|Gs],R1,R2,N1,N2,D,Hs) :-
  340     add_sub_actions(Gs,R1,R2,N1,N2,D,Hs).
  341
  342
  343cond_add(false,H,Hs,Hs) :- !.
  344
  345cond_add(true,H,Hs,[H|Hs]).
  346
  347
  348solve_befores([],R,R,N,N,D).
  349
  350solve_befores([before(T1,T2)|Gs],R1,R3,N1,N3,D) :-
  351     !, abdemo([before(T1,T2)],R1,R2,N1,N2,D),
  352     solve_befores(Gs,R2,R3,N2,N3,D).
  353
  354solve_befores([G|Gs],R1,R2,N1,N2,D) :-
  355     solve_befores(Gs,R1,R2,N1,N2,D).
  356
  357
  358check_sub_action_nafs([],N1,R,R,N2,N2,D) :- !.
  359
  360check_sub_action_nafs([happens(A,T1,T2)|Hs],N1,R1,R3,N2,N4,D) :-
  361     check_nafs(A,T1,T2,N1,R1,R2,N2,N3,D),
  362     check_sub_action_nafs(Hs,N1,R2,R3,N3,N4,D).
  363
  364
  365check_clipping([],R,R,N,N,D) :- !.
  366
  367check_clipping([not(clipped(T1,F,T2))|Gs],R1,R3,N1,N3,D) :-
  368     !, abdemo_naf([clipped(T1,F,T2)],R1,R2,N1,N2,D),
  369     check_clipping(Gs,R2,R3,N2,N3,D).
  370
  371check_clipping([not(declipped(T1,F,T2))|Gs],R1,R3,N1,N3,D) :-
  372     !, abdemo_naf([declipped(T1,F,T2)],R1,R2,N1,N2,D),
  373     check_clipping(Gs,R2,R3,N2,N3,D).
  374
  375check_clipping([G|Gs],R1,R2,N1,N2,D) :-
  376     check_clipping(Gs,R1,R2,N1,N2,D).
  377
  378
  379
  380
  381/* ABRESOLVE */
  382
  383
  384/*
  385   The form of a call to abresolve is as follows.
  386
  387        abresolve(Goal,ResidueIn,Goals,ResidueOut,Flag)
  388
  389   where Goals is the body of clause resolved with, and Flag is set to true
  390   if a happens fact has been added to the residue.
  391*/
  392
  393abresolve(terms_or_rels(A,F,T),R,Gs,R,false) :- axiom(releases(A,F,T),Gs).
  394
  395abresolve(terms_or_rels(A,F,T),R,Gs,R,false) :- !, axiom(terminates(A,F,T),Gs).
  396
  397abresolve(inits_or_rels(A,F,T),R,Gs,R,false) :- axiom(releases(A,F,T),Gs).
  398
  399abresolve(inits_or_rels(A,F,T),R,Gs,R,false) :- !, axiom(initiates(A,F,T),Gs).
  400
  401/*
  402   happens goals get checked to see if they are already in the residue.
  403   This permits the re-use of actions already in the residue. However,
  404   this decision may lead to later failure, in which case we try adding
  405   a new action to the residue.
  406
  407   happens goals aren't resolved against object-level program clauses.
  408   Only goals that are marked as expand(goal) are resolved against
  409   program clauses, and this is done by abdemo.
  410
  411   Time variables get skolemised, but not action variables because
  412   they end up getting instantiated anyway.
  413*/
  414
  415abresolve(happens(A,T),R1,Gs,R2,B) :- !, abresolve(happens(A,T,T),R1,Gs,R2,B).
  416
  417abresolve(happens(A,T1,T2),[[HA,TC],RB],[],[[HA,TC],RB],false) :-
  418     member(happens(A,T1,T2),HA).
  419
  420abresolve(happens(A,T,T),[[HA,TC],RB],[],[[[happens(A,T,T)|HA],TC],RB],B) :-
  421     executable(A), !, B = true, skolemise(T).
  422
  423abresolve(happens(A,T1,T2),R1,[],R2,B) :-
  424     !, B = true, skolemise(T1), skolemise(T2), add_happens(A,T1,T2,R1,R2).
  425
  426/*
  427   If either X or Y is not bound in a call to abresolve(before(X,Y)) then
  428   they get skolemised.
  429*/
  430
  431abresolve(before(X,Y),R,[],R,false) :-
  432     skolemise(X), skolemise(Y), demo_before(X,Y,R), !.
  433
  434abresolve(before(X,Y),R1,[],R2,B) :-
  435     !, B = false, skolemise(X), skolemise(Y), \+ demo_beq(Y,X,R1),
  436     add_before(X,Y,R1,R2).
  437
  438/*
  439   The predicates "diff" (meaning not equal) and "is" (for evaluating
  440   arithmetic expressions) are built in.
  441*/
  442
  443abresolve(diff(X,Y),R,[],R,false) :- !, X \= Y.
  444
  445abresolve(is(X,Y),R,[],R,false) :- !, X is Y.
  446
  447abresolve(G,R,[],[G|R],false) :- ec_abducible(G).
  448
  449abresolve(G,R,Gs,R,false) :- axiom(G,Gs).
  450
  451
  452
  453
  454/* ABDEMO_NAFS and CHECK_NAFS */
  455
  456
  457/*
  458   abdemo_nafs([G1...Gn],R1,R2) demos not(G1) and ... and not(Gn).
  459
  460   Calls to abdemo_naf have the following form.
  461
  462        abdemo_nafs(Negations,ResidueIn,ResidueOut,
  463             NegationsIn,NegationsOut,DepthIn,DepthOut)
  464
  465   where Negations is the list of negations to be established, ResidueIn
  466   is the old residue, ResidueOut is the new residue (abdemo_nafs can add
  467   both before and happens facts, as well as other abducibles, to the
  468   residue), NegationsIn is the old list of negations (same as Negations
  469   for top-level call), and NegationsOut is the new list of negations
  470   (abdemo_nafs can add new clipped goals to NegationsIn).
  471
  472   DepthIn and DepthOut keep track of the number of sub-goals generated,
  473   for iterative deepening purposes.
  474*/
  475
  476
  477abdemo_nafs([],R,R,N,N,D).
  478
  479abdemo_nafs([N|Ns],R1,R3,N1,N3,D) :-
  480     abdemo_naf(N,R1,R2,N1,N2,D), abdemo_nafs(Ns,R2,R3,N2,N3,D).
  481
  482
  483/*
  484   abdemo_naf([G1...Gn],R1,R2) demos not((G1) and ... and (Gn)).
  485
  486   As for abdemo, the main event calculus axioms are compiled into the
  487   meta-level in abdemo_naf. In addition to the two holds_at axioms, we
  488   have,
  489
  490        clipped(T1,F,T3) <-
  491             happens(A,T2) and T1 < T2 < T3 and
  492             [terminates(A,F,T2) or releases(A,F,T2)]
  493
  494        declipped(T1,F,T3) <-
  495             happens(A,T2) and T1 < T2 < T3 and
  496             [initiates(A,F,T2) or releases(A,F,T2)]
  497
  498   We have to use findall here, because all ways of achieving a goal
  499   have to fail for the goal itself to fail.
  500
  501   Note that only the two-argument version of happens is used, because
  502   the residue only contains instantaneous actions, and the effects of
  503   compound actions are assumed to match the effects of their
  504   component actions.
  505*/
  506
  507abdemo_naf([clipped(T1,F,T4)|Gs1],R1,R2,N1,N2,D) :-
  508     !, findall(Gs3,
  509          (abresolve(terms_or_rels(A,F,T2),R1,Gs2,R1,false),
  510          abresolve(happens(A,T2,T3),R1,[],R1,false),
  511          append([before(T1,T3),before(T2,T4)|Gs2],Gs1,Gs3)),Gss),
  512     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  513
  514abdemo_naf([declipped(T1,F,T4)|Gs1],R1,R2,N1,N2,D) :-
  515     !, findall(Gs3,
  516          (abresolve(inits_or_rels(A,F,T2),R1,Gs2,R1,false),
  517          abresolve(happens(A,T2,T3),R1,[],R1,false),
  518          append([before(T1,T3),before(T2,T4)|Gs2],Gs1,Gs3)),Gss),
  519     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  520
  521/*
  522   To show the classical negation of holds_at(F) (which is what we want), we
  523   have to show that holds_at(neg(F)). Conversely, to show the classical
  524   negation of holds_at(neg(F)) we have to show holds_at(F). Within a call
  525   to abdemo_naf, we can add both happens and before (and other abducibles)
  526   to the residue. This removes a potential source of incompleteness.
  527
  528   Note that F must be a ground term to preserve soundness and completeness.
  529   To guarantee this, all variables that occur in the body of an
  530   initiates, terminates or releases clause must occur in the fluent
  531   argument in its head.
  532*/
  533
  534/* DANGER: Cut in next clause rules out other ways to solve holds_at(F2,T). */
  535
  536abdemo_naf([holds_at(F1,T)|Gs1],R1,R3,N1,N3,D) :-
  537     opposite(F1,F2), copy_term(Gs1,Gs2),
  538     abdemo([holds_at(F2,T)],R1,R2,N1,N2,D), !,
  539     abdemo_naf_cont(R1,Gs2,R2,R3,N1,N3,D).
  540
  541abdemo_naf([holds_at(F,T)|Gs],R1,R2,N1,N2,D) :-
  542     !, abdemo_naf(Gs,R1,R2,N1,N2,D).
  543
  544/*
  545   Special facilities for handling temporal ordering facts are built in.
  546   We can add a before fact to the residue to preserve the failure of
  547   a clipped goal. The failure of a before goal does NOT mean that the
  548   negation of that goal is assumed to be true. (The Clark completion is
  549   not applicable to temporal ordering facts.) Rather, to make before(X,Y)
  550   fail, before(Y,X) has to follow. One way to achieve this is to add
  551   before(Y,X) to the residue.
  552*/
  553
  554abdemo_naf([before(X,Y)|Gs],R,R,N,N,D) :- X == Y, !.
  555
  556abdemo_naf([before(X,Y)|Gs],R,R,N,N,D) :- demo_before(Y,X,R), !.
  557
  558abdemo_naf([before(X,Y)|Gs1],R1,R2,N1,N2,D) :-
  559     !, append(Gs1,[postponed(before(X,Y))],Gs2),
  560     abdemo_naf(Gs2,R1,R2,N1,N2,D).
  561
  562/*
  563   A before fact is only added to the residue as a last resort. Accordingly,
  564   if we encounter a before(X,Y) goal and cannot show before(Y,X), we
  565   postpone that goal until we've tried other possibilities. A postponed
  566   before goal appears in the goal list as postponed(before(X,Y)).
  567*/
  568
  569abdemo_naf([postponed(before(X,Y))|Gs],R1,R2,N,N,D) :-
  570     \+ demo_beq(X,Y,R1), add_before(Y,X,R1,R2).
  571
  572abdemo_naf([postponed(before(X,Y))|Gs],R1,R2,N1,N2,D) :-
  573     !, abdemo_naf(Gs,R1,R2,N1,N2,D).
  574
  575/* 
  576   We drop through to the general case for goals other than special event
  577   calculus goals.
  578*/
  579
  580/* DANGER: Cut in next clause rules out other ways to solve G. */
  581
  582abdemo_naf([not(G)|Gs1],R1,R3,N1,N3,D) :-
  583     copy_term(Gs1,Gs2), abdemo([G],R1,R2,N1,N2,D), !,
  584     abdemo_naf_cont(R1,Gs2,R2,R3,N1,N3,D).
  585
  586abdemo_naf([not(G)|Gs],R1,R2,N1,N2,D) :- !, abdemo_naf(Gs,R1,R2,N1,N2,D).
  587
  588abdemo_naf([G|Gs1],R,R,N,N,D) :- \+ abresolve(G,R,Gs2,R,false), !.
  589
  590abdemo_naf([G1|Gs1],R1,R2,N1,N2,D) :-
  591     findall(Gs2,(abresolve(G1,R1,Gs3,R1,false),append(Gs3,Gs1,Gs2)),Gss),
  592     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  593
  594
  595/*
  596   abdemo_naf_cont gets an extra opportunity to succeed if the residue
  597   has been altered. This is determined by comparing R1 with R2. If
  598   a sub-goal has failed and the residue hasn't been altered, there's
  599   no need to look for other ways to prove the negation of the overall goal.
  600*/
  601
  602abdemo_naf_cont(R1,Gs,R2,R2,N,N,D).
  603
  604abdemo_naf_cont(R1,Gs,R2,R3,N1,N2,D) :-
  605     R1 \= R2, abdemo_naf(Gs,R1,R3,N1,N2,D).
  606
  607
  608/*
  609   check_nafs is just like abdemo_nafs, except that it only checks
  610   negated clipped and declipped facts against the most recent event
  611   added to the residue. To check one of these negations, not only can
  612   we confine our attention to the most recent event, but we can ignore
  613   that event if it doesn't fall inside the interval covered by the
  614   clipped/declipped in question. Of course, the negated clipped/declipped
  615   fact might depend on other holds_at facts. But their preservation is
  616   ensured because the clipped/declipped negation they themselves depend
  617   on will also be checked.
  618*/
  619
  620
  621check_nafs(false,N1,R,R,N2,N2,D) :- !. % 
  622
  623check_nafs(true,N,[[[happens(A,T1,T2)|HA],TC],RB],R,N1,N2,D) :-
  624     check_nafs(A,T1,T2,N,[[[happens(A,T1,T2)|HA],TC],RB],R,N1,N2,D).
  625
  626check_nafs(A,T1,T2,[],R,R,N,N,D).
  627
  628check_nafs(A,T1,T2,[N|Ns],R1,R3,N1,N3,D) :-
  629     check_naf(A,T1,T2,N,R1,R2,N1,N2,D),
  630     check_nafs(A,T1,T2,Ns,R2,R3,N2,N3,D).
  631
  632
  633check_naf(A,T2,T3,[clipped(T1,F,T4)],R1,R2,N1,N2,D) :-
  634     !, findall([before(T1,T3),before(T2,T4)|Gs],
  635          (abresolve(terms_or_rels(A,F,T2),R1,Gs,R1,false)),Gss),
  636     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  637
  638check_naf(A,T2,T3,[declipped(T1,F,T4)],R1,R2,N1,N2,D) :-
  639     !, findall([before(T1,T3),before(T2,T4)|Gs],
  640          (abresolve(inits_or_rels(A,F,T2),R1,Gs,R1,false)),Gss),
  641     abdemo_nafs(Gss,R1,R2,N1,N2,D).
  642
  643check_naf(A,T1,T2,N,R1,R2,N1,N2,D) :- abdemo_naf(N,R1,R2,N1,N2,D).
  644
  645
  646
  647
  648/* DEMO_BEFORE, ADD_BEFORE and ADD_HAPPENS */
  649
  650
  651/*
  652   demo_before simply checks membership of the transitive closure half of
  653   the temporal ordering part of the residue. Likewise demo_beq checks for
  654   demo_before or for membership of the transitive closure half of the
  655   happens part of the residue.
  656*/
  657
  658demo_before(0,Y,R) :- !, Y \= 0.
  659
  660demo_before(X,Y,[RH,[BA,TC]]) :- member(before(X,Y),TC).
  661
  662/* demo_beq is demo before or equal. */
  663
  664demo_beq(X,Y,R) :- X == Y, !.
  665
  666demo_beq(X,Y,R) :- demo_before(X,Y,R), !.
  667
  668demo_beq(X,Y,[[HA,TC],RB]) :- member(beq(X,Y),TC).
  669
  670
  671/*
  672   add_before(X,Y,R1,R2) adds before(X,Y) to the residue R1 giving R2.
  673   It does this by maintaining the transitive closure of the before and beq
  674   relations in R2, and assumes that R1 is already transitively closed.
  675   R1 and R2 are just the temporal ordering parts of the residue.
  676*/
  677
  678add_before(X,Y,[RH,[BA,TC]],[RH,[BA,TC]]) :- member(before(X,Y),TC), !.
  679
  680add_before(X,Y,[[HA,HC],[BA,BC1]],[[HA,HC],[[before(X,Y)|BA],BC2]]) :-
  681     \+ demo_beq(Y,X,[[HA,HC],[BA,BC1]]), find_bef_connections(X,Y,BC1,C1,C2),
  682     find_beq_connections(X,Y,HC,C3,C4), delete_abdemo(X,C3,C5), delete_abdemo(Y,C4,C6),
  683     append(C5,C1,C7), append(C6,C2,C8),
  684     cross_prod_bef(C7,C8,C9,BC1), append(C9,BC1,BC2).
  685
  686/*
  687   add_happens(A,T1,T2,R1,R2) adds happens(A,T1,T2) to the residue R1
  688   giving R2. Because happens(A,T1,T2) -> T1 <= T2, this necessitates
  689   updating the transitive closures of the before and beq facts in the residue.
  690   Duplicates aren't checked for, as it's assumed this is done by the
  691   calling predicate.
  692*/
  693
  694add_happens(A,T1,T2,[[HA,HC1],[BA,BC1]],[[[happens(A,T1,T2)|HA],HC2],[BA,BC2]]) :-
  695     \+ demo_before(T2,T1,[[HA,HC1],[BA,BC1]]),
  696     find_beq_connections(T1,T2,HC1,C1,C2), cross_prod_beq(C1,C2,C3,HC1),
  697     append(C3,HC1,HC2), find_bef_connections(T1,T2,BC1,C4,C5),
  698     cross_prod_bef(C4,C5,C6,BC1), delete_abdemo(before(T1,T2),C6,C7),
  699     append(C7,BC1,BC2).
  700
  701/*
  702   find_bef_connections(X,Y,TC,C1,C2) creates two lists, C1 and C2,
  703   containing respectively all the time points before X and after
  704   Y according to TC, which is assumed to be transitively closed.
  705*/
  706
  707find_bef_connections(X,Y,[],[X],[Y]).
  708
  709find_bef_connections(X,Y,[before(Z,X)|R],[Z|C1],C2) :-
  710     !, find_bef_connections(X,Y,R,C1,C2).
  711
  712find_bef_connections(X,Y,[before(Y,Z)|R],C1,[Z|C2]) :-
  713     !, find_bef_connections(X,Y,R,C1,C2).
  714
  715find_bef_connections(X,Y,[before(Z1,Z2)|R],C1,C2) :-
  716     find_bef_connections(X,Y,R,C1,C2).
  717
  718/*
  719   find_beq_connections is like find_bef_connections, except that it works
  720   on the transtive closure of happens part of the residue.
  721*/
  722
  723find_beq_connections(X,Y,[],[X],[Y]).
  724
  725find_beq_connections(X,Y,[beq(Z,X)|R],[Z|C1],C2) :-
  726     !, find_beq_connections(X,Y,R,C1,C2).
  727
  728find_beq_connections(X,Y,[beq(Y,Z)|R],C1,[Z|C2]) :-
  729     !, find_beq_connections(X,Y,R,C1,C2).
  730
  731find_beq_connections(X,Y,[beq(Z1,Z2)|R],C1,C2) :-
  732     find_beq_connections(X,Y,R,C1,C2).
  733
  734
  735cross_prod_bef([],C,[],R).
  736
  737cross_prod_bef([X|C1],C2,R3,R) :-
  738     cross_one_bef(X,C2,R1,R), cross_prod_bef(C1,C2,R2,R), append(R1,R2,R3).
  739
  740cross_one_bef(X,[],[],R).
  741
  742cross_one_bef(X,[Y|C],[before(X,Y)|R1],R) :-
  743     \+ member(before(X,Y),R), !, cross_one_bef(X,C,R1,R).
  744
  745cross_one_bef(X,[Y|C],R1,R) :- cross_one_bef(X,C,R1,R).
  746
  747
  748cross_prod_beq([],C,[],R).
  749
  750cross_prod_beq([X|C1],C2,R3,R) :-
  751     cross_one_beq(X,C2,R1,R), cross_prod_beq(C1,C2,R2,R), append(R1,R2,R3).
  752
  753cross_one_beq(X,[],[],R).
  754
  755cross_one_beq(X,[Y|C],[beq(X,Y)|R1],R) :-
  756     \+ member(beq(X,Y),R), !, cross_one_beq(X,C,R1,R).
  757
  758cross_one_beq(X,[Y|C],R1,R) :- cross_one_beq(X,C,R1,R).
  759
  760
  761
  762
  763/* REFINE */
  764
  765
  766/*
  767   refine(R1,N1,Gs,R2,N2) takes the earliest compound action out of the residue
  768   R1 and puts it in the goal list Gs, along with all "before", not(clipped) and
  769   not(declipped) facts that refer to the same time points. These time points
  770   are unskolemised, so that they can be bound to existing time points in the
  771   residue, thus permitting sub-actions to be shared between abstract actions.
  772   This almost restores the state of computation to the state S before the chosen
  773   action was added to the residue in the first place. But not quite, because
  774   some derived before facts will be retained in the transitive closure part
  775   of the before part of the residue that weren't there in state S. This doesn't
  776   matter, however, because these derived facts will need to be there eventually
  777   anyway, when those before facts that have been transferred from residue to goal
  778   list get put back in the residue.
  779
  780   The compound action extracted from the residue is marked for expansion by
  781   inserting it in the goal list in the form expand([happens(A,T1,T2)|Bs]),
  782   where Bs is the list of "before" facts taken out of the residue, as
  783   described above. When abdemo comes across a goal of this form, it will
  784   resolve the "happens" part against program clauses. The reason for
  785   not doing this resolution here is that we want to backtrack to alternative
  786   definitions of a compound goal inside the iterative deepening search, not
  787   outside it. This ensures the desired behaviour for compound actions which
  788   expand to one series of sub-actions given certain conditions but to another
  789   series of sub-actions given other conditions. Otherwise the check for these
  790   conditions, which will be a holds_at goal in the compound action definition,
  791   is in danger of being treated as a goal to be established instead of just
  792   checked.
  793*/
  794
  795refine([[HA1,HC1],[BA1,BC1]],N1,Gs,[[HA2,HC2],[BA2,BC2]],N3) :-
  796     split_happens(HA1,[BA1,BC1],happens(A,T1,T2),HA2),
  797     split_beqs(HC1,T1,T2,T3,T4,HC3,HC2),
  798     split_befores(BA1,T1,T2,T3,T4,BA3,BA2),
  799     split_befores(BC1,T1,T2,T3,T4,BC3,BC2),
  800     split_nafs(N1,T1,T2,T3,T4,N2,N3),
  801     append([expand([happens(A,T3,T4)|BA3])],N2,Gs).
  802
  803
  804/*
  805   split_happens(RH1,RB,H,RH2) holds if H is the earliest non-executable
  806   (abstract) action in RH1 according to RB. The remainder of RH1 ends up in
  807   RH2. If there are no non-executable actions, H is the earliest action.
  808*/
  809
  810split_happens([happens(A,T1,T2)],RB,happens(A,T1,T2),[]) :- !.
  811
  812split_happens([happens(A1,T1,T2)|RH1],RB,happens(A3,T5,T6),
  813          [happens(A4,T7,T8)|RH2]) :-
  814     split_happens(RH1,RB,happens(A2,T3,T4),RH2),
  815     order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
  816          happens(A3,T5,T6),happens(A4,T7,T8)).
  817
  818
  819order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
  820          happens(A1,T1,T2),happens(A2,T3,T4)) :-
  821     \+ executable(A1), executable(A2), !.
  822
  823order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
  824          happens(A2,T3,T4),happens(A1,T1,T2)) :-
  825     \+ executable(A2), executable(A1), !.
  826
  827order(happens(A1,T1,T2),happens(A2,T3,T4),RB,
  828          happens(A1,T1,T2),happens(A2,T3,T4)) :-
  829     demo_before(T1,T3,[[],RB]), !.
  830
  831order(happens(A1,T1,T2),happens(A2,T3,T4),RB,happens(A2,T3,T4),happens(A1,T1,T2)).
  832
  833
  834split_befores([],T1,T2,T3,T4,[],[]).
  835
  836split_befores([before(T1,T2)|Bs1],T3,T4,T5,T6,Bs2,[before(T1,T2)|Bs3]) :-
  837     no_match(T1,T2,T3,T4), !, split_befores(Bs1,T3,T4,T5,T6,Bs2,Bs3).
  838                                        
  839split_befores([before(T1,T2)|Bs1],T3,T4,T5,T6,[before(T7,T8)|Bs2],Bs3) :-
  840     substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
  841     split_befores(Bs1,T3,T4,T5,T6,Bs2,Bs3).
  842
  843
  844split_beqs([],T1,T2,T3,T4,[],[]).
  845
  846split_beqs([beq(T1,T2)|Bs1],T3,T4,T5,T6,Bs2,[beq(T1,T2)|Bs3]) :-
  847     no_match(T1,T2,T3,T4), !, split_beqs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
  848
  849split_beqs([beq(T1,T2)|Bs1],T3,T4,T5,T6,[beq(T7,T8)|Bs2],Bs3) :-
  850     substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
  851     split_beqs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
  852
  853
  854split_nafs([],T1,T2,T3,T4,[],[]).
  855
  856split_nafs([[clipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,Bs2,[[clipped(T1,F,T2)]|Bs3]) :-
  857     no_match(T1,T2,T3,T4), !, split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
  858
  859split_nafs([[clipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,
  860          [not(clipped(T7,F,T8))|Bs2],Bs3) :-
  861     !, substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
  862     split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
  863
  864split_nafs([[declipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,Bs2,
  865          [[declipped(T1,F,T2)]|Bs3]) :-
  866     no_match(T1,T2,T3,T4), !, split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
  867
  868split_nafs([[declipped(T1,F,T2)]|Bs1],T3,T4,T5,T6,
  869          [not(declipped(T7,F,T8))|Bs2],Bs3) :-
  870     !, substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
  871     split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
  872
  873split_nafs([N|Bs1],T3,T4,T5,T6,Bs2,[N|Bs3]) :-
  874     substitute_time(T1,T3,T4,T5,T6,T7), substitute_time(T2,T3,T4,T5,T6,T8),
  875     split_nafs(Bs1,T3,T4,T5,T6,Bs2,Bs3).
  876
  877
  878substitute_time(T1,T1,T2,T3,T4,T3) :- !.
  879
  880substitute_time(T2,T1,T2,T3,T4,T4) :- !.
  881
  882substitute_time(T1,T2,T3,T4,T5,T1).
  883
  884
  885no_match(T1,T2,T3,T4) :- T1 \= T3, T2 \= T3, T1 \= T4, T2 \= T4.
  886
  887
  888
  889
  890/* OTHER BITS AND PIECES */
  891
  892
  893/*
  894   add_neg(N,Ns1,Ns2) adds goal N to the list of (lists of) negations Ns1,
  895   giving Ns2. Duplicates are ignored, but N must be fully bound.
  896*/
  897
  898add_neg(N,Ns,Ns) :- member(N,Ns), !.
  899
  900add_neg(N,Ns,[N|Ns]).
  901
  902
  903/* append_negs is just append, but ignoring duplicates. */
  904
  905append_negs([],[],[]).
  906
  907append_negs([N|Ns1],Ns2,Ns4) :- add_neg(N,Ns2,Ns3), append(Ns1,Ns3,Ns4).
  908
  909
  910delete_abdemo(X,[],[]).
  911
  912delete_abdemo(X,[X|L],L) :- !.
  913
  914delete_abdemo(X,[Y|L1],[Y|L2]) :- delete_abdemo(X,L1,L2).
  915
  916
  917/* Skolemisation */
  918
  919skolemise(T) :- var(T), gensym(t,T), !.
  920
  921skolemise(T).
  922
  923
  924opposite(neg(F),F) :- !.
  925
  926opposite(F,neg(F)).
  927
  928
  929trace(off)