Copyright
(c) 1998, 2003, Fahiem Bacchus and Michael Ady. All rights reserved. Use of
this software is permitted for non-commercial research purposes, and it may be
copied only for that use. All copies must include this copyright message. This
software and any documentation and/or information supplied with it is
distributed on an as is basis. Fahiem Bacchus, Michael Ady and the University
of Toronto make no warranties, express or implied, including but not limited to
implied warranties of merchantability and fitness for a particular purpose,
regarding the documentation, functions or performance of such software,
documentation and/or information.
Microsoft,
Windows 95, Windows 98, Windows NT, Windows 2000, Windows XP and MS-DOS are
trademarks or trade names of Microsoft Corporation.
UNIX is a trademark of X/Open Company Ltd.
Intel and Pentium are trademarks or trade names of Intel Corporation.
Sun, Sun Microsystems, SunOS and Solaris are trademarks or trade names
of Sun Microsystems Inc.
This software was developed with support from the Canadian Government
through their NSERC and IRIS programs.
The system
is distributed as a tar file named tlplan.tar Follow the following
sequence of steps.
The README
file gives a bit more detail, and there is also a “runtlplan” file
that can be edited and used to invoke tlplan. To test, move to the
sub-directory and invoke
tlplan
runblockstest.tlp
This should
result the creation of a file “tlplan.log” containing a plan for a
random 1000 blocksworld problem (a random problem generated by the
Slaney-Thiébaux generator, John Slaney and Sylvie Thiébaux Blocks World
revisited Artificial Intelligence 125 (2001): 119-153). On a 2Gz this will take about 1/3 of
a sec. The script file will also terminate tlplan with an (exit) command.
Comment out (with a “;”) this command if you want to enter an
interactive session after the plan has been completed.
The best
place to start is to browse the paper Using Temporal Logics to Express Search Control
Knowledge for Planning. In particular, look at the section that
describes the design of Tlplan. The basic steps are
Commands for Defining a Domain
Initializations
and Declarations
Commands for Defining Operators
Commands for Controlling the Planner
Search Cost
and Priority Routines
Controlling
information generated during planning
Commands for Running the Planner
Commands for Specifying and Manipulating Worlds
Commands
for Handling Files and I/O
Commands for Installing a Domain
Routines
for Interrogating the Current World
Routines
for Retrieving Planning Statistics
Arithmetic
Functions and Predicates
CDF – Cumulative
Distribution Functions
Type: Pseudo-predicate returning true.
Description: Clear the previous domain's
language definition. This command must be called first in a new domain
definition file. This command also calls the reset-print-world-fn command and reset-tl-control. These commands reset the temporal
control formula and the print world command to their defaults.
(declare-defined-symbols
(function|predicate|generator name arity) ...)
Type: Pseudo-predicate returning false on
error.
Description: Declare the defined predicate,
function and generator symbols of the domain. The defined symbols must be
declared after the described symbols. name is the name of the defined symbol (i.e. function, predicate or
generator). arity specifies the number of parameters
accepted by the defined symbol.
(declare-described-symbols
(function|predicate name arity [no-cycle-check|rewritable]) ...)
Type: Pseudo-predicate returning false on
error.
Description: Declare the described predicate and
function symbols of the domain. The described symbols must be declared prior to
any other symbols. name is the name of the described symbol (i.e. function or predicate). arity specifies the number of parameters
accepted by the described symbol.
Optionally,
either qualifier, no-cycle-check and/or rewritable may be specified. If no-cycle-check is specified, then the associated
described symbol will be excluded from cycle-checking. The planner can spend a significant amount of
time doing cycle-checking, and in some circumstances performance can be greatly
improved by excluding certain described symbols from cycle checking. This option can be specified if a particular
function/predicate value never changes, or if it does not affect any of the
decisions made by the planner.
By
default, TLPlan, complains whenever a described predicate is add’ed whenever it is already
asserted or true. If rewritable is specified for a described predicate, then
this warning is suppressed. The use of
this option is not recommended unless you are trying to get someone
else’s domain to work under TLPlan (i.e. the domain semantics are defined
for some other planner). If TLPlan
complains with “Rewriting predicate symbol…” for domains you
have written yourself, then it is most likely that you have a logical error in
you domain definition. Rather than
specifying rewritable for a particular described predicate, first
consider if you have failed to add or delete the symbol in some operator, and
you will almost certainly discover a logical error.
(declare-external-symbols library
(function|predicate|generator|macro name libref arity)
...)
Type: Pseudo-predicate returning false on
error.
Description: Declare the externally defined
predicate, function, generator and macro symbols of the domain. External
symbols must be declared before they are used. library, is the location and name of the
user library. A separate call to assign
a value to the function's name.
Note that formula may include a reference to the current function (thus recursive
function definitions are allowed). To use this feature be sure you understand
the evaluator's early termination rules. With early termination formula can be written so as to ensure any
recursion terminates.
While
parameters and local variables are "local" to the defined function,
they are "global" to all formulas evaluated as a consequence of
evaluating formula.
(def-defined-generator (name
parameters) (local-vars declarations) formula)
Type: Pseudo-predicate returning false on
error.
Description: Include a new generator, defined in
the domain language. name is a symbol which names the new
generator. parameters is a list of variables that are the
arguments of the new generator. declarations is an optional list of local
variables and arrays.
formula is evaluated to calculate the
value(s) of the generator (as a side-effect). To return generated values, the
generator must assign
each value to the appropriate parameter in the parameters list.
In
addition to its parameters, each generator is passed a value that indicates
whether it is being called for the first time or not. This value is passed in a
variable with the same name as the generator, but with a leading '?'. This
variable has a value of 0 the first time the generator is called, and a value
of 1 each time thereafter.
The
first time a generator is called, it must initialize
its context and save important information in its declared local-vars. Each time the generator
successfully generates a new value or set of values, formula must evaluate to true. When the
generator has generated all possible values and wishes to terminate, formula must evaluate to false.
While
parameters and local variables are "local" to the defined generator,
they are "global" to all formulas evaluated as a consequence of
evaluating formula.
(def-defined-predicate
(name parameters) (local-vars declarations) formula)
Type: Pseudo-predicate returning false on
error.
Description: Include a new predicate, defined in
terms of a first-order formula involving other predicates, in the domain
language. name is a symbol naming the new predicate. parameters is a sequence of variables that are the arguments of the new predicate.
declarations is a list of local variables and arrays. formula
is a first-order formula that defines the new predicate. Note that formula may include a reference to the
current predicate (thus recursive predicate definitions are allowed). To use
this feature be sure you understand the evaluator's early termination rules.
With early termination formula can be written so as to ensure any recursion terminates.
While
parameters and local variables are "local" to the defined predicate,
they are "global" to all formulas evaluated as a consequence of
evaluating formula.
Type: Pseudo-predicate returning false on
error.
Description: Define name as an abbreviation for list. This allows macro substitution in
domain definition files.
Type: Pseudo-predicate returning false on
error.
Description: := is a pseudo-predicate that assigns value to ?variable. Note that := is only used to assign
values to variables. = is used to assign values to described functions (among other things).
Type: Term.
Description: Any symbol, number, or string is a
term.
Type: Term.
Description: Any symbol that starts with ? is a variable, and is also a term.
Type: Term.
Description: An array reference is a special
type of variable, and is also a term. The declared dimension of the array must
agree with the number of indices given.
Type: Term.
Description: A list consisting of a function
name followed by a sequence of terms is a term. function is a symbol that has been declared
to be a domain function by one of the initial declarations. (See
Initializations
and Declarations.) The arity of function must agree with the number of terms
given. Note that any of the built-in arithmetic functions can be used as
functions (they do not need to be declared).
Type: Predicate.
Description: A list consisting of a predicate
followed by a sequence of terms is an atomic formula. predicate is a symbol that has been defined
to be a domain predicate one of the initial declarations. (See
Initializations
and Declarations.) The arity of predicate must agree with the number of terms
given.
Type: Predicate.
Description: Equality is a predefined binary
predicate.
Type: Predicate.
Description: The constant atomic formula that
always evaluates to true.
Type: Predicate.
Description: The constant atomic formula that
always evaluates to false.
Type: Predicate.
Description: Any atomic formula is a first-order formula.
Type: Predicate.
Description: The logical and of a sequence of
formulas.
Type: Predicate.
Description: The logical or of a sequence of
formulas.
Type: Predicate.
Description: The logical exclusive or of a
sequence of formulas.
Type: Predicate.
Description: The logical negation of formula.
Type: Predicate.
Description: Logical implication, the result is
true iff formula1 and formula2 are both true or formula1 is false.
(if-then-else formula1
formula2 formula3)
Type: Predicate.
Description: The result is true iff formula1 and formula2 are both true, or
formula1 is false and formula3 is true.
(forall var-gen
... [formula])
Type: Predicate.
Description: Universal quantification, the
formula is true iff formula is true for all bindings of the variables in var-gen that are generated by the generator in var-gen. This formula is trivially TRUE if
the final formula is missing.
Multiple
var-gens may
appear in a quantified formula. This is shorthand for a nested invocation of
the quantifier. For example, the formula:
(forall (?x) (at ROBOT ?x) (?y)
(in ?x ?y) ...)
is
equivalent to:
(forall (?x) (at ROBOT ?x)
(forall (?y) (in ?x ?y) ...))
(exists var-gen
... [formula])
Type: Predicate.
Description: Existential quantification, the
formula is true iff formula is true for some binding of the variables in var-gen that are generated by the generator in var-gen. The last item, formula, is optional. If it is absent then
the formula is true iff the generator in var-gen generates some binding for the
variables in var-gen.
Once
again, multiple var-gens may appear in a quantified formula as shorthand for a nested invocation
of the quantifier. For example, the formula:
(exists (?x) (at ROBOT ?x)
(?y) (in ?x ?y) ...)
is
equivalent to:
(exists (?x) (at ROBOT ?x) (exists
(?y) (in ?x ?y) ...))
(exists!
var-gen ... [formula])
Type: Predicate.
Description: Unique existential quantification,
the formula is true iff formula is true for exactly one binding of the variables in var-gen that are generated by the generator in var-gen. If formula is absent then the formula is true
iff generator generates only a single binding for the variables in var-gen.
When
multiple var-gens appear in a quantified formula, it is shorthand for a nested invocation
of the quantifier. For example, the formula:
(exists! (?x)
(at ROBOT ?x) (?y) (in ?x ?y) ...)
is
equivalent to:
(exists! (?x)
(at ROBOT ?x) (exists! (?y) (in ?x ?y) ...))
(predicate-generator
term ...)
Type: Generator.
Description: Any described predicate can serve
as a generator. Every one of the immediately enclosing quantifier's variables
must appear as a term of this formula. Additional variables appearing in term ... must have been bound by earlier
quantifiers.
Type: Generator.
Description: Any described function can be a
generator. Every one of the immediately enclosing quantifier's variables must
appear as a term of the function. Additional variables appearing in value and term ... must have been bound by earlier
quantifiers.
Note
that described functions generate at most one binding of the quantified
variables.
Type: Generator.
Description: An internal or user defined
computed generator can be used as generator. Every one of the immediately
enclosing quantifier's variables must appear as a term of the generator.
Additional variables appearing in term ... must have been bound by earlier quantifiers.
Look here
for a list of the available internal generators, external or user defined
generators are described here.
Type: Temporal formula.
Description: Any first-order formula is a temporal formula,
as is any first-order formula that contains temporal formulas.
Type: Temporal formula.
Description: This formula is true of a sequence
of states iff the temporal formula tf is true in the next state.
Type: Temporal formula.
Description: This formula is true of a sequence
of states iff the temporal formula tf is true of some future state.
Type: Temporal formula.
Description: This formula is true of a sequence
of states iff the temporal formula tf is true of some future state in the interval ispec.
Type: Temporal formula.
Description: This formula is true of a sequence
of states iff the temporal formula tf is true for all future states.
Type: Temporal formula.
Description: This formula is true of a sequence
of states iff the >Description: This formula is true of a sequence of states
iff the temporal formula tf1 is true in all states until a state is reached
where tf2
is true. Note that if tf2 is true in the current state, then so is the until
formula.
Type: Temporal formula.
Description: This formula is true of a sequence
of states iff the temporal formula tf1 is true in all states until a state
is reached in the interval ispec where tf2 is true.
Type: Temporal formula.
Description: The user should not use this
temporal formula constructor. It is used internally by the planner while progressing formulas. This formula is true iff tf …
(binding (variables)
(values) tf)
Type: Temporal formula.
Description: The user should not use this
temporal formula constructor. It is used internally by the planner while progressing formulas. This formula is true iff tf is true when the variables (that appear in tf) are bound (sequentially) to values.
Modalities
cause their arguments to be evaluated in the context of another world.
Modalities can be applied to any first-order formula, temporal formula or generator,
and the result, respectively, is a first-order formula, a temporal formula or a
generator.
Type: Modality.
Description: The specified first-order formula,
temporal formula or generator is evaluated in the goal world. The goal modality can only be used when
dealing with classical
goals.
(previous formula|tf|generator)
Type: Modality.
Description: The specified first-order formula,
temporal formula or generator is evaluated in the previous state. (previous tf) is always false in the initial world.
(current formula|tf|generator)
Type: Modality.
Description: The specified first-order formula,
temporal formula or generator is evaluated in the current state. This modality
is used with select-initial-world,
select-final-world,
select-previous-world
and select-next-world
to interrogate the results of a planning session.
(def-strips-operator
name pre
Type: Pseudo-predicate returning false on
error.
Description: This command defines a new STRIPS
operator. It accepts seven sub-clauses, described below:
(name v ...)
The name clause declares the name of the
operator and its parameters. The operator is given the name symbol, and the variables, v ..., are declared to be arguments of
the operator.
When
the variables are instantiated, the name and instantiated variables should
provide a unique name for the action. This helps to make clear, just which
operator generated each world. However, there is no requirement that the name
clauses of distinct operators be distinct themselves. Sometimes this feature
can be put to good use, allowing a single logical operation to be split up and
then handled by two or perhaps more operators.
The pre clause declares the precondition
list. This is a list of conditions that must be satisfied before applying the
operator. It is a list of atomic
formulas, including negations
of atomic formulas, i.e., expressions of the form (not atomic-formula). Arbitrary terms can appear in the atomic formulas.
However, every variable in the list of preconditions must first appear as a
term of a non-negated described
predicate. Furthermore, every variable in the name clause must appear as a term in at
least one formula of the pre clause.
The add clause declares the additions list.
The additions list specifies the described predicates that are added to the new
world by the action. The additions list can also specify updates to described functions
which have their values modified in the new world by the action.
The
additions list is a list of atomic
formulas formed from described predicates and described functions.
Arbitrary terms are allowed in these predicates, but every variable that
appears in these terms must have previously appeared in the pre clause.
The
When
modifying the value of a described
function, it is not necessary to first delete the previous value of
the function, before adding the new value. This action is implied by the add. The
only time that the value of a described function might possibly need to be
deleted would be to make the value of the function in question undefined.
The cost clause specifies the cost of the
action, n. n may be a number or a term which
evaluates to a number. The default cost is 1.
The duration clause specifies the duration of
the action, n. n may be an number or a term which evaluates to
a number. The default duration is 1.
The priority clause specifies the priority of
the action, n, an integer. The priority is used during
search to order the successors of a world (dependent on the search strategy).
It defaults to 0. Operations with higher priorities are selected before those
with lower priorities by priority-based search strategies.
(def-adl-operator
name pre modifier-clauses cost duration priority)
Type: Pseudo-predicate returning false on
error.
Description: This command defines a new ADL
operator. It accepts six sub-clauses, described below.
(name v ...)
The name clause declares the name of the operator
and its parameters. The operator is given the name symbol, and the variables, v ..., are declared as the arguments of
the operator.
(pre var-gen ... [formula])
The pre clause declares the precondition
list. It contains a sequence of one or more variable-generator pairs and a
single, optional, first-order
formula. It can be viewed like a quantifier, and has the same syntax
as, for example, the forall
quantifier. Each binding of the variables contained in var-gen that for make formula true generates a single instance of
the ADL action that can be applied to the current world.
modifier-clauses
Each
ADL operator must contain one or more modifier clauses. The modifier clauses
describe what changes to make in the current world to create the new world
generated by each of its instances. Each modifier clause is an arbitrary first-order formula
with the addition of one or more add or
The add and del clauses have the same syntax as the
corresponding STRIPS clauses. However, within ADL operators, add and
Modifier
clauses are preprocessed internally by the planner so that all deletions act
before all additions. When a modifier clause contains both add and
(cost n)
The cost clause specifies the cost of the
action, n. n may be a number or a term which
evaluates to a number. The default cost is 1.
(duration n)
The
duration clause specifies the duration of the action, n. n may be an
number or a term which evaluates to a number. The default duration is 1.
(priority n)
The
priority clause specifies the priority of the action, n, an
integer. The priority is used during search to order the successors of a world
(see search strategy).
It defaults to 0.