SHOP3 Manual

Next: , Previous: , Up: (dir)   [Contents][Index]

SHOP3 Manual

img/shop3-logo-small
Robert P. Goldman1, Dana Nau2, and Contributors

1 SIFT, LLC

319 North First Avenue, Suite 400

Minneapolis, MN 55401, USA

2 Department of Computer Science

University of Maryland

College Park, MD 20742, USA

Table of Contents


1 Introduction

AI planning is the subfield of artificial intelligence (AI) that aims at automating processes of means-ends reasoning. In general, AI planning is the problem of finding a sequence of actions that, executed in a specified initial state, will reach a goal state. This is a problem with applications to diverse areas including manufacturing, autonomous space and deep sea exploration, medical treatment, and military operations, to name just a few. This is the manual for SHOP3, the third major version of the Simple Hierarchical Ordered Planner.

An AI planning system takes as input a domain – a description of available actions, relations, etc.; a problem – a description of the initial state of the system, and an objective, a task to be performed or goal to be achieved. From these, it generates a plan: a sequence of actions that, if performed with the expected results, will attain the objective. This is the key function performed by SHOP3, although, as will be seen in this manual, many additional functions are offered.

SHOP3 is a domain-independent planning system based on ordered task decomposition, a modified version of Hierarchical Task Network (HTN) planning that involves planning for tasks in the same order that they will later be executed. An HTN, or decomposition, planner “proceeds by decomposing nonprimitive tasks recursively into smaller and smaller subtasks, until primitive tasks are reached that can be performed directly using the planning operators” (see Ghallab et al., 2004). This manual does not give an introduction to HTN planning or AI planning in general, for that we recommend the textbook by Ghallab et al. and the research papers describing SHOP.

SHOP and SHOP 2 were originally developed at the Computer Science Department of the University of Maryland, College Park, by Prof. Dana Nau’s research group. This manual draws heavily on material from the manual for SHOP2, which was, in turn based, in part, on the JSHOP documentation written by Füsun Yaman, with additional material from Yue Cao’s December 2000 draft of the SHOP2 documentation and pseudocode from Nau et al. (see Nau et al., 2001). Some updates to the SHOP2 manual were made by Robert P. Goldman and John Maraist, of SIFT.

SHOP3 contains two important subsystems that perform useful functions as part of it, but can also be used on their own. The first is the unifier, which computes the most general unifier of two logical formulas, encoded as Lisp s-expressions. The second subsystem is the theorem-prover, which performs Prolog-style rule-based Horn clause deduction over state sequences.

Robert P. Goldman and Ugur Kuter have a paper in the European Lisp Symposium describing SHOP3 (see Goldman & Kuter, 2019).

The planners in the SHOP family have the following distinctive characteristics:


Next: , Previous: , Up: SHOP3 Manual   [Contents][Index]

2 Execution Environment

SHOP3 is written in Common Lisp. To be able to run SHOP3, you will need to have Common Lisp installed on your computer. We have run SHOP3 successfully under the following implementations of Common Lisp, and we would be interested in hearing your reports about other implementations:

We suspect that there may be some difficulties in running SHOP3 on Windows; most of these have to do with getting the ASDF system definitions to work on Windows, not with SHOP3 proper. Please contact us if you encounter difficulties. We welcome reports of experiences with other platforms and CL implementations, and will attempt to support users who wish to bring SHOP3 up on other combinations.

Note that SHOP3 is known not to work with Embeddable Common Lisp (ECL).

SHOP3 is distributed with a system definition written using the open-source ASDF system definition facility (for more information, see http://common-lisp.net/projects/asdf/). You should insure that all of the .asd files in the SHOP3 distribution can be found by ASDF, per the instructions given with ASDF, and then SHOP3 should load without any problems. See Section 5.1 for more details about how to load SHOP3. All of the CL implementations we know of ship with ASDF pre-installed. To enable it you may have to

(require :asdf)

3 Running SHOP3

The latest version of SHOP3 is loaded by using the ASDF system definition facility. The first of the following subsections explains how to use ASDF to load SHOP3.1 There are three ways to invoke the SHOP3 planning process: find-plans, and find-plans-stack, which find plans for a single planning problem, and do-problems, which finds plans for a planning problem set. See Executing the Planner for instructions in the use of these functions. The functions shop-trace and shop-untrace are the primary mechanisms for debugging SHOP3 domain descriptions and problem specifications, see Tracing for instructions. See Other Debugging Features describes some additional features that may be useful for debugging domain descriptions and problems for SHOP3. Finally, see Hook Routines for a description of some hook routines that can be used to customize the behavior of SHOP3.


3.1 Loading the Planner

The SHOP3 planner should be loaded into your Lisp environment using ASDF. Assuming that ASDF is properly installed, and the SHOP3.asd system definition file can be found by ASDF,, the following command should get the system loaded:

(asdf:load-system "shop3")

SHOP3 is defined in the SHOP3 package (and uses the SHOP3.theorem-prover package). The easiest way to use the system for experimentation will be to change to the predefined :SHOP-USER package and work in there:

(in-package :shop-user)

If you are working on a larger or more ambitious project, it will be more appropriate for you to work in a package of your own definition, which should, at least, :use the SHOP3 and COMMON-LISP packages.


3.2 Executing the Planner


3.2.1 find-plans

The find-plans function has one mandatory argument, the name of a planning problem, and a set of optional keyword arguments. It returns up to four values. find-plans will always return two values: (1) a list of plans and (2) the total amount of CPU time used during planning (in seconds). If the :plan-tree argument (see below) is non-NIL, then two additional values will be returned: (3) a list of plan tree data structures and (4) a list of final state data structures. From the plan state data structures, the user can extract full state trajectories for the plans.

Function: find-plans problem &key domain which verbose gc pp plan-tree optimize-cost collect-state time-limit explanation depth-cutoff state tasks state-type hand-steer leashed out-stream

find-plans looks for solutions to the planning problem named problem. The keyword arguments are as follows: :which tells what kind of search to do. Its possible values are: :first - depth-first search, returning the first plan found. :all - depth-first search for *all* plans. :shallowest - depth-first search for the shallowest plan in the search space (this usually is also the shortest plan). If there’s more than one such plan, return the first.

:all-shallowest - depth-first search for all shallowest plans.
:id-first - iterative deepening search, returning the first plan.
:id-all - iterative deepening search for all shallowest plans.
:random - Randomized search. Used by Monroe. Not for normal

SHOP3 domains, since normal SHOP3 domains have order- dependent semantics.

:mcts - Monte Carlo Tree Search mode (experimental and unstable).

:verbose says how much information to print about the plans SHOP3

finds. Its values can be any of the following: 0 or nil - print nothing 1 or :stats - print some statistics on SHOP3’s operation 2 or :plans - print the stats and print all plans found, but omit operator costs and omit all operators whose names start with "!!" 3 or :long-plans - print the stats and plans, including all operator costs and all operators (even those whose names start with "!!")

:gc says whether to do a garbage collection before calling seek-plans
:plan-tree indicates whether or not to return plan tree(s).
:collect-state indicates whether or not to return final state(s). For backward-

compatibility, states are also returned whenever :plan-tree is true. This should probably eventually change.

return values:

plans found --- a list of plans. Each plan is a list that alternates a between instantiated operators and costs run time --- floating point value in seconds /if/ the plan-tree keyword argument is supplied, there will be two additional return values: plan-trees --- a list of plan trees, whose form is specified elsewhere. final-states --- a list of final state structures, one per plan.


3.2.2 find-plans-stack

Function: find-plans-stack problem &key domain verbose plan-tree gc no-dependencies repairable rationale state-type out-stream which analogical-replay unpack-returns make-analogy-table

Top level search function for explicit-state search in SHOP3. Does not support the full range of options supported by SHOP3’s ‘find-plans-stack‘.

Keyword arguments:

  • domain : either a domain name (symbol) or a ‘shop:domain‘ object.
  • verbose : 0, 1, 2, 3; default 0
  • plan-tree : build and return a plan tree? (‘plan-tree:top-node‘), defaults to ‘nil‘.
  • gc : If possible, perform a full gc before starting to plan. Default: current value of ‘shop:*gc*‘.
  • no-dependencies : if building a plan tree, build it *without* causal dependencies. Default: ‘nil‘.
  • repairable : return plans that can be repaired. Default: ‘nil‘.
  • rationale : build a plan tree with rationale information. Default: ‘nil‘.
  • state-type : what state type should be used for representing world states? (Note: world-state/SHOP state, *not* search-state). Default: ‘:mixed‘.
  • out-stream : where should output be printed. Default: ‘t‘ (standard output).
  • which : What/how many plans should be returned? Supports only ‘:first‘ (the default) and ‘:all‘.
  • analogical-replay : Do search informed by the contents of the ‘*analogical-replay-table*‘. Default: ‘nil‘.
  • make-analogy-table : Populate ‘*analogical-replay-table*‘ while planning. Only works with ‘:which‘ = ‘:first‘. Default: ‘nil‘.
  • unpack-returns : If true, return values in a way compatible with ‘find-plans‘. If false, return a list of ‘plan-return‘ objects instead. See discussion of return values, below. Default: ‘t‘.

Return values: There are two possible return types, selected by the keyword argument ‘unpack-returns‘:

1. Default/compatible with ‘find-plans‘:

  • List of plans
  • List of plan trees (if computed)
  • List of plan tree lookup tables
  • List of final world states
  • List of analogical replay tables (if computed)

To comply with SHOP3, though, always returns a list of plans. If the plan-tree keyword argument is non-NIL, will return an enhanced plan tree, with causal links, unless no-dependencies is non-NIL. Returns the values returned by seek-plans-stack, qv.


3.2.3 do-problems

The do-problems function has one mandatory argument, which can either be the name of a planning problem set or a list of names of planning problems. It executes find-plans on each of the given planning problems and returns nil.

Function: do-problems problems &rest keywords

do-problems runs find-plans on each problem in problems, which may be either a problem-set name (a symbol) or a list of problems.

Returns nothing of interest: should only be run for what it displays on the console.


3.2.4 Common Keyword Arguments

The keyword arguments to find-plans and do-problems are as follows:

  • which says what kind of search to do. Here are its possible values and what they mean. The default value of which is the value of the global variable *which* (whose default value is :first).
    ValueKind of search
    :first Depth first search, stopping at the first plan found
    :allDepth-first search, but don’t stop until all plans in plans(S, T, M) have been found
    :shallowestDepth-first search for the shallowest plan, or the first such plan if there is more than one of them. In many domains this is also the least-cost plan
    :all-shallowestDepth-first search for all shallowest plans in the search space
    :id-first Iterative-deepening search, stopping after the first plan found
    :id-allIterative-deepening search for all shallowest plans

    The iterative deepening options, :id-all and :id-first, are equivalent to taking a modified version of find-plans that backtracks each time it reaches depth d, and calling it repeatedly with d = 1, 2, …, until a plan is found.

  • verbose says what information to print out, as shown in the following table. The default value for verbose is 1.
    Value What to print
    0 or nilNothing
    1 or :statsSome statistics about the search
    2 or :plansThe statistics plus a succinct version of each plan found: internal operators (see internal operators), and operator costs are omitted.
    3 or :long-plansThe statistics plus the complete version of each plan found
  • If gc is non-nil, then find-plans calls the garbage collector just before starting its search, thus making it somewhat easier to get repeatable experimental results. The default value of gc is T.
  • If pp is non-nil, then all printing done by SHOP3 is performed using the Common Lisp pretty-printing mechanism. This typically leads to more easily read output. The default value of pp is T.
  • The state argument controls how states are represented internally. SHOP3 can have different performance characteristics depending on the value provided to this augment. If you are encountering out-of-memory errors in SHOP3 or you want to get the maximum speed possible from SHOP3 for a particular set of problems, you may wish to experiment with different values for this argument. The default value is :mixed, which represents states using a combination of lists and hash tables; this value has been shown to provide a reasonably good combination of speed and memory usage on a variety of test problems. The other values are :list, :hash, and :bit.
  • The optimize-cost argument is used to perform planning with branch-and-bound optimization of the total plan cost. The default value for this argument is nil. If the value of this argument is nil, the optimization feature is disabled. If the value of the argument is t, SHOP3 will search for plans with the minimum total cost. If the value of the argument is a number, SHOP3 will use the branch-and-bound technique to search for plans with cost less than or equal to the value of the argument. The optimization feature is written under the assumption that the costs of operators are always non-negative. If this assumption is invalid, SHOP3 will produce unreliable results (specifically it will prune out some valid plans). The interaction of :optimize-cost with the various options for :which can be subtle. Below are notes on each possible combination:
  • (:which :first :optimize-cost t)

    Under these arguments, SHOP3 returns the first plan found for which no other valid plan has a lower total cost. Note that this option may take much more time to run than using (:which :first :optimize-cost nil) since even after it finds the plan, it must keep searching to see if it can find a cheaper plan. However, this option may be significantly faster than (:which :all :optimize-cost nil) since the branch-and-bound mechanism will prune out non-optimal plans without having to consider them all the way to the end. In some cases, this will mean that (:which :first :optimize-cost t) terminates and (:which :all :optimize-cost nil) does not.

  • (:which :first :optimize-cost number)

    Under these arguments, SHOP3 returns the first plan found whose total cost is less than or equal to the number given. If there is no plan whose total cost is less than or equal to that number, SHOP3 will return no plans. Note that if the number given is large enough, these arguments can produce results much more quickly than with (:which :first :optimize-cost t); specifically, as soon as SHOP3 finds a plan for which the cost is met, it can terminate and does not have to keep searching for cheaper plans.

  • (:which :all :optimize-cost t)

    Under these arguments, SHOP3 returns all plans for which no other valid plan has a lower total cost. Obviously, all plans returned under these options will have equal total cost.

  • (:which :all :optimize-cost number)

    Under these arguments, SHOP3 returns all plans with total cost less than or equal to the given number.

  • (:which :shallowest :optimize-cost t)

    Under these arguments, SHOP3 returns a plan that has the shallowest depth of all valid plans and for which there is no other shallowest depth valid plan which has a lower total cost. In other words, these arguments produce the cheapest of all shallowest plans (which, incidentally, is not necessarily the same thing as the shallowest of all cheapest plans).

  • (:which :shallowest :optimize-cost number)

    Under these arguments, SHOP3 returns a plan which has the shallowest depth of all valid plans and whose total cost is less than or equal to the given number. Note that if there is no plan whose cost is less than or equal to the number and whose depth is shallowest among all valid plans, then no plan will be returned (even if there are deeper plans which do have cost less than or equal to the number).

  • (:which :all-shallowest :optimize-cost t)

    Under these arguments, SHOP3 returns all plans which have the shallowest depth of all valid plans and for which there is no other shallowest depth valid plan which has a lower total cost.

  • (:which :all-shallowest :optimize-cost number)

    Under these arguments, SHOP3 returns all plans which have the shallowest depth and whose total cost is less than or equal to the given number.

  • (:which :id-first) or (:which :id-all)

    The :id-first and :id-all options produce the same results as the shallowest and all-shallowest arguments, respectively for each different combination with :optimize-cost. Note, however, that there are domains for which SHOP3 will terminate using id-first and id-all and will not terminate using other values for :which.

  • The time-limit argument may either nil or a number. Its default is nil and if it is nil, no time limit is imposed on the planning process. If the time-limit argument is a number, SHOP3 will check the elapsed CPU time at the start of each step of the planning process, and if the number of seconds elapsed is greater than the argument value, SHOP3 will immediately terminate. The main use for this feature is in combination with (:optimize-cost t) argument, in order to return the optimal value found within the given time limit. For example, consider the call (find-plans 'foo :verbose 1 :optimize-cost t :time-limit 120). This call addresses a problem named foo, and runs until it either finds the minimum cost plan or until 2 minutes have elapsed. It then returns the lowest cost plan that it found during that time. This functionality is inspired, in part, by Anytime Algorithms (see Dean & Boddy, 1998).
  • If explanation is non-nil, SHOP3 adds extra information at the end of each operator explaining how the preconditions for that operator were satisfied. Currently supports only logical atoms, and, and or; it doesn’t work with forall, not, eval, etc. If this feature is used with the external-access-hook feature (see Hook Routines), any attribution information provided by the external-access-hook routine is included in the relevant explanation. The default value of explanation is nil.
  • The plan-tree argument defaults to nil; if true, the planner will return two additional values: (1) a list of complete task decomposition trees for the plans and (2) a list of plan state data structures corresponding to the final states of each plan. Plan trees are encoded in a nested list format in which the decomposition of an upper level task into lower level tasks is represented by the upper level task atom, followed by trees for each lower level task. The leaves of the tree, involving operators, are each lists of three elements: the cost of the operator, the task atom for the operator, and the numerical position of the operator in the plan (starting at 1). For example, a task (travel houston springfield) that was directly decomposed into operators, (!fly houston boston) with cost 200 and (!drive boston springfield) with cost 50, would have the following plan tree:
    ((travel houston springfield)
     (200 (!fly houston boston) 1)
     (50 (!drive boston springfield) 2))
    

3.3 Tracing

There are two functions used for controlling the tracing mechanism in SHOP3: shop-trace and shop-untrace. These are similar to Lisp’s trace and untrace functions. Once they have been invoked, subsequent calls to find-plans or do-problems will print out information about elements of the domain for which tracing is enabled whenever those elements are encountered. More specifically:

  • (shop-trace item) will turn on tracing for item, which may be any of the following:
    • a method, axiom, operator, task, or goal;
    • one of the keywords :methods, :axioms, :operators, :tasks, :goals, or :protections in which case SHOP3 will trace all items of that type (:goals refers to predicates that are goals for the theorem-prover, and :protections refers to predicates used as arguments of :protection in operators);
    • the keyword :states, in which case SHOP3 will include the current state whenever it prints out a tracing message
    • the keyword :plans in which case SHOP3 will print diagnostic information whenever it has found a plan (and may be considering whether or not to keep the plan, depending on the :which and :optimize arguments of seek-plans).
    • The keyword :all, which will trace all available items, currently methods, axioms, operators, tasks, goals and protections.
  • (shop-trace item1 item2 …) will do the same for a list of items
  • (shop-trace) will print a list of what’s currently being traced
  • (shop-untrace item) will turn off tracing for an item
  • (shop-untrace item1 item2 …) will turn off tracing for a list of items
  • (shop-untrace) will turn off tracing for all items
Macro: shop-trace &rest items

- (shop-trace) with no arguments will return a list of what’s currently being traced.

- (shop-trace item) will turn on tracing for item.

item may be any of the following:

  • the name of a method, axiom, operator, task, or predicate;
  • one of the keywords :methods, :axioms, :operators, :tasks, :goals, :effects, or :protections, in which case shop will trace all items of that type (:GOALS, :effects, and :protections refer to three different ways predicates can occur: as goals to be satisfied, and as effects or protections in operators);
  • a pair of the form (:task <taskname>), (:method <methodname>). shop will break when attempting to expand the task, or apply the method, respectively.
  • the keyword :states, in which case shop will include the current state whenever it prints out a tracing message
  • the keyword :all in which case shop will print out all the tracing information it knows how to.

- (shop-trace item1 item2 ...) will do the same for a list of items


Next: , Previous: , Up: Running SHOP3   [Contents][Index]

3.4 Other Debugging Features

There are three variables, namely *current-state*, *current-plan*, and *current-tasks*, in SHOP3. These variables can be used to monitor the current status of the state, current plan and the list of current tasks to be accomplished respectively. Since these are the internal variables of the SHOP3 planning system, the following functions are defined to access the current contents of those variables: print-current-state, print-current-plan, and print-current-tasks, respectively. Note that these are Lisp functions that must be called by using the Lisp evaluator. The best way to use these functions is to define dedicated methods in the domain that invoke the functions using eval or call expressions in their predicates. Those methods can then be used in the problem definition where debugging output is needed. For example, the following methods can be included in any domain description for this purpose:

(:method (print-current-state)
    ((eval (print-current-state)))
    ())

(:method (print-current-tasks)
   ((eval (print-current-tasks)))
   ())

(:method (print-current-plan)
    ((eval (print-current-plan)))
    ())

And these special purpose methods can be used in the task decompositions of other methods for debugging purposes. For example,

(:method
    (do-both ?x ?y)
    nil
    (:ordered
      (:task !do ?y)
      (:task print-current-state)
      (:task !do ?x))))

There is now a new variable, *break-on-backtrack*, that will cause the Lisp environment to throw into a break loop when SHOP3 backtracks.


3.5 Syntax Checks

We have adopted for SHOP3 the “singleton variable” check common in Prolog implementations. Logic variables are used to express unification constraints on expressions. In practice, a singleton logical variable in a SHOP3 expression (a method, operator, or axiom definition) is often a typographical error. Accordingly, SHOP3 will issue a warning when it encounters a logical variable used only once. If the single use is correct, the proper (and nicely self-documenting) way to disable this warning is to use an anonymous variable (see see Symbols).


3.6 Debugging Suggestions

When you have a problem that does not solve as expected, the following general recipe may help you home in on bugs in your domain definition:

  1. Start by doing (shop-trace :tasks) and then try find-plans again.
  2. In many cases, the domain will be written so that there will be little or no backtracking. In this case, examine the output of the traced call to find-plans and look for the first backtracking point.
  3. The above process should help you identify a particular task, either a primitive or a complex task, as a likely problem spot. If it’s a primitive task, the next step is to examine the operator definition. If it’s a complex task, you should check the method definitions. If you have any trouble identifying which method definition is relevant, you can use (shop-trace :methods) to further focus your attention.
  4. If visual inspection of method and operator definitions does not reveal the problem, you most likely have problems with precondition expressions. In this case, try using (shop-trace :goals), re-running find-plans and check to see what’s happened when your problematic method or operator’s preconditions are checked.

This recipe has proven effective for finding the vast majority of bugs in SHOP3 domains.


3.7 Hook Routines

SHOP3 recognizes several different hook routines. These are Lisp routines that may be defined by the user; if they are defined, they are invoked under specific circumstances. Hook routines are typically used when embedding SHOP3 in an application; they allow such an application to obtain additional information from SHOP3 or to affect its behavior. There are three hooks that are recognized by SHOP3:

  • (plan-found-hook state which plan cost depth) If this routine is defined, SHOP3 invokes it whenever it finds a plan. It can be useful for displaying and/or recording details about the plan. The arguments are the current state, the value for the :which argument that was provided to the planner, the plan, the cost of the plan, and the search depth at which the plan was found.
  • (trace-query-hook type item additional-information state-atoms) If this routine is defined, SHOP3 invokes it whenever it invokes the tracing mechanism (see Tracing). The arguments include the type of item being traced (e.g., :task, :method), the item, the list of Lisp values that are printed by the tracing mechanism, and a list of logical atoms in the current state.
  • (external-access-hook query) This hook routine is intended to allow SHOP3 to use an external source (such as a database) to determine the applicability of methods and operators. To use this hook routine, a domain must include one or more logical expressions that have the keyword :external as the first symbol. Such expressions must only involve a single logical atom, or a single conjunction of logical atoms. When SHOP3 attempts to find a binding that satisfies such an expression, it will first invoke external-access-hook to satisfy the expression; if that routine is undefined or returns nil, SHOP3 will then try to satisfy the expression using its internal knowledge state. The argument to external-access-hook is a list of the form '(and (pred v1 v2)…). It returns a list of responses, each of which is a list of two elements: an attribution, and a list of bindings for the unbound variables in the query. The attribution is stored for use with the explanation option for the planning system (see explanation). For example, consider a method that has the following precondition:
    (or (and (clear ?b1) (clear ?b2) (clear ?b3))
             (:external and (on ?b1 ?b2) (on ?b2 ?b3)))
    

    When this precondition is encountered and external-access-hook is defined, SHOP3 invokes that routine with the argument '(and (on ?b1 ?b2) (on ?b2 ?b3)). The routine might (for example) return the list:

    '((database-123 ((?b1 block10) (?b2 block 11) (?b3 block 12)))
      (database-223 ((?b1 block20) (?b2 block 21) (?b3 block 22))))
    

Next: , Previous: , Up: SHOP3 Manual   [Contents][Index]

4 The SHOP3 Formalism

The inputs to SHOP3 are a planning domain and either a single planning problem or a planning problem set. Planning domains are composed of operators, methods, and axioms. Planning problems are composed of logical atoms (an initial state) and tasks lists (high-level actions to perform). Planning problem sets are composed of planning problems.

The components of a planning domain (operators, methods, and axioms) all involve logical expressions. These logical expressions combine logical atoms through a variety of forms (e.g., conjunction, disjunction). Logical atoms involve a predicate symbol plus a list of terms. Task lists in planning problems are composed of task atoms. The components of domains and problems are all ultimately defined by various symbols.

This section describes each of the aforementioned structures. It is organized in a bottom-up manner because the specification of higher-level structures is dependent on the specification of lower-level structures. For example, methods are defined after logical expressions because methods contain logical expressions.


4.1 Symbols

In the structures defined below, there are five kinds of symbols: variable symbols, constant symbols, function symbols, primitive task symbols, and compound task symbols. To distinguish among these symbols, SHOP and SHOP3 both use the following conventions:

  • a variable symbol can be any Lisp symbol whose name begins with a question mark (such as ?x or ?hello-there)
  • an anonymous variable symbol can be any variable symbol with an underscore immediately following the question mark in its name (such as ?_ or ?_airplane). These variables will unify with any value, and need not co-refer (i.e., two copies of ?_ in a single term need not unify with each other). These variables will also not trip the singleton variable check.
  • a primitive task symbol can be any Lisp symbol whose name begins with an exclamation point (such as !unstack or !putdown)
  • a constant symbol, a function symbol, a predicate symbol, or a compound task symbol can be any Lisp symbol whose name does not begin with a question mark or exclamation point. We use “predicate” and “function” in the first-order logic sense; as will be seen in Eval Terms, the functions can be general Lisp functions.

Any of the structures defined in the remaining sections are said to be ground if they contain no variable symbols.


Next: , Previous: , Up: The SHOP3 Formalism   [Contents][Index]

4.2 General Lisp Expressions

A number of SHOP3 domain structures described in this section, (e.g. Assignments, Sorted Precondition, Eval Terms, and Call terms) use general Lisp expressions. These are arbitrary pieces of Lisp code which can include function calls, macro invocations, special macro symbols (e.g., backquote), etc. When SHOP3 needs to get the value of a general Lisp expression, it first substitutes values for any variable symbols in the expression that are bound. Then it submits the entire expression to the Lisp environment to get its value.

Note: Counter-intuitive bugs may arise when symbols are passed to Lisp for evaluation (either as constants or as the values of variables). Remember that the Lisp evaluator will assume that these are variables! If you wish them to be treated as symbols, you will need to quote them. This leads to a slightly undesirable oddity — variables that will be bound to, for example, numbers, can appear normally. Variables that will be bound to symbols will have to be quoted. See eval terms.


4.3 Terms

A term is any one of the following:

  • a variable symbol
  • a constant symbol
  • a number
  • a list term
  • an eval term
  • a call term

The last two are function terms in first-order logic parlance.


Next: , Previous: , Up: Terms   [Contents][Index]

4.3.1 List Terms

A list term is a term having the form

([list] t1 t2tn [. l])

where list is an optional reserved word and each ti is a term. This specifies that t1 t2tn are the items of a list. If the final, optional element is included, the item l should evaluate to a list; all items in l are included in the list after t1 through tn.


Next: , Previous: , Up: Terms   [Contents][Index]

4.3.2 Eval Terms

An eval term is an expression of the form

(eval general-lisp-expression)

The value associated with an eval term is determined as follows. First, any variable symbols which appear in general-lisp-expression and are bound are replaced by the values that they are bound to. Then, the entire expression is evaluated in Lisp. For example, if the variable symbol ?foo is bound to the value 3 then the term:

(eval (mapcar #'(lambda (x) (+ x ?foo)) `(1 2 ,(* ?foo ?foo))))

will have as its value a list containing the numbers 4, 5, and 12.

Note that variable substitutions in eval terms are handled before any evaluation of the expression, as in Lisp macros. One implication of this fact is that variables with symbolic values must be explicitly quoted if they are to be treated as Lisp symbols. For example, if the variable ?foo is bound to the symbol bar, the following eval term has the value (bar baz):

(eval (list '?foo 'baz))

But if this were written

(eval (list ?foo 'baz))

it would cause a Lisp error when Lisp attempts to find the value of bar, which it would believe to be a variable.


Previous: , Up: Terms   [Contents][Index]

4.3.3 Call terms

A call term is not as expressive as an eval term. In particular, it does not support the evaluation of Lisp macros (including macro characters such as backquote). Both call and eval are supported in SHOP3 because the former is compatible with JSHOP 1.0 and the latter is compatible with SHOP 1.x. SHOP3 users who are not interested in either form of compatibility may use either form.

A call term is an expression of the form

(call f t1 t2tn)

where f is a function symbol and each ti is a term or a call term. A call term has a special meaning to SHOP3, because it tells SHOP3 that f is an attached procedure, i.e., that whenever SHOP3 needs to evaluate a precondition or task list that contains a call term, SHOP3 should replace the call term with the result of applying the function f to the arguments t1, t2, …, tn. We later will define preconditions (see preconditions) and task lists (see Task Lists).

For example, the following call term would have the value 6:

(call + (call + 1 2) 3)

4.4 Logical Atoms

A logical atom has the form:

(p t1 t2tn)

where p is a predicate symbol, each ti is a term other than an eval or call term, and n can be 0.


4.5 Logical Expressions

A logical expression is a logical atom or any of the following complex expressions: conjuncts, disjuncts, negations, implications, universal quantifications, assignments, eval, call, enforce, setof, and bagof. Terms enter into logical expressions via atoms.


4.5.1 Conjuncts

A conjunct has the form

([and]l1 l2ln)

where each li is a logical expression.

Note that if there are 0 conjuncts (e.g., the expression is ()) then the form always evaluates to true.

Also note that implicit conjunction (list of logical expressions without an explicit and) is deprecated, and will eventually be removed, as it significantly complicates SHOP3’s parsing – and reading SHOP3 code by humans.


Next: , Previous: , Up: Logical Expressions   [Contents][Index]

4.5.2 Disjuncts

A disjunct is an expression of the form

(or l1 l2ln)

where l1, l2ln are logical expressions.


4.5.3 Negations

A negation is an expression of the form

(not l)

where l is a logical expression.


4.5.4 Implications

An implication is an expression of the form

(imply Y Z)

where Y and Z are logical expressions. The intent of an implication is to evaluate its logical counterpart; that is, \neg Y \lor Z. Note that the context should not leave free variables in Y, or the semantics of the implication will be ambiguous.


4.5.5 Universal Quantifications

A universal quantification expression is an expression of the form

(forall V E1 E2)

where E1 and E2 are logical expressions, and V is the list of variables in E1. To satisfy a universally quantified expression, the following must hold: for each possible substitution u for variables in V, if E1u is satisfied then E2u must also be satisfied in the current state of the world. Note that this use of the keyword forall is distinct from its use in add and delete lists in operators (see Operators): the latter is used to express a set of effects rather than a logical expression and consequently has a different syntax.

There is no need for existential quantifications. See [Ghallab et al., 2004] or Internal Knowledge Structures.


4.5.6 Assignments

A simple assignment expression has the form

(assign v e)

where v is a variable symbol and e is general Lisp expression. The intent of an assignment expression is to bind the value of e to the variable symbol v. Variable substitutions in assignment expressions are done using literal substitutions, as with eval terms (see Eval Terms). For example, if ?foo is bound to the symbol if and ?bar is bound to the number 0 then the following expression will bind the variable ?baz to the list (if fish):

(assign ?baz (?foo (< ?bar 3) (list '?foo 'fish) (/ 8 ?bar)))

Similarly, if ?foo is bound to list and ?bar is bound to 4 then the expression above will bind ?baz to the list (nil (list fish) 2).2

Note: assign is not the default way to bind SHOP3’s logical variables. The default way to bind logical variables is through unification. assign is specifically for use when you wish to use Lisp code to produce values you will bind variables to. To that end, assign expects that its second argument will be a Lisp expression and it will evaluate that expression. It is because of this evaluation process that the following expression (with = interpreted as unification)

(= ?x foo)

will bind ?x to the symbol foo, but

(assign ?x foo)

will cause a run-time error. In the second example, SHOP3 will attempt to evaluate foo and report it as an unbound variable – unless this is evaluated in a context where foo is a variable, in which case ?x will be bound to the current value of foo.

SHOP3 also offers a compound assignment expression of this form:

(assign* v e)

As in the simple assign, v is a variable symbol and e is general Lisp expression. However, for assign*, e should evaluate to a list of possible values and through backtracking, SHOP3’s theorem-prover will find all solutions with v bound to the various values of e in turn.


4.5.7 Eval expressions

An eval expression has the same form as an eval term (see Eval Terms). Unlike an eval term, however, an eval expression is interpreted simply as either true or false rather than having some value which would be used as an argument to a predicate. Thus an eval expression typically invokes boolean Lisp functions such as evenp or >=.

Note that if you use an eval expression for its side effects, you must be careful to ensure that it still returns a true value. For example, if you introduce an invocation of format for debugging purposes, remember that format always returns nil, and will cause the containing precondition to fail!


4.5.8 Call expressions

A call expression has the same form as a call term (see Call terms). As with eval expressions (see Eval expressions), call expressions are interpreted as either true or false, and the warning mentioned there about using eval expressions for side effects applies to call expressions, as well.


4.5.9 Enforce expressions

An enforce expression has the form

(enforce t1 &rest error-args)

Enforce expressions are for goals that should always be satisfied. SHOP3’s theorem-prover will attempt to prove t1 and if it fails, will call error with error-args. For example

(enforce (x-position ?aircraft)
          "~A x-position undefined." (quote ?aircraft))

Enforce expressions are useful when debugging domains.


4.5.10 Setof expressions

A setof expression has the form

(setof term expr set-var)

Find all solutions to expr, and bind the set of values for term in expr to set-var. For example

(setof ?u (uav ?u) ?uavs)

will bind ?uavs to the set of UAVs in the current state.

(setof (pair ?u1 ?u2)
  (and (uav ?u1) (uav ?u2) (line-of-sight ?u1 ?u2))
  ?pairs)

will bind ?pairs to a set of terms, e.g., ((pair rotor1 fw2) (pair rotor2 fw3)) indicating pairs of UAVs with line of sight from the first to the second.

Note: The semantics of setof are to fail if the expr is an unsatisfiable goal, rather than to succeed with set-var bound to ().

Note: Support for general terms as the first argument to setof and bagof (see Bagof expressions) is new in version 3.4 of SHOP3. Code that depends on it should use a corresponding version dependency qualifier in, e.g., ASDF ((:version "shop3" "3.4")).


4.5.11 Bagof expressions

The syntax for bagof is the same as for setof (see Setof expressions), but binds set-var to a bag of results, which may contain duplicates, instead of a set.


4.6 Logical Precondition

A logical precondition is either a logical expression or one of the following special precondition forms: first satisfier precondition, sorted precondition.


4.6.1 First Satisfiers Precondition

A first satisfier precondition has the form

(:first l1 l2 … ln)

where each li is a logical expression. Such a precondition causes SHOP3 to consider only the first set of bindings that satisfies all of the given expressions. Alternative bindings will not be considered even if the first bindings found do not lead to a valid plan.


4.6.2 Sorted Precondition

A sorted precondition has the form

(:sort-by v [e] l)

where v is a variable symbol, e.g., ?x; e is a general Lisp expression that should evaluate to a comparison function; and l is a logical expression. Such a precondition causes SHOP3 to consider bindings for v in a specific order: bindings are sorted such that if the comparison function holds between values x and y then bindings of v to x may not occur after bindings of v to y. For example consider the precondition:

(:sort-by ?d #'> (and (at ?here) (distance ?here ?there ?d)))

This precondition will cause SHOP3 to consider bindings in decreasing (high to low) order of the value of ?d. If the comparison function (e) is omitted, it defaults to #'<, indicating increasing (low to high) order.


4.7 Axioms

An axiom is an expression of the form

(:- a
    [name1] E1
    [name2] E2
    [name3] E3 …
    [namen] En)

where the axiom’s head is a logical atom a, and its tail is the list ([name1] E1 [name2] E2 [name3] E3 … [namen] En). Each Ei is a logical expression and namei is a symbol called the name of Ei. These names are optional; when a domain definition is loaded into SHOP3, a unique name will be generated for each Ei if no name was given. The names have no semantic meaning to SHOP3, but are provided to help the user debug domain descriptions by looking at traces of SHOP3’s behavior.

The intended meaning of an axiom is that a is true if E1 \vee \cdots \vee En, and the evaluation stops when, for i=1,2,\ldots, the first true Ei is encountered.

For example, the following axiom says that a location is in walking distance if the weather is good and the location is within two miles of home, or if the weather is not good and the location is within one mile of home:

(:- (walking-distance ?x)
     good (and (weather-is good) (distance home ?x ?d) (call <= ?d 2))
     bad  (and (distance home ?x ?d) (call <= ?d 1)))

There is more to be said on axioms: see More on axioms.


Next: , Previous: , Up: The SHOP3 Formalism   [Contents][Index]

4.8 Task Atoms

A task atom is an expression of any of the forms

(s t1 t2tn)
(:task s t1 t2tn)
(:task :immediate s t1 t2tn)

where s is a task symbol and the arguments t1, t2, …, tn are terms. The task atom is primitive if s is a primitive task symbol, and it is compound if s is a compound task symbol; recall Symbols, and also see Operators. The first and second forms are called an ordinary task atom; the third form is called an immediate task atom. The purpose of the :immediate keyword is to give a higher priority to the task, as described in the following subsection.


Next: , Previous: , Up: The SHOP3 Formalism   [Contents][Index]

4.9 Task Lists

A task list is any of the following:

  • an expression of the form (:unordered tasklist1 tasklist2 … tasklistn), where tasklist1 tasklist2 … tasklistn are task lists;
  • an expression of the form ([:ordered] tasklist1 tasklist2 … tasklistn), where tasklist1 tasklist2 … tasklistn are task lists.
  • A task atom, see Task Atoms.

The :ordered keyword, which is optional, specifies that SHOP3 must perform the task lists in the order that they are given. The :unordered keyword specifies that there is no particular ordering specified between tasklist1, tasklist2 … tasklistn With the use of the :unordered keyword, SHOP3 may interleave tasks between different task lists. The :ordered and :unordered keywords may be used to specify a simple task network (see GhallabEtAl2004).

Now suppose that we have the following two task lists T = (:ordered t1 t2tm),

U = (:ordered u1 u2un),

and the main task list

M = (:unordered T U ).

If none of the tasks have the :immediate keyword, then the tasks in T should be performed in the order given, and the tasks in U should also be performed in the order given—but it is permissible for SHOP3 to interleave the tasks of T and the tasks of U. However, if some of the tasks are immediate, then each time SHOP3 chooses the next task to accomplish, it needs to give a higher priority to the immediate tasks. For example, if t1 is immediate and u1 is not immediate, then SHOP3 should perform t1 before both t2 and u1.

Note: A task with the :immediate keyword specifies that this task must be performed immediately when it has no predecessors.  Therefore, we can allow only one task with the :immediate keyword in the list of tasks that have no predecessors.  Otherwise SHOP3’s behavior on those tasks is undefined.  In other words, it is not allowed to have two tasks in an :unordered list with both having the :immediate keyword.  For instance, in the example above t1 and u1 cannot both have the :immediate keyword.


Next: , Previous: , Up: The SHOP3 Formalism   [Contents][Index]

4.10 Operators

An operator is description of how to perform a primitive task, which cannot be decomposed further. An operator definition has the following form:

(:op head
       [:precond precondition]
       [:delete delete-list]
       [:add add-list]
       [:cost cost-fn])

where

  • head (the operator’s head) is a primitive task atom, i.e. a task atom with a task symbol that begins with an exclamation point.
  • The operator’s precondition is a logical expression. This is quite general: recall Logical Expressions, especially Assignments, and Eval expressions. With the latter two one can, for example, compute values for auxiliary variables, which can be used later in the body of the operator.
  • The operator’s add-list is a list for which each element may be any of following:
    • a logical atom (recall Logical Atoms),
    • a protection condition, see Protection conditions,
    • an expression of the form (forall V E L), where V is a list of variables in E, E is a logical expression, and L is a list of logical atoms.

      Such an expression can, for example, be used to implement PDDL’s conditional effects.

  • The operator’s delete-list is a list of logical atoms of the same form as the add-list.
  • cost-fn (the operator’s cost) is a general Lisp expression. If cost-fn is omitted, the cost defaults to 1.

Note that the components of an :op expression do not need to be presented in any special order – :add, :delete, etc. are processed as keyword (named) arguments.


4.10.1 Internal Operators

As noted above, the head of the operator is a primitive task atom, so it must begin with a primitive task symbol, i.e., a symbol that begins with an exclamation point. Note that operator names which begin with two exclamation points have a special meaning in SHOP3; operators of this sort are known as internal operators. Internal operators are ones which are used for purposes internal to the planning process and are not intended to correspond to actions performed in the plan (e.g., to do some computation which will later be useful in deciding what actions to perform). Other than requiring two exclamation points at the start of the name, the syntax for internal operators is identical to the syntax for other operators. SHOP3 handles internal operators exactly the same way as ordinary operators during planning. SHOP3 includes these operators in any plans that it returns at the end of execution. It may, however, omit them from the printout of the final plan (depending on the value of the :verbose argument (see verbose).

The primary reason that the internal operator syntax exists in SHOP3 is so that automated systems which use SHOP3 plans as an input can easily distinguish between those operators which involve action and those which were merely internal to the planning process.


4.10.2 Operators must be deterministic

When designing an operator, it is important to ensure that each variable symbol in the add list, delete list, and cost always be bound to a single value when the operator is invoked. Variable symbols can be bound in the head of the operator (by the method that invokes the associated primitive task) or in the precondition of the operator. An operator should be written such that for any variable appearing after the precondition (a) no two unifiers of the precondition have different bindings for that variable, and (b) unification results in some binding for it, i.e. it does not remain unbound. SHOP3 does not check this requirement; if conflicting unifiers are available when applying an operator, it will apply one arbitrarily. This can lead to unpredictable behavior and plans with ambiguous semantics. In general, we recommend that operator preconditions be designed such that only one unifier is possible. However, SHOP3 will be able to correctly process operators that have multiple unifiers for preconditions as long as no two unifiers can provide different values for a variable that appears in the add list, delete list, or cost.


4.10.3 Protection conditions

In the definition of operators, a protection condition is an expression of the form

(:protection a)

where a is a logical atom. The purpose of a protection condition in the add list is to tell SHOP3 that it should not execute any operator that deletes a. The purpose of a protection condition in the delete list is to cancel a previously added protection condition. For example, if we drive a delivery truck to a certain location in order to pick up a package, then we might not want to allow the truck to be moved away from that location until after we have picked up the package.  To represent this, we might use the following operators:

(:op (!drive-to ?truck ?old-loc ?location)
   :delete ((at ?truck ?old-loc))
   :add ((at ?truck ?location)
           (:protection (at ?truck ?location))))
(:op (!pick-up ?truck ?package ?location)
  :delete
    ((at ?package ?location)
     (:protection (at ?truck ?location)))
   :add ((in ?package ?truck)))

4.10.4 Operators: Legacy Syntax

In our work with SHOP2, we found that operator definitions in its original syntax were prone to hard-to-detect syntax errors and typos that can give rise to difficult to identify “garbage in/garbage out” bugs. Particularly prevalent are hard-to-identify bugs arising when a programmer inadvertently reverses the order of add and delete lists in a SHOP3 operator. These problems are exacerbated by the extreme permissiveness of SHOP3’s parser. This led us to the new syntax, described above, which relies on keywords to make operator definitions more readable, and less error-prone. Our new syntax also supports arbitrary order and the omission of empty components, without the “DWIM” parsing in SHOP2. Because of its many advantages, so we encourage you to adopt the new syntax, instead of continuing to use the “classical” form described here, although it is still supported.

The original operator definition syntax was as follows:

(:operator head precondition delete-list add-list [c])

The two operators described above are written in the old syntax as follows:

(:operator (!drive-to ?truck ?old-loc ?location)
   ()
   ((at ?truck ?old-loc))
   ((at ?truck ?location)
    (:protection (at ?truck ?location))))
(:operator (!pick-up ?truck ?package ?location)
  ()
  ((at ?package ?location)
   (:protection (at ?truck ?location)))
  ((in ?package ?truck)))

For backwards compatibility with SHOP 1.x, SHOP3 will also accept operators where the precondition P is missing. In this case the domain definition pre-processing code puts a null precondition into the operator, which is always satisfied. SHOP3’s ability to recognize operators without preconditions is deprecated and is likely to disappear in the future.


4.11 Methods

A method is a list of the form

(:method [nm] T [n1] C1 T1 [n2] C2 T2 … [nk] Ck Tk)

where

  • nm is an optional name for this method. Note that nm is distinct from the (also optional) names ni for each (precondition, task network) pair described below. The exception to this rule is that if an n1 is supplied for a method expression with only one (precondition, task network) pair, n1 will be used as the identifier for the entire method expression.
  • T, also referred to as the method’s head, is a task atom in which no call or eval terms can appear.
  • Each Ci, a precondition for the method, is a logical precondition; see Logical Precondition.
  • Each Ti, called a tail of the method, is a task list. The task atoms in the list can contain call terms.
  • Each ni is the name for the succeeding Ci Ti pair. These names are optional and if omitted a unique name will be assigned for each pair. The names have no semantic meaning to SHOP3, but are provided in order to help the user debug domain descriptions by looking at traces of SHOP3’s behavior.

A method indicates that the task specified in its head can be performed by performing all of the tasks in one of its tails, when that tail’s precondition is satisfied. The preconditions in a method are considered in the order given, and a later precondition is considered only if all of the earlier ones are not satisfied.

On the other hand, if there are multiple top-level methods for a given task available at some point in time, all of these methods will be considered (through backtracking). Consequently, the following code:

(:method (eat ?food)
    (have-fork ?fork)
    ((!eat-with-fork ?food ?fork))
    (have-spoon ?spoon)
    ((!eat-with-spoon ?food ?spoon))

is semantically equivalent to the following code with multiple methods and explicitly exclusive preconditions:

(:method (eat ?food)
   (have-fork ?fork)
   ((!eat-with-fork ?food ?fork)))

(:method (eat ?food)
    (and (not (have-fork ?fork)) (have-spoon ?spoon))
    ((!eat-with-spoon ?food ?spoon))

In both of the above examples, the !eat-with-spoon operator may be performed only if (have-spoon ?spoon) is satisfied and (have-fork ?fork) is not satisfied.

This should be compared with the following case, where one is permitted to eat with either fork or spoon – where the spoon is not limited to use when a fork is not available:

(:method (eat ?food)
   (have-fork ?fork)
   ((!eat-with-fork ?food ?fork)))

(:method (eat ?food)
    (have-spoon ?spoon)
    ((!eat-with-spoon ?food ?spoon))

In this case, both alternatives will be tried.


4.12 Planning Domain

A planning domain is an object that contains all of the information for solving a class of planning problems3. At a minimum, it will include definitions of the operators (or actions) and methods available in the domain. A planning domain definition may also contain axioms, or other items that are accepted by specific SHOP domain extensions. Finally, a domain definition can include other domains by reference, see Inclusion directives.


4.12.1 Simple Form

A planning domain definition in the simple form looks like this:

(defdomain domain-name (i1 i2in))

where domain-name is a symbol (which does not need to be quoted). Beginning users of SHOP3 should simply use the simple domain-name form of this argument.

Each item ii is one of the following: an operator, a method, or an axiom.


4.12.2 Extended form

The extended form of the SHOP3 domain definition looks like this:

(defdomain (domain-name &rest args) (i1 i2in))

args includes the following keyword arguments:

  • a :type keyword argument, allowing the domain modeler to indicate a specific subclass of the SHOP3 domain class. E.g., one might have (my-domain :type pddl-domain).
  • A :redefine-ok argument. If this is NIL (the default), defdomain will warn when the domain domain-name is already defined.
  • A :noset argument. Should the dynamic variable *domain* be bound as a side-effect of evaluating the defdomain expression?Currently this defaults to NIL, to provide for backward compatibility, but I would like to see this move to defaulting to T. See discussion of *domain* below.

4.12.3 The *domain* variable

This is actually a bit of a kludge. The existing defdomain implementation, as a side-effect, sets the global variable *domain*. If this were only a default domain name, that would be fine, but it is used everywhere as a special variable to mean “the domain within which we are planning.” So if there’s concurrent action, or there are multiple copies of SHOP (or its component libraries) running in a single Lisp image, bad things can happen. I would like to stamp out the use of *domain* as a default domain.

The question of which additional arguments are accepted in args is a matter for the implementer of the specialized domain type4 being used. Any additional arguments will be passed to the make-instance method for the domain subclass.5 SHOP3 extenders can create new subclasses of domain that accept initialization arguments. A first example of the use of this is the built-in pddl-domain class.

If you are using the extended form of defdomain, you should have in hand a new SHOP3 domain subclass, with a description of its arguments. If you do not, you should ignore the extended form.


4.12.4 Inclusion directives

A domain definition can include the items of another domain by reference using the include directive:

(:include domain-name file-name)

for example

(:include flight-operators
  #.(asdf:system-relative-pathname "core-domains" "domains.lisp"))

would take the text of the flight-operators domain, which should be found in the domains.lisp file. Note the use of the reader evaluation form – #. – to force evaluation of the expression that yields the pathname.

Designer’s Note: SHOP3’s inclusion directive is a mess. SHOP3 really needs an inclusion directive, but it is a poor fit to defdomain, because the latter is an executable macro, but the inclusion directive is inherently file-based, rather than code (s-expression)-based. I have not been able to come up with a more graceful solution, however. –rpg


4.13 Planning Problem

A planning problem has the form

(defproblem problem-name domain-name (a1 a2an) T)

where problem-name is a symbol, domain-name is a symbol, each ai is a ground logical atom, and T is a task list. This form defines a problem which may be solved by addressing the tasks in T, using the operators, methods and axioms in domain-name, starting in an initial state defined by the ground atoms a1 through an.

Macro: defproblem problem-name &rest args

(defproblem {<name>|<name-and-options>} <state> <tasks>) For backward compatibility, will support also (defproblem <name> <domain-name> <state> <tasks>).

The corresponding functional interface is:

Function: make-problem problem-name-etc state tasks &rest extras

make-problem creates a planning problem named problem-name by putting state and task onto PROBLEM-NAME’s property list under the indicators :state and :tasks. As a side effect, sets the global variable *problem*.


4.14 Planning Problem Set

A planning problem set has the form

(def-problem-set set-name (p1 p2pn))

where set-name is a symbol and each pi is the name of a planning problem.


4.15 Plans

The previous subsections describe the inputs to SHOP3. This subsection describes the result that SHOP3 produces. A plan is a list of the form

(h1 c1 h2 c2 … hn cn )

where each hi and ci, respectively, are the head and the cost of a ground operator instance oi. If p = (h1 c1 h2 c2hn cn) is a plan and S is a state, then p(S) is the state produced by starting with S and executing o1, o2, …, on in the order given. The cost of the plan p is c1 + c2 + … + cn (thus, the cost of the empty plan is 0).

Often what is wanted is a truncated version of the plan sequence, with the internal operators (see internal operators) and costs removed. For this, one may use

Function: shorter-plan plan

Removes the internal operators and costs from a plan sequence, and returns the resulting new sequence. Non-destructive.


Previous: , Up: The SHOP3 Formalism   [Contents][Index]

4.16 Simple example

This very simple, ready-to-run example illustrates the basics of what we’ve covered so far about SHOP3.

(in-package :shop-user)

(defdomain simple
    (
     (:op (!pickup ?a)
      :add ((have ?a)))

     (:op (!drop ?a)
      :precond (and (have ?a))
      :delete ((have ?a)))

     (:method (swap ?x ?y)
       dec0
       (and (have ?x) (have ?y))
       () ; nothing to do
       dec1
       ((have ?x))
       ((!drop ?x) (!pickup ?y))
       dec2
       ((have ?y))
       ((!drop ?y) (!pickup ?x)))
     )
  )

(defproblem p1 simple
  ((have banjo))       ; facts
  ((swap banjo kiwi))  ; task list
  )

(find-plans 'p1 :verbose :plans)


5 PDDL Support

The current release of SHOP3 provides a preliminary capability to incorporate PDDL domain definitions into a SHOP3 domain. You should be able to incorporate components of a PDDL domain definition into a SHOP3 domain definition of :type pddl-domain or simple-pddl-domain. A pddl-domain corresponds to a PDDL domain of the ADL type. The pddl-domain uses conditional-effects, existential-preconditions, universal-preconditions, and equality (note that these are PDDL conditional effects, existential preconditions and universal preconditions; these are not SHOP-syntax conditional effects, etc.). A simple-pddl-domain will not have conditional-effects, existential-preconditions, universal-preconditions, or equality.

Currently the PDDL integration is a little bumpy, and details are in flux.

PDDL action names are translated into names that SHOP will recognize as primitives (e.g., move would become !move, and would have to be referenced that way in SHOP method definitions that use it).

You must splice the PDDL domain components into the SHOP domain definition. Typically, the best way to do this is to use an :include form (see Inclusion directives ).

Fully ground STRIPS-style domains – i.e., those where a set of STRIPS operators has been exploded into a large set of ground operators by some automated transformation – will work very poorly.

Note that the parsing of PDDL domains in SHOP is not strict. This is intentional, because we don’t want to make it impossible to include SHOP constructs together with PDDL constructs. However, there should probably be a “strict mode” that checks for true conformance with PDDL syntax.


Next: , Previous: , Up: PDDL Support   [Contents][Index]

5.1 PDDL Metric Fluents

We have recently added support for PDDL operators with metric fluents, signaled by PDDL’s :fluents requirement. Metric fluents are numerically-valued functions of domain objects. Here is an example taken from Fox and Long’s paper on PDDL 2.1, and updated to the changes in PDDL syntax they specify:

(define (domain jug-pouring)
  (:requirements :typing :fluents)
  (:types jug)
  (:functions
   (amount ?j - jug) (capacity ?j - jug))
  (:action empty
    :parameters (?jug1 ?jug2 - jug)
    :precondition (>= (- (capacity ?jug2) (amount ?jug2))
                                 (amount ?jug1)))
    :effect (and (assign (amount ?jug1) 0)
                       (assign (amount ?jug2)
                              (+ (amount ?jug1) (amount ?jug2))))))

In the above example, the two functions are amount and capacity, and we see use of the update operator assign (other such operators are increase, decrease, scale-up, and scale-down), the comparison predicate >= (there are also <=, <, >, and =), and the binary arithmetic operators - and + (* and / are also supported).

See PDDL Domain Classes, specifically the discussion of the fluents-mixin class for more details.

5.1.1 Implementation Notes

As the name suggests, the domain mixin class fluents-mixin is responsible for the correct interpretation of PDDL metric fluents. This requires extensions to the SHOP theorem prover and to the interpretation of PDDL actions.

In its state representation, SHOP stores the current values of metric fluents using the dedicated predicate FLUENT-VALUE, as in, for example: (fluent-value (capacity jug0) 12). When the value of a metric fluent must be found, this is the form of literal that is actually retrieved.

In the grammar of PDDL, there are also fluent expressions (f-exps) that are made up of fluent values, numbers, binary and unary operators. Internally, the SHOP theorem-prover uses the special predicate F-EXP-VALUE to find values of such expressions, and has a special-purpose inference rule coded for them. These expressions appear both in preconditions (as part of comparison predications) and in action effects (as part of updates).

A fluent comparison (f-comp in the PDDL grammar) is a binary comparison applied to two f-exps. Internally, the theorem-prover uses the distinguished predicate fluent-check to check these. As one would expect, it first evaluates the two fluent expressions and then applies the comparison operator.

When handling updates to fluent expressions, parsing methods on the fluents-mixin class will translate update expressions into new fluent-update expressions of the following form:

(fluent-update update-op fluent-function f-exp)

Special code for handling such effect expressions has been added to the apply-action function in SHOP.


5.2 PDDL Methods

In order to support replanning, we have developed “PDDL methods” that have more limited expressive power than normal SHOP3 methods, and that have clearer semantics. This feature is experimental: the syntax, semantics, and implementation are all likely to change.

PDDL method proposed syntax:

(:pddl-method head[φ] precond[φ] body[φ])

As in normal SHOP3 methods (see Section 4.11), a PDDL Method’s head is a task. We notate it here as head[φ] in order to indicate that some set of variables, φ, may appear free in the head. Similarly, we have precond[φ] and body[φ] to indicate that φ may appear free in the preconditions and the body. A PDDL method’s preconditions must be an enhanced PDDL goal expression (see below). A PDDL method’s body must be an ordered task network. In the interests of clean syntax, task network keywords (:ordered and :unordered) are not optional, and must be provided. For the moment, only ordered task networks are supported; unordered task networks may be supported later.

Note that provision for free variables does not relax the constraint that all operators must be ground when inserted into the plan. The intention is to allow the variables in φ to be bound by the preconditions. As in PDDL operators, only the variables in the head of a PDDL method are scoped over the preconditions and the body (in standard SHOP3 methods we have Prolog-style scoping where any free variable is implicitly scoped over the entire method).

Note also that PDDL methods do not permit multiple precondition sets and task networks in a single PDDL method form, and so do not support the if-then-else semantics of SHOP3 method forms. To get this kind of semantics in PDDL methods, the programmer must supply a set of methods with mutually-exclusive and exhaustive preconditions.

PDDL methods may only be used in domains that are a subclass of SIMPLE-PDDL-DOMAIN (see PDDL Domain Classes).


Previous: , Up: PDDL Methods   [Contents][Index]

5.2.1 Enhanced Preconditions

PDDL method preconditions are based on PDDL goals, but with the following extensions:

  • A PDDL method’s preconditions may use the :sort-by keyword. More precisely:
    P
    ::= PDDL goal
    v
    ::= PDDL/SHOP variable
    P_v
    ::= PDDL goal with v appearing free
    precond
    ::= P | P_v with v a method parameter
       | :sort-by v [<rel>] P_v
  • Variables that appear free in the head of the PDDL method may appear free in the precondition, hence the use of P and P_v.

PDDL goals are as described in the PDDL syntax (we have used the PDDL 2.1 paper as primary source). Note that PDDL goals with free variables are permitted, as long as the free variables appear in the parameters for the task.

Currently we do not support typing in PDDL method task heads, but this could change.


Previous: , Up: PDDL Support   [Contents][Index]

5.3 PDDL Domain Classes

In order to implement the requirements of PDDL, SHOP3 contains a number of classes, which can be used when defining domains with defdomain (see Planning Domain).

  • SIMPLE-PDDL-DOMAIN – this is the base class. All PDDL domain classes should include this class.
  • PDDL-DOMAIN – for historical reasons, this class corresponds roughly to PDDL domains with the ADL requirements. Use of this class is deprecated; it was added without sufficient thought.
  • ADL-DOMAINSIMPLE-PDDL-DOMAIN with ADL-MIXIN (see below).
  • Mixin classes for different requirements:
    • NEGATIVE-PRECONDITIONS-MIXIN
    • DISJUNCTIVE-PRECONDITIONS-MIXIN
    • UNIVERSAL-PRECONDITIONS-MIXIN
    • EXISTENTIAL-PRECONDITIONS-MIXIN
    • QUANTIFIED-PRECONDITIONS-MIXIN – this simply inherits universal and existential preconditions, since they are typically used together.
    • CONDITIONAL-EFFECTS-MIXIN
    • EQUALITY-MIXIN
    • PDDL-TYPING-MIXIN
    • COSTS-MIXIN
    • ADL-MIXIN
    • FLUENTS-MIXIN

6 The SHOP Theorem Prover

One of the main extensions that SIFT has made to SHOP3 is to make its theorem prover usable separately. The SHOP3 theorem-prover is very similar to Prolog, but operates over a state that changes over time. Note, however, that the prover does not (at least not yet) support temporal modalities such as “previously,” “next,” or “always.”

The theorem-prover is supplied only as a toolbox unlike the unifier (see The SHOP Unifier), which provides functionality that is ready to use “out-of-the box.” Specifically, it does not contain any built-in functionality for advancing the world state; this needs to be developed by the programmer, based on facilities supplied by SHOP3’s “common” subsystem. The theorem-prover relies critically on the unifier subsystem, and re-exports most of the key functions from the unifier package.

The top-level function of the theorem-prover is query, which is built on top of the more difficult-to-use find-satisfiers:

Generic Function: query [shopthpr] goals state &key just-one domain record-dependencies

More convenient top-level alternative to find-satisfiers. Manages optional arguments and ensures that the variable property is properly set in goals.

Function: find-satisfiers [shopthpr] goals state &key just-one level domain

Find and return a list of binding lists that represents the answer to goals (a list representation of a deductive query), where state provides the database. level is a non-negative integer indicating the current depth of inference, used in debugging prints, and just-one is a boolean indicating whether you want just one answer (non-nil) or all answers (nil).

The theorem prover has its own notion of a domain object, but unlike the full SHOP3 domain, this one supports only specification of axioms (although it can be extended by the programmer).

Class: thpr-domain [shopthpr]

Class precedence list: thpr-domain, domain-core, has-axioms-mixin, standard-object, t

An object representing a SHOP3 theorem prover domain.


7 The SHOP Unifier

The SHOP3 unifier may be loaded stand-alone with

(asdf:load-system "shop3/unifier")

It provides a library that may be useful for general symbolic computation that requires unification of first order (or, indeed, higher order) logical expressions represented as Lisp s-expressions.

Function: unify [shopunif] e1 e2

Checks to see whether or not E1 and E2 unify, returning a substitution (a binding list) if they do, or fail (*not* nil) if they don’t.

The unify function is also exported from the SHOP3 theorem-prover package and the top level SHOP3 package.

To check the results of unification, SHOP3 offers these predicates:

Macro: unify-p [shopunif] e1 e2

It’s painful (and bug-inducing) to have to remember to compare the result of unify with ’fail. This checks to see whether E1 and E2 unify, and returns t or nil, accordingly.

Macro: unify-fail [shopunif] e1 e2

It’s painful (and bug-inducing) to have to remember to compare the result of unify with ’fail.

Macro: unify-fail-p [shopunif] e1 e2

Better-named alias for unify-fail.

A binding-list or substitution is a list of bindings:

Structure: binding [shopunif]

Class precedence list: binding, structure-object, t

A binding is a structure with a variable and a value.

Accessors:

Function: binding-val [shopunif] instance

Binding structure accessor

Function: binding-var [shopunif] instance

Binding structure accessor

Utility functions:

Function: make-binding-list [shopunif] variables values

Takes a list of variables and values and returns a binding-list.

Function: binding-list-value [shopunif] var binding-list &optional if-not-found

Return the value of var in binding-lisp. When there is no such value, raises an error if if-not-found is :error, else returns the value of if-not-found.

To apply a unifier in a target expression, use apply-substitution:

Macro: apply-substitution [shopunif] target substitution

apply-substitution searches through target, replacing each variable symbol with the corresponding value (if any) in substitution

The following are some predicates that may be useful to a programmer using the unifier at a low level.

Macro: variable-p [shopunif] x

An alias for variablep, for more consistent naming.

Function: variablep [shopunif] x

Is x a symbol representing a logical variable for SHOP’s theorem-prover?

Function: anonymous-var-p [shopunif] x

Does x name an anonymous variable?

Function: groundp [shopunif] literal

Is literal a ground literal? Traverse the tree looking for a variable.

Finally, before unifying, it may be necessary to standardize the expressions – renaming variables to be unique.

Function: standardize [shopunif] expr &optional subs

Replace all variables in expr with newly-generated variables, with new names.


8 Plan Grapher

In order to make the plan trees that SHOP3 can produce more useful, we have developed the SHOP3 plan grapher.

Function: graph-plan-tree [spg] plan-forest &key tree-processor attributes graph-object

Takes a shop plan forest (plan-forest) as input, and returns a cl-dot graph object.

Function: graph-enhanced-plan-tree [spg] plan-tree &key graph-object attributes label-dependencies show-dependencies

Takes an enhanced shop plan tree (plan-tree) as input, and returns a cl-dot graph object.

Class: enhanced-plan-tree-graph [spg]

Class precedence list: enhanced-plan-tree-graph, standard-object, t

A null class that the user may subclass to tailor display of shop enhanced plan trees.

Class: plan-tree-graph [spg]

Class precedence list: plan-tree-graph, standard-object, t

A null class that the user may subclass to tailor display of shop plan trees.


9 Data Structures


9.1 States

A state represents the state of the world at any given time, and is identified with a set of ground literals.6 The meaning of the state is a function of this set of ground literals and the set of axioms in effect. For more discussion of the semantics of states, see see States and Satisfiers.

The programmer may choose from a number of different representations of world states, which may be more or less efficient, depending on the problem at hand:

  • :list – This is the simplest state representation, a simple list of facts. As the set of facts in the state description grows, the linear search for lookup that is required here will become increasingly expensive.
  • :hash – In this representation, the state is represented as a hash table of propositions. The performance of this alternative will depend on how well the host implementation hashes full s-expressions.
  • :mixed – This encoding, which is the default, uses a hash table, but hashes each state literal on its predicate. As long as there are not very large data tables in the state, this should be quite efficient. If there are many facts with the same predicate, this will devolve to linear search.
  • :doubly-hashedNewly added. Similar to the :mixed representation, the state is represented as a hash table, indexed on state predicates. However, each hash bucket in this representation is itself a hash table, indexed on the value of the first argument. This should often improve performance on large data tables, where there are often checks of single facts.
  • :bit – The state is encoded as vectors, based on argument indices, etc. I don’t understand the implementation well, nor do I understand under what conditions it will work well or badly. I believe for this to be correct, the set of possible values for a given predicate’s arguments must be known in advance, but I can’t say for sure. It would be helpful for someone to dig into this more deeply. Until someone does, this representation is probably to be avoided.

Adding a new state representation is a relatively easy thing to do. Any new state data structure must be a structure that extends shop3.common::tagged-state. It must support the following generic functions:

Generic Function: make-initial-state [shop3cmn] domain state-encoding atoms &key

Make a state according to a specified domain type and state encoding. Always takes a list of atoms, for special domain types, may take keyword arguments for additional state components.

Method: around make-initial-state [shop3cmn] (domain fluents-mixin) state-encoding atoms &key

Rewrite initial state facts of the form (= <fluent-function> <value>) into new facts of the form (fluent-value fluent-function value).

Generic Function: state->state-type [shop3cmn] state

Return the state-type keyword for state.

Generic Function: insert-atom [shop3cmn] atom state

Insert the atom into the state. The return value is undefined. This function destructively modifies its state argument. Note that an atom is not a lisp atom --- it is actually a list of pred . args representing a first order logic positive literal.

Generic Function: remove-atom [shop3cmn] atom state

Delete the atom from the statebody. The return value is undefined. This function destructively modifies its state argument. Note that an atom is not a lisp atom --- it is actually a list of pred . args representing a first order logic positive literal.

Generic Function: state-atoms [shop3cmn] state

Return the atoms of the state in a plain list

Method: state-atoms [shop3cmn] (problem problem)

automatically generated reader method

Generic Function: atom-in-state-p [shop3cmn] atom state

Is the atom in the state?

state-all-atoms-for-predicate

state-candidate-atoms-for-goal

Generic Function: copy-state [shop3cmn] state

Return a copy of the state


10 General Notes on SHOP3


10.1 More on axioms

  1. Prolog. SHOP3’s axiom syntax and semantics are like those of Prolog’s Horn clauses.
    • (:- (p ?x) (q ?x)) is patterned after Prolog’s p(x) :- q(x).
    • As in Prolog, there is implicit universal quantification over all variables. For example the axiom
      (:- (p ?x ?y) (q ?x ?z))
      

      means \forall x\,\forall y\,\forall z\; \bigl( q(x,z) \rightarrow p(x,y) \bigr).

  2. Lisp in axioms. An axiom may invoke arbitrary Lisp functions, but only through the eval, call, and assign family of pseudo-predicates. Note that these functions do not have access to the current state, except by using the special variable shop::*current-state*.

    Other predicates are addressed through the theorem-prover. The theorem prover knows about SHOP3’s state and queries will be evaluated in the context of the current state.

    By default, the theorem prover will search for all solutions to a query (you can use the :just-one flag to avoid this), and recursive queries will cause the theorem-prover to go away forever.

  3. Axioms vs. facts. Since the null conjunct is always true, an axiom of the form (:- a nil) is equivalent to asserting the atom a as a basic fact. The difference is that the expression (:- a nil) is what one would put into the set of axioms for the problem domain, whereas the atom a is what one would put into a state description. Such an atom can be deleted by an operator, but with the axiom (:- a nil), a is always true and no operator can change that.
  4. Multiple tails vs. separate axioms. An axiom with several conjuncts in its tail has different semantics than what you would get by making each conjunct the tail of a separate axiom. Consider the following axiom lists:
    X1 = ((:- (a ?x) ((b ?x)) ((c ?x))))
    X2 = ((:- (a ?x) ((b ?x))) (:- (a ?x) ((c ?x))))
    

    In X1, the single axiom acts like an if-then-else: if ((b ?x)) is true then find-satisfiers returns the satisfiers for (b ?x); otherwise if ((c ?x)) is true then it returns the satisfiers for (c ?x). For example,

    (find-satisfiers '((a ?u)) '((b 2) (c 3)))
    

    would return (((?u . 2))).

    On the other hand, in X2 the set of axioms acts like a logical “or”: find-satisfiers returns every satisfier for (b ?x) and every satisfier for (c ?x). In this case,

    (find-satisfiers '((a ?u)) '((b 2) (c 3)))
    

    would return (((?u . 2)) ((?u . 3))).

10.2 Tasks, methods, operators, plans

  1. Since a primitive task name is basically a call to an operator, you should never create a set of methods and operators that has more than one operator for the same primitive task. Otherwise your plans will be ambiguous.
  2. In the following two calls to find-plans SHOP3 will find the same set of all shallowest plans, but in the first case SHOP3 will use a depth-first search and in the second case it will use an iterative-deepening search:
    (find-plans 'p :which :all-shallowest)
    (find-plans 'p :which :id-all)
    

    Likewise, the following two calls to SHOP3 will both find the same shallowest plan, but in the first case SHOP3 will use a depth-first search and in the second case it will use an iterative-deepening search:

    (find-plans 'p :which :shallowest)
    (find-plans 'p :which :id-first)
    

11 Internal Technical Information

This section has not been updated since the transition from SHOP2 to SHOP3, and its accuracy is likely compromised. Caveat lector.

This section presents information about the internal workings of the SHOP3 planning process. Important Note: This section is primarily of interest to planning researchers and planning system developers. Most SHOP3 users (especially beginning users) are advised to skip this section.

The first subsection presents some key internal knowledge structures that must be defined in order to completely specify the behavior of SHOP3. The second subsection presents the formal semantics of operators and plans. The third subsection describes an assortment of functions within SHOP3 that are used to accomplish those semantics.


11.1 Internal Knowledge Structures

The following SHOP3 internal knowledge structures must be defined in order to fully specify the semantics of plan generation in SHOP3.


11.1.1 Substitutions

Update note: The variable bindings in a substitution are no longer represented by dotted pairs. Instead, they are represented by Common Lisp structures that have ‘binding-var‘ and ‘binding-value‘ slots. So, until there has been time for a rewrite, please read “binding structure” for “dotted pair” in the following. [rpg 12 June 2018]

A substitution is a list of dotted pairs of the form

((x1 . t1) (x2 . t2) … (xk . tk))

where every xi is a variable symbol and every ti is a term. If e is an expression and u is the above substitution, then the substitution instance eu is the expression produced by starting with e and replacing each occurrence of each variable symbol xi with the corresponding term ti.

If d and e are two expressions, then:

  • d is a generalization of e if e is a substitution instance of d;
  • d is a strict generalization of e if d is a generalization of e but e is not a generalization of d;
  • d and e are equivalent if each is a generalization of the other.

If u and v are two substitutions, then:

  • u is a generalization of v if for every expression e, eu is a generalization of ev;
  • u is a strict generalization of v if for every expression e, eu is a strict generalization of ev;
  • u and v are equivalent if for every expression e, eu and ev are equivalent.

If e is an expression and x1, x2, …, xk are the variable symbols in e, then a standardizer for e is a substitution of the form

((x1 . y1) (x2 . y2) … (xk . yk))

where each yi is a new variable symbol that is not used anywhere else. Note that if u is a standardizer for e, then e and eu are equivalent expressions.

If d and e are expressions and there is a substitution u such that du = eu, then d and e are unifiable and u is a unifier for them. A unifier of d and e is a most general unifier (or mgu) of d and e if it is a generalization of every unifier of d and e. Note that all mgu’s for d and e are equivalent.


11.1.2 States and Satisfiers

A state is a list of ground atoms intended to represent some “state of the world”. A conjunct C is a consequent of a state S and an axiom list X if every logical expression l in C is a consequent of S and X. A logical expression l is a consequent of S and X if one of the following is true:

  • l is an atom in S;
  • l is a ground expression of the form (eval f t1 t2 … tn), and the evaluation of f with arguments t1,t2,…,tn returns a non-nil value;
  • l is a ground expression of the form (call f t1 t2 … tn), and the evaluation of f with arguments t1,t2,…,tn returns a non-nil value;
  • l is an expression of the form (not a), and the atom a is not a consequent of S and X;
  • l is an expression of the form (assign v t), where v is a variable symbol and t is any Lisp expression. The value of t, which was evaluated via a call to the Lisp evaluator, is a substitution of v, i.e.( v . t). This term is always a consequent of S and X;
  • l is an expression of the form (or l1 l2 … ln), where l1, l2, l3, …, ln are logical expressions, and at least one expression in this list is a consequent of S and X;
  • l is an expression of the form (forall V Y Z), where Y and Z are logical expressions and V is the list of variables in Y such that for every satisfier u that satisfies Y in S and X, u also satisfies Z in S and X;
  • l is an expression of the form (imply Y Z), where Y and Z are logical expressions such that any satisfier u that satisfies Y in S and X also satisfies Z in S and X;
  • there exists a substitution v and an axiom (:- a n1 C1 n2 C2 … nn Cn) in X such that l = av and one of the following holds:
    • C1v is a consequent of S and X;
    • C1v is not a consequent of S and X, but C2v is a consequent of S and X;
    • neither C1v nor C2v is a consequent of S and X, but C3v is a consequent of S and X;
    • …;
    • none of C1v, C2v, C3v, …, Cn-1v is a consequent of S in X, but Cnv is a consequent of S and X.

If C is a consequent of S and X, then it is a most general consequent of S and X if there is no strict generalization of C that is also a consequent of S and X.

Let S be a state, X be an axiom list, and C be an ordinary conjunct. If there is a substitution u such that Cu is a consequent of S and X, then we say that S and X satisfy C and that u is the satisfier. The satisfier u is a most general satisfier (or mgs) if there is no other satisfier that is a strict generalization of u. Note that C can have multiple non-equivalent mgs’s. For example, suppose X contains the “walking distance” axiom given earlier, and S is the state

((weather-is good)
 (distance home convenience-store 1)
 (distance home supermarket 2))

Then for the conjunct ((walking-distance ?y)), there are two mgs’s from S and X: ((?y . convenience-store)) and ((?y . supermarket)).

Let S be a state, X be an axiom list, and C = (:first C') be a tagged conjunct. If S and X satisfy C’, then the mgs (most general satisfier) for C from S and X is the first mgs for C’ that would be found by a left-to-right depth-first search. For example, if S and X are as in the previous example, then for the tagged conjunct (:first (walking-distance ?y)), the mgs from S and X is ((?y . convenience-store)).


11.2 Formal Semantics

Recall that a plan is a list of operator invocations with costs and that an operator has an add list and a delete list. Informally, the meaning of the plan is that the specified operators are performed in sequence, incurring the specified costs. Similarly, the meaning of the operator is that the assertions in the add list are added to the state and the assertions in the delete list are removed from the state. The meaning of a method is that when the method’s precondition is satisfied, the task specified in the method’s head can be performed by performing each of the tasks specified in the method’s tail.

This subsection elaborates these informal notions, presenting detailed formal semantics of operators and plans. It is of particular use to anyone who has a SHOP3 domain and wishes to prove theorems (e.g., correctness, completeness, etc.) regarding plans generated in that domain.


11.2.1 Semantics of Operators

Update note: SHOP3 now supports PDDL operators, which have cleaner (but more restricted) semantics. Their semantics is discussed in many treatments of the PDDL specification. We hope to add an explanation later. See Chapter 7 for discussion of PDDL support in SHOP3. [12 June 2018 – rpg]

The intent of an operator is to specify that the task h can be accomplished at a cost of c, by modifying the current state of the world to remove every logical atom in D and add every logical atom in A if P is satisfied in the current state. In order to prevent plans from being ambiguous, there should be at most one operator for each primitive task symbol. Furthermore, whenever an action is inserted into a plan, it must be ground – there must be no unbound parameters in its task head. [Inserted 12 June 2018 based on discussions with Ugur – rpg]

Let S be a state, X be the list of axioms, L be the list of protected conditions, t be a primitive task atom, and o be a planning operator whose head, precondition, delete list, add list, and cost are h, P, D, A, and c, respectively. Suppose that there is an mgu u for t and h, such that hu is ground, that none of the ground atoms in Du are in the list of protected conditions, and Pu is satisfied in S. Then we say that ou is applicable to t, and that hu is a simple plan for t. If S is a state, then the state and the protection list produced by executing ou (or equivalently, hu) in S and L is the new state:

(S’,L’) = result(S,L,hu) = result(S,L,ou) = (S - Du) U Au.

where S’ and L’ are obtained by modifying the current state of the world and the list of protected conditions as follows:

  • remove every logical atom in Du from the current state;
  • remove every protection condition in Du from the list of protected conditions;
  • for every expression (forall V Y Z) in Du and every satisfier v such that S and X satisfy Yv, remove every logical atom in Zu from the current state;
  • for every expression (forall V Y Z) in Du and every satisfier v such that S and X satisfy Yv,, remove every protection condition in Zu from the list of protected conditions;
  • add every logical atom in Au to the current state;
  • add every protection condition in Au to the list of protected conditions;
  • for every expression (forall V Y Z) in Au and every satisfier v such that S and X satisfy Yv, add every logical atom in Zu to the current state;
  • for every expression (forall V Y Z) in Au and every satisfier v such that S and X satisfy Yv, add every protection condition in Zu to the list of protected conditions.

Here is an example:

S((has-money john 40) (has-money mary 30))
T(!set-money john 40 35)
O
(:operator (!set-money ?person ?old ?new)
    ((has-money ?person ?old))
    ((has-money ?person ?old))
    ((has-money ?person ?new)))
U((?person . john) (?old . 40) (?new . 35))
ou
(:operator (!set-money john 40 35)
    ((has-money john 40))
    ((has-money john 40))
    ((has-money john 35)))
hu(!set-money john 40 35)
Result(S,hu)

result(S,ou)

((has-money john 35) (has-money mary 30) )

((has-money john 35) (has-money mary 30) )

Here is an example using the forall keyword

S((location l1) (location l2) (location l3) (truck-at truck1 l1))
T(!clear-locations)
O
 (:operator (!clear-locations)
    ((forall (?l)
        ((location ?l)
        (not (truck-at ?t ?l)))
    ((location ?l))))
    ())
U()
ou
(:operator (!clear-locations)
    (forall (?l)
        ((location ?l)
         (not (truck-at ?t ?l))))
     ((location ?l))
    ())
hu =(!clear-locations)
Result(S,hu)((location l1) (truck-at truck1 l1))
result(S,ou)((location l1) (truck-at truck1 l1))

11.2.2 Semantics of Methods

The purpose of a method is to specify the following:

  • If the current state of the world satisfies C1, then h can be accomplished by performing the tasks in T1 in the order given;
  • otherwise, if the current state of the world satisfies C2, then h can be accomplished by performing the tasks in T2 in the order given;
  • …;
  • otherwise, if the current state of the world satisfies Ck, then h can be accomplished by performing the tasks in Tk in the order given.

Let S be a state, X be an axiom list, t be a task atom (which may or may not be ground), and m be the method (:method h C1 T1 C2 T2 … Ck Tk). Suppose there is an mgu (most general unifier) u that unifies t with h; and suppose that m has a precondition Ci such that S and X satisfy Ciu; if there is more than one such precondition, then let Ci be the first such. Then we say that m is applicable to t in S and X, with the active precondition Ci and the active tail Ti. Then the result of applying m to t is the set of task lists

R = {CALL((Tiu)v): v is an mgs for Ciu from S and X}

where CALL is SHOP3’s evaluation function (the function that evaluates the values of the call terms in the form (call f t1 t2 .. tn)). Each task list r in R is called a simple reduction of t by m in S and X. Here is an example:

S((has-money john 40) (has-money mary 30))
Xnil
t(transfer-money john mary 5)
M
 (:method (transfer-money ?p1 ?p2 ?amount)
    ((has-money ?p1 ?m1)
     (has-money ?p2 ?m2)
     (call >= ?m1 ?amount))
    (:ordered (:task !set-money ?p1 ?m1 (call - ?m1 ?amount))
                   (:task !set-money ?p2 ?m2 (call + ?m2 ?amount))))
u((?p1 . john) (?p2 . mary) (?amount . 5))
hu(transfer-money john mary 5)
C1u
((has-money john ?m1)
 (has-money mary ?m2)
 (call >= ?m1 5))
T1u
(:ordered
     (:task !set-money john ?m1 (call - ?m1 5))
     (:task !set-money mary ?m2 (call + ?m2 5)))
v((?m1 . 40) (?m2 . 30))
(C1u)v
((has-money john 40)
  (has-money mary 30)
  (call >= 40 30))
(Tu)v
(:ordered
     (:task !set-money john 40 (call - 40 5))
     (:task !set-money mary 30 (call + 30 5)))
call((Tu)v)
(:ordered
     (:task !set-money john 40 35)
     (:task !set-money mary 30 35))

11.2.3 Semantics of Plans

Recall that a planning domain contains axioms, operators, and methods, and that a planning problem is a 4-tuple (S,M,L,D), where S is a state, M is a task list, L is a protection list, and D is a domain representation.  Let T be the list of tasks in M that have no predecessor (i.e., those tasks can be performed at this time if they are applicable).   If t is a task in T, and S is a state, then a reduction of t in S and D with respect to M and L that results in a new planning problem (S’,M’,L’,D)  is defined as follows:

if t is a primitive task, then

(S’, L’) = result(S,L,t);

M’ = the task list produced by removing t from M

else t is a compound task, then

S’ = S;

L’ = L;

Suppose m is an applicable method to t in S, with unifier u, the active precondition Ci and the active tail Ti.

M’ = the task list produced by replace t with Tiu in M

endif

If P = (p1 p2pn) is a plan, then we say that P solves (S,M,L,D), or equivalently, that P achieves M from S in D (we will omit the phrase "in D" if the identity of D is obvious) in any of the following cases:

Case 1.

both M and P are empty.

Case 2.

T = (t1 t2tk) is a list of tasks in M that have no predecessor for which there is a task ti that has the :immediate keyword and is applicable to the current state S.  Let (S’, M’, L’) = reduction(ti, S, M, L).  We say P solves(S,M,L,D) if either of the following is true.

  • ti is primitive and  p1 = ti and (p2  p3 … pn) solves (S’, M’, L’, D)
  • ti is not primitive, and P solves (S’, M’, L’, D)

Case 3.

T = (t1 t2tk) is a list of tasks in M that have no predecessor, where ti is a task in T that’s applicable to the current state S.  Let (S’, M’, L’) = reduction(ti, S, M, L).  We say P solves (S,M,L,D) if either of the following is true.

  • ti is primitive and p1 = ti and (p2  p3 … pn) solves (S’, M’, L’, D)
  • ti is not primitive and P solves (S’, M’, L’, D)

The planning problem (S,M,L,D) is solvable if there is a plan that solves it. For example, suppose that

Snil
M ((:ordered (:task do-both op1 op2)))
T((:task do-both op1 op2))
Lnil
D
(
    (:operator (!do ?operation) nil ((did ?operation)))
    (:method (do-both ?x ?y)
           nil
           (:ordered
               (:task !do ?x)
               (:task !do ?y)))
    (:method (do-both ?x ?y)
        nil
        (:ordered (:task !do ?y)
               (:task !do ?x))))
P1((do op1) 1 (do op2) 1)
P2((do op2) 1 (do op1) 1)

Then P1 and P2 are all of the plans that solve (S,M,L,D).


11.3 Key Functions in SHOP3

Below are some important functions in the Lisp implementation of SHOP3. They should be of interest to anyone who wishes to modify SHOP3 or to directly access internal capabilities of SHOP3. Pseudocode algorithms for the main planning functions of SHOP3 are also presented.

(apply-substitution e u)

e is an expression and u is a substitution. The function returns eu.

(compose-substitutions u v)

If u and v are substitutions, then this function returns a substitution w such that for every expression e, ew = (eu)v.

(standardizer e)

This function returns a standardizer for e.

(standardize e)

This function is equivalent to (apply-substitution e (standardizer e)).

(unify d e)

This procedure returns an mgu for the expressions d and e if they are unifiable, and returns fail otherwise.

(find-satisfiers C S &optional just-one)

If C is a conjunct and S is a state, then this function returns a list of mgs’s, one for every most general instance of C that is satisfied by S. If the optional argument just-one is not nil, then the function returns the first mgs it finds, rather than all of them. Calling (find-satisfiers C S) is roughly equivalent to calling the following (simplified) pseudocode:

procedure find-satisfiers(C, S)

if C is empty then return {nil}

l = the first logical atom in C; B = the remaining logical atoms in C

answers = nil

if l is an expression of the form (not e) then

if find-satisfiers(e, S, nil) = nil then

return find-satisfiers(B, S)

else

return nil

end if

else if l is an expression of the form (eval e) then

if eval(e) is not nil then

return find-satisfiers(B, S)

else

return nil

end if

else if l is an expression of the form (or p1 p2 … pn) then

for every unifier u that unifies any pi with l

for every v in find-satisfiers(Bu, S)

insert compose-substitutions(u,v) into answers

end for

end for

else if l is an expression of the form (imply C1 C2) then

mgu = find-satisfiers(C1, S)

if mgu is null or there exist a unifier u in mgu such that

find-satisfiers(C2u, S) is not equal to nil then

return find-satisfiers(B, S)

else

return nil

end if

else if l is an expression of the form

(forall variables bounds conditions) then

mgu = find-satisfiers(bounds, S)

if mgu is null or for every unifier u in mgu,

find-satisfiers(conditionsu, S) is not equal to nil then

return find-satisfiers(B, S)

else

return nil

end if

else

for every atom s in S that unifies with l

let u be the unifier

for every v in find-satisfiers(Bu, S)

insert compose-substitutions(u,v) into answers

end for

end for

for every axiom x in *axioms* whose head unifies with l

let u be the unifier

if tail(x) contains a conjunct D such that

find-satisfiers(append(Du, Bu), S) is not nil then

let D be the first such conjunct

for every v in find-satisfiers(append(Du, Bu), S)

insert compose-substitutions(u, v)

into answers

end for

end if

end for

end if

return answers

end find-satisfiers

In this pseudo-code, *axioms* is an internal variable of SHOP3. It holds the list of the axioms defined for the domain under consideration.

(apply-method S t m)

If S is a state, t is a task, and m = (:method h C1 T1 C2 T2 … Ck Tk) is a method, then this function does the following:

  • If m is not applicable to t in S, then the function returns the symbol FAIL.
  • If m is applicable to t in S and Ci is the active precondition, then the function returns a list of all simple reductions of Ti, one for each satisfier of Ci in S.

(apply-operator S t o)

If S is a state, t is a task, and o is an operator, then this function does the following:

  • If there is an mgu u for o and t, then it returns the state produced by executing ou in S.
  • Otherwise, it returns FAIL.

(find-plans problem &key which verbose pshort gc pp state plan-tree optimize-cost time-limit explanation)

This function implements the SHOP3 planning algorithm. For more about the arguments to and use of this function, see find-plans. A brief overview of the algorithm for this function is presented here. Calling find-plans is roughly equivalent to calling the following pseudocode, where S is the current state, T is a partially ordered set of tasks, and L is a list of protected conditions:

procedure find-plans (S,T,L)

if T is empty then

return NIL

endif

nondeterministically choose a task t in T that has no predecessors

<r,R’> = reduction (S,t)

if r = FAIL then

return FAIL

endif

nondeterministically choose an operator instance o applicable to r in S

S’ = the state produced from S by applying o to r

L’ = the protection list produced from L by applying o to r

T’ = the partially ordered set of tasks produced from T by replacing t with R’

P = find-plans (S’,T’,L’)

return cons(o,P)

end find-plans

procedure reduction (S,t)

if t is a primitive task then

return <t,NIL>

else if no method is applicable to t in S then

return <FAIL,NIL>

endif

nondeterministically let m be any method applicable to t in S

R = the decomposition (partially ordered set of tasks) produced by m from t

r = any task in R that has no predecessors

<r’,R’> = reduction (S,r)

if r’ = FAIL then

return <FAIL,NIL>

endif

R” = the partially ordered set of tasks produced from R by replacing r with R’

return <r,R”>

end reduction

(defdomain domain-name D)

This macro gives the name domain-name to planning domain D. (More specifically, what it does is to store D’s axioms, operators, and methods on domain-name’s property list.)

(defproblem problem-name domain-name S T)

This macro gives the name problem-name to the planning problem (S,T,D), where D is the planning domain whose name is domain-name. (More specifically, what it does is to store S, T, and domain-name on problem-name’s property list.)

(def-problem-set set-name list-of-problems)

This macro gives the name set-name to the set of planning problems in list-of-problems. (More specifically, what it does is to store list-of-problems on set-name’s property list.)

Note that for backwards compatibility, SHOP3 also accepts the forms make-domain, make-problem, and make-problem-set, which were employed in SHOP 1.x, using the same arguments as defdomain, defproblem, and def-problem-set. The difference between the make-X and def-X forms is that in the latter case since the form is a macro, the arguments are not evaluated. This changes the syntax one uses. Thus in a SHOP 1.x domain one might define a problem as

(make-problem ‘problem-namedomain-name(list of state atoms)(list of tasks to be accomplished))

whereas in SHOP3 the syntax becomes

(defproblem problem-name domain-name
    (list of state atoms)
    (list of tasks to be accomplished))

where the arguments are all quoted in the SHOP 1.x make-problem function, they are unquoted when using the SHOP3 defproblem macro.

(print-axioms &optional name)

This function prints a list of the axioms for the domain whose name is name; defaults to the most recently defined domain.

(print-operators &optional name)

This function prints a list of the operators for the domain whose name is name; defaults to the most recently defined domain.

(print-methods &optional name)

This function prints a list of the methods for the domain whose name is name; defaults to the most recently defined domain.

(get-state name)

This function returns the initial state for the problem whose name is name.

(get-tasks name)

This function returns the list of tasks for the problem whose name is name.

(get-problems name)

This function returns the list of problem names for the problem set whose name is name.

(do-problems name-or-list &rest keywords)

name-or-list should be either a list of problem names or the name of a problem set. This function runs find-plans on each planning problem specified by the list or problem set, and then returns nil. The keywords are simply passed on to find-plans.


12 Acknowledgments

Thanks to Kostas N. Oikonomou for multiple corrections, edits, and improvements to the SHOP3 manual.

Original University of Maryland work on SHOP3 was supported in part by the following grants, contracts, and awards: Air Force Research Laboratory F30602-99-1-0013 and F30602-00-2-0505, Army Research Laboratory DAAL01-97-K0135, and National Science Foundation DMI-9713718, and the University of Maryland General Research Board.

SIFT, LLC work on SHOP3 has been supported by DARPA SBIR contract DAAH01-03-C-R177, Army AFDD contract NAS-0155(MJH), Delivery Order 920, by the Air Force Research Laboratory (AFRL) under contract FA8750-16-C-0182,and by Contract FA8650-11-C-7191 with the US Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory.

SIFT LLC work was also supported by Internal Research and Development.

Joint SIFT, LLC and University of Maryland work was supported by DARPA contract FA8650-06-C-7606.

Previous SIFT work on the manual was supported by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory under Contract No. FA8750-17-C-0184.

Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Defense Advanced Research Projects Agency (DARPA), the Department of Defense, the National Science Foundation, the University of Maryland, SIFT, or the United States Government.


13 References

[Dean and Boddy, 1998] T. Dean and M. Boddy. An analysis of time-dependent planning. In AAAI-88, 1988.

[Ghallab et al., 2004] M. Ghallab, D. Nau, P. Traverso. Automated Planning: Theory and Practice, Morgan Kaufmann, 2004.

[Goldman & Kuter, 2019] Goldman, R. P., & Kuter, U. Hierarchical Task Network Planning in Common Lisp: the case of SHOP3. Proceedings of the 12th European Lisp Symposium. European Lisp Symposium, Genova, Italy, April 2019.

[Nau et al., 1999] D. Nau, Y. Cao, A. Lotem, and H. Muñoz-Avila. SHOP: Simple Hierarchical Ordered Planner. In IJCAI-99, 1999.

[Nau et al., 2000] D. S. Nau, Y. Cao, A. Lotem, and H. Muñoz-Avila. SHOP and M-SHOP: Planning with Ordered Task Decomposition. Tech report TR 4157, University of Maryland, College Park, MD, June 2000.

[Nau et al., 2001] D. S. Nau, H. Muñoz-Avila Y. Cao, A. Lotem, and.S. Mitchell. Totally Ordered Planning with Partially Ordered Subtasks. In IJCAI-01, 2001.


Function and Macro Index

Jump to:   A   B   C   D   E   F   G   I   M   P   Q   R   S   T   U   V  
Index Entry  Section

A
anonymous-var-p [shopunif]: The SHOP Unifier
anonymous-var-p [shopunif]: The SHOP Unifier
APPLY-ACTION: PDDL Metric Fluents
apply-substitution [shopunif]: The SHOP Unifier
apply-substitution [shopunif]: The SHOP Unifier
around make-initial-state [shop3cmn]: States
atom-in-state-p [shop3cmn]: States
atom-in-state-p [shop3cmn]: States

B
binding-list-value [shopunif]: The SHOP Unifier
binding-list-value [shopunif]: The SHOP Unifier
binding-val [shopunif]: The SHOP Unifier
binding-val [shopunif]: The SHOP Unifier
binding-var [shopunif]: The SHOP Unifier
binding-var [shopunif]: The SHOP Unifier

C
copy-state [shop3cmn]: States
copy-state [shop3cmn]: States

D
def-problem-set: Planning Problem Set
defdomain: Simple Form
defdomain: Extended form
defproblem: Planning Problem
defproblem: Planning Problem
defproblem: Planning Problem
do-problems: Running SHOP3
do-problems: do-problems
do-problems: do-problems

E
external-access-hook: Hook Routines

F
find-plans: Running SHOP3
find-plans: find-plans
find-plans: find-plans
find-plans-stack: Running SHOP3
find-plans-stack: find-plans-stack
find-plans-stack: find-plans-stack
find-satisfiers [shopthpr]: The SHOP Theorem Prover
find-satisfiers [shopthpr]: The SHOP Theorem Prover

G
graph-enhanced-plan-tree [spg]: Plan Grapher
graph-enhanced-plan-tree [spg]: Plan Grapher
graph-plan-tree [spg]: Plan Grapher
graph-plan-tree [spg]: Plan Grapher
groundp [shopunif]: The SHOP Unifier
groundp [shopunif]: The SHOP Unifier

I
insert-atom [shop3cmn]: States
insert-atom [shop3cmn]: States

M
make-binding-list [shopunif]: The SHOP Unifier
make-binding-list [shopunif]: The SHOP Unifier
make-initial-state [shop3cmn]: States
make-initial-state [shop3cmn]: States
make-problem: Planning Problem
make-problem: Planning Problem
mk:defsystem: Running SHOP3

P
plan-found-hook: Hook Routines
print-current-plan: Other Debugging Features
print-current-state: Other Debugging Features
print-current-tasks: Other Debugging Features

Q
query [shopthpr]: The SHOP Theorem Prover
query [shopthpr]: The SHOP Theorem Prover

R
remove-atom [shop3cmn]: States
remove-atom [shop3cmn]: States

S
shop-trace: Running SHOP3
shop-trace: Tracing
shop-trace: Tracing
shop-trace: Tracing
shop-untrace: Running SHOP3
shop-untrace: Tracing
shorter-plan: Plans
shorter-plan: Plans
standardize [shopunif]: The SHOP Unifier
standardize [shopunif]: The SHOP Unifier
state->state-type [shop3cmn]: States
state->state-type [shop3cmn]: States
state-atoms [shop3cmn]: States
state-atoms [shop3cmn]: States
state-atoms [shop3cmn]: States

T
trace-query-hook: Hook Routines

U
unify [shopunif]: The SHOP Unifier
unify [shopunif]: The SHOP Unifier
unify-fail [shopunif]: The SHOP Unifier
unify-fail [shopunif]: The SHOP Unifier
unify-fail-p [shopunif]: The SHOP Unifier
unify-fail-p [shopunif]: The SHOP Unifier
unify-p [shopunif]: The SHOP Unifier
unify-p [shopunif]: The SHOP Unifier

V
variable-p [shopunif]: The SHOP Unifier
variable-p [shopunif]: The SHOP Unifier
variablep [shopunif]: The SHOP Unifier
variablep [shopunif]: The SHOP Unifier

Jump to:   A   B   C   D   E   F   G   I   M   P   Q   R   S   T   U   V  

Type and Class Index

Jump to:   A   B   C   D   E   F   N   P   Q   S   T   U  
Index Entry  Section

A
ADL-DOMAIN: PDDL Domain Classes
ADL-MIXIN: PDDL Domain Classes

B
binding [shopunif]: The SHOP Unifier
binding [shopunif]: The SHOP Unifier

C
CONDITIONAL-EFFECTS-MIXIN: PDDL Domain Classes
COSTS-MIXIN: PDDL Domain Classes

D
DISJUNCTIVE-PRECONDITIONS-MIXIN: PDDL Domain Classes

E
enhanced-plan-tree-graph [spg]: Plan Grapher
enhanced-plan-tree-graph [spg]: Plan Grapher
EQUALITY-MIXIN: PDDL Domain Classes
EXISTENTIAL-PRECONDITIONS-MIXIN: PDDL Domain Classes

F
FLUENTS-MIXIN: PDDL Metric Fluents
FLUENTS-MIXIN: PDDL Domain Classes

N
NEGATIVE-PRECONDITIONS-MIXIN: PDDL Domain Classes

P
pddl-domain: The domain variable
PDDL-DOMAIN: PDDL Domain Classes
PDDL-TYPING-MIXIN: PDDL Domain Classes
plan-tree-graph [spg]: Plan Grapher
plan-tree-graph [spg]: Plan Grapher

Q
QUANTIFIED-PRECONDITIONS-MIXIN: PDDL Domain Classes

S
SIMPLE-PDDL-DOMAIN: PDDL Domain Classes

T
thpr-domain [shopthpr]: The SHOP Theorem Prover
thpr-domain [shopthpr]: The SHOP Theorem Prover

U
UNIVERSAL-PRECONDITIONS-MIXIN: PDDL Domain Classes

Jump to:   A   B   C   D   E   F   N   P   Q   S   T   U  

Variable Index

Jump to:   *
Index Entry  Section

*
*break-on-backtrack*: Other Debugging Features
*break-on-backtrack*: Other Debugging Features
*current-plan*: Other Debugging Features
*current-state*: Other Debugging Features
*current-state*: More on axioms
*current-tasks*: Other Debugging Features
*domain*: The domain variable
*problem*: Planning Problem
*which*: Common Keyword Arguments

Jump to:   *

Next: , Previous: , Up: SHOP3 Manual   [Contents][Index]

Concept Index

Jump to:   :  
A   D   E   F   H   I   L   O   P   Q   R   S  
Index Entry  Section

:
:include: Inclusion directives

A
anonymous variables: Syntax Checks
assignment: Assignments
Axioms: Axioms

D
defdomain, extended form: Extended form
depth-first search: Common Keyword Arguments
domain: Planning Domain
domain :noset argument: Extended form
domain :redefine-ok argument: Extended form
domain :type argument: Extended form
domain inclusion: Inclusion directives

E
example: Simple example
explanation: Common Keyword Arguments

F
F-EXP-VALUE: PDDL Metric Fluents
FLUENT-CHECK: PDDL Metric Fluents
FLUENT-VALUE: PDDL Metric Fluents

H
hook-routines: Hook Routines

I
implicit conjunction: Conjuncts
include directives: Inclusion directives
internal operators: Internal Operators
iterative-deepening search: Common Keyword Arguments

L
loading SHOP3: Running SHOP3

O
Operators, deterministic: Operators must be deterministic

P
PDDL method preconditions: Enhanced Preconditions
planning problem: Planning Problem
plans: Plans
protections: Protection conditions

Q
quoting in call and eval terms: Eval Terms

R
running SHOP3: Running SHOP3

S
short-circuit evaluation: Axioms
singleton variables: Syntax Checks
Sorting in PDDL method preconditions: Enhanced Preconditions

Jump to:   :  
A   D   E   F   H   I   L   O   P   Q   R   S  

Previous: , Up: SHOP3 Manual   [Contents][Index]

Colophon

This manual is maintained in Texinfo, and automatically translated into other forms (e.g. HTML or pdf). If you’re reading this manual in one of these non-Texinfo translated forms, that’s fine, but if you want to modify this manual, you are strongly advised to seek out a Texinfo version and modify that instead of modifying a translated version.

This manual was made possible in part by the SB-TEXINFO library provided by Nikodemus Siivola and Rudi Schlatte, for which we are very grateful.


Footnotes

(1)

Previous methods of starting SHOP3, by hand-coded load files, and mk:defsystem, are no longer supported.

(2)

A somewhat cumbersome way to verify this is as follows:

(defdomain test-domain ((:- (= ?x ?x) ())))
(query '((= ?foo list)
            (= ?bar 4)
            (assign ?baz (?foo (< ?bar 3) (list '?foo 'fish) (/ 8 ?bar))))
        (shop::make-initial-state 'test-domain :mixed nil)
        :domain 'test-domain)
(3)

The term “class” here is meant informally; the reader should draw no conclusions about programming language classes in the SHOP3 implementation. – rpg

(4)

Which must be a subclass of the shop:domain Common Lisp class.

(5)

If you don’t know what this means, you may safely ignore it.

(6)

Note that the state of the world is not the same as the search state. The (projected) world state is only one component of the search state.