VAL is 'The Automatic Validation Tool For PDDL, including PDDL3 and PDDL+'

VAL is used with the executable validate as follows:

validate [options] domain.pddl problem.pddl plan1.pddl plan2.pddl...

where the options are as below in the usage instructions. One or more plans can be validated for the given domain and problem.

Contents


Compilation

The idea is that you should be able to type "make validate" on a standard Gnu make/g++ machine. However, there are some issues caused by dependency on flex/bison generated code, because these systems do not appear to generate uniformly compliant code. The distribution includes pddl+.cpp and lex.yy.cc which are generated by bison and flex respectively. If you get a complaint about one of these files (typically a forward declaration of istream in lex.yy.cc), try deleting the file and regenerating it using your local tools. The distribution also includes FlexLexer.h, which is not always available locally. If the included file causes problems, see whether you have one locally that works better.

In the last resort, contact one of us!

Resources

Description

File

VAL - version 4.2.08, with minor fixes and now reads action-costs syntax of PDDL3.1. Still not handling SAS+ variant, but that is coming... (Jan 2011) VAL-4.2.08.tgz
VAL - version 4.2.07, some significant bug fixes and an extension of capabilities to cover a previously missing situation (quantified conditional temporal effects with preconditions at start and effects at end - rather esoteric and nasty to handle, but included to handle a particular use case!). (July 2010) VAL-4.2.07.tgz
VAL - version 4.2.04, several additions and updates, including instantiation code (December 2008) VAL-4.2.04.tgz
VAL - version 4.2.02, various updates and debugs (January 2008) VAL-4.2.02.tgz
VAL - version 4.2.01, various updates and debugs (1st October 2007) VAL-4.2.01.tgz
VAL - version 4.1, PDDL3/PDDL+ version - processes, events and trajectory constraints (9 May 2006) VAL-4.1.tgz
VAL - version 3.3, handles PDDL3 VAL-3.3.tgz
VAL - version 3.2 VAL-3.2.tgz
VAL - version 3.1 VAL-3.1.tar.gz
VAL - version 3.0 VAL-3.0.tar.gz
R. Howey and D. Long, VAL's Progress: The Automatic Validation Tool for PDDL2.1 used in the International Planning Competition, in Proceedings of the ICAPS 2003 workshop on "The Competition: Impact, Organization, Evaluation, Benchmarks", June 2003, Trento, Italy valsprogress.pdf
Talk from the workshop paper above. val.ppt
Example PDDL2.1 files of the generator problem (with continuous effects). genpddl.tar.gz
An example of a plan validation report. generator.ps
M. Fox and D. Long 2003 PDDL2.1: An extension to PDDL for expressing temporal planning domains. Forthcoming in JAIR special issue on 3rd IPC. pddl2.ps.gz
S. Edelkamp, J. Hoffmann, PDDL2.2: The Language for the Classical Part of the 4th IPC. pddl2.2.ps.gz
S. Thiébaux, J. Hoffmann and B. Nebel. In Defense of PDDL Axioms. IJCAI-03, Morgan Kaufmann, Acapulco (Mexico), August 2003. ijcai03.ps.gz ijcai03.pdf
Extended version of the above. Technical Report TR-ARP-01-03, ANU. Canberra (Australia), February 2003. trarp0103.pdf
R. Howey, D. Long, and M. Fox. Plan Validation and Mixed-Initiative Planning in Space Operations. Proceedings of ECAI Workshop on Planning: Bridging the Gap between Theory and Practice. 2004. mixedinit.pdf
R. Howey, D. Long, and M. Fox. Validating Plans with Exogenous Events. Proceedings of the 23rd Workshop of the UK Planning and Scheduling Special Interest Group. December 2004. events.pdf

Features

VAL validates plans written in PDDL+ (including PDDL2.1 levels 1-4 and PDDL2.2) and features the following:

Continuous Effects

Durative actions may define the rate of change of numerical fluents in the domain thus creating continuous change on the numerical fluents for the duration of the action. For example

(increase (volume ?car) (* #t (refuel-rate ?pump)))

models in PDDL the continuous change of a car's volume of fuel which increases at a constant rate. In general, continuous effects of durative actions give a system of differential equations which must be solved to determine the values of the numerical fluents. This combined with invariant conditions that must hold over certain intervals, which may contain continuously changing quantities, makes validating plans with continuous effects non-trival. An invariant condition to check for example may be:

(t^2 -9t + 14 >= 0 ) OR ( (t-1 > 0) AND (-t + 8 >= 0) ) for t in (0,10)

VAL is capable of validating plans where the continuous effects are defined as functions of time that are polynomials, for more details on continuous effects see the paper on `VAL's Progress' in Resources.

Derived Predicates

VAL is capable of validating plans with derived predicates, they are predicates that are not affected by any of the actions available to the planner. Instead, the predicate's truth values are derived by a set of rules of the form if formula(x) then predicate(x). The semantics are, roughly, that an instance of a derived predicate (a derived predicate whose arguments are instantiated with constants; a fact, for short) is TRUE iff it can be derived using the available rules. An example for a derived predicate is an ``above'' predicate in the Blocksworld, which can be derived by the following rule:

IF on(x, y) OR (exists z: on(x, z) AND above(z, y)) THEN above(x, y)

Note that the ``above'' predicate captures a transitive closure (that of ``on''). This (expressing transitive closures) is also what derived predicates will be used for in IPC-4. For more details on derived predicates see the papers on `In Defense of PDDL Axioms' in Resources.

Timed Initial Literals

VAL is capable of validating plans which have timed initial literals defined in the problem. Timed initial literals are a syntactically very simple way of expressing a certain restricted form of exogenous events: facts that will become TRUE or FALSE at time points that are known in advance. Timed initial literals are thus deterministic unconditional exogenous events. Syntactically, we simply allow the initial state to specify -- beside the usual facts that are true at time point 0 -- literals that will become true at time points greater than 0.

As a syntactic example for a timed initial literal that expresses a time window:

(:init (at 8 (shop-open)) (at 17 (not (shop-open))))

Special actions are inserted into the plan to enact the effects of the timed initial literals when VAL validates a plan using them. For more details on timed initial literals see the PDDL2.2 paper in Resources.

Processes

Processes are used to model continuous change in the world, but unlike durative actions with continuous effects they do not form part of the plan. Continuous change is activated by a process whenever its precondition is satisfied. For example consider the `filling a bath' example where the bath filling process is activated when the flow into the bath is positive. This could be the consequence of turning a tap on for example.

( :process bath_filling
:parameters (?b - bath)
:precondition (> (flow ?b) 0)
:effect (increase (level ?b) (* #t (flow ?b))))

Exogenous Events

Exogenous events are used to model instantaneous changes in the world that may occur as a consequence of change, not necessarily a direct consequence of the actions of an executive. For example if a tap is left running into a bath, a flooding event will occur when the water reaches the top of the bath.

( :event flood
:parameters (?b - bath)
:precondition (and (>= (level ?b) (capacity ?b))
(> (flow ?b) 0)
(dry_floor ?b))
:effect (not (dry_floor ?b)))

Events are particularly intersting when combined with processes in a model, then it is possible for an event to initiate a process. The process in time may then trigger an event which then initiates another processes, and so on. For example, consider the bath where instead of flooding when the water level gets too high the plug is automatically pulled out, which in turn initiates the bath draining process.

The technical details of the semantics of events are not trivial, nor is evaluation of which events should be triggered at a given time point (there may be 1e52 events to check!). For more information see the paper on `Exogenous Events' in Resources.

Plan Repair Advice

When validating a plan if an action precondition is not satisfied then the plan is invalid. Rather than reporting that the action precondition is flawed it would be much more helpful if we were told why the action precondition is not satisfied. And VAL does exactly this! For a given action precondition and a state VAL produces advice on how the state could be altered to satisfy the precondition. For example, consider the action, (read-book bob get-rich-quick), against the state, { (book-is-worth-reading get-rich-quick), (have-book bob get-rich-quick) }:

( :action read-book
:parameters (?b - book ?p - person)
:precondition (or (and (have-book ?p ?b) (book-open ?b))
(not (book-is-worth-reading ?b)))
:effect (book-reviewed ?p ?b))

The advice for this action is to either set (book-open get-rich-quick) to true or set (book-is-worth-reading get-rich-quick) to false. This may seem obvious for this example, but for complex preconditions it can be far from simple. The advice can be very useful if only one predicate has the wrong truth value. For invariant conditions it is more complicated since the condition may be satisfied on a subset of an interval, as well as involving complex continuous effects making it extremely difficult to fix the problem.

For more information see the paper on `Mixed-Initiative Planing' in Resources.

LaTeX Report

When validating a plan there is an option to produce a LaTeX report of the plan validation. To produce output text that compiles with LaTeX use the -l option, for example:

validate -l domain.pddl problem.pddl plan.pddl

The report allows better analysis of a plans validation, as well as providing a more formal record. Included is a Gantt chart which is useful to visualize a plans temporal structure, there are also graphs of the values taken by numerical fluents during a plans execution.

Example of a graph taken from a LaTeX report. The graph shows the fuel level of a generator whilst it is generating. The two bumps are when refuelling is taking place, here the generating continuous effect interacts with the refuelling continuous effects.
Example of a gantt chart taken from a LaTeX report (A key is provided). This example is taken from a rover domain, each rectangle represents a durative action showing its start and end time. The chart hilights concurrent activity in the plan as well as dependencies of actions. Each different colour represents a different rover, this is given with the -o option which defines which type of objects or type of objects to track on the gantt chart.

There is an example LaTeX validation report in Resources.


Usage Instructions

This code is written in C++ using the STL. It is known to compile under Linux with Gnu C++ (3.2.2 and 2.96) and the associated STL.

The current version is more ANSI-standard C++ compliant than previous releases, but this has made it harder to compile under older compilers (particularly where the STL is non-standard, for example). We are attempting to construct versions that will compile under other environments. Windows is our priority, but please contact us if you have other specific needs.

The parser requires flex++ and bison (also Gnu tools).

The Makefile is automatically constructed using makemake with the given Make.header and Make.files. It should not need to be touched if the program is simply constructed "as is".

To build, simply "make".

The executable is "validate". It expects three or more file name arguments: a domain, a problem and one or more plans. There are also many optional arguments that must come first:

-t where is a (floating point format) value determining the tolerance that is to be used in determining whether the plan will execute correctly. In particular, this value must be set small enough to ensure that the time stamps on actions are distinguishable (otherwise the validator will treat those actions with time stamps closer than the tolerance value apart as simultaneous). It defaults to 0.01.
-v makes the output verbose - this is useful to find out more about failing plans.
-l Output a LaTeX report of the plan validation. This is very useful to find out more about failing plans. It includes a Gantt chart and graphs of the values taken by numerical expressions.
-c Continue the plan validation even if an action precondition is not satisfied. The plan will still, of course, be deemed to have failed. Note that a happening containing mutex actions will not have its effects enacted.
-h Display the help message.
-g Use the graphplan length where no metric is specified.
-a Do not output plan repair advice in verbose mode. Useful to reduce the size of reports for badly flawed plans.
-e Produce error report for the full plan. Useful if a error report is required without verbosing the plan.
-p This option allows the Gantt chart to be split across a number of pages. The first value is the number of pages to split the time axis over, the second value is the number of pages to split the rows over. Zero obtains the default value.
-o ... -o Specify a list of the objects and/or types of objects to be tracked on the Gantt chart.
-q This option specifies the number of points to use when drawing each LaTeX graph of PNEs. The more points used the smoother the appearance of the curves. To reduce the size of the graphs change the '\setlength{\unitlength}{100pt}' part in the .tex file to change the point size, such as: '\setlength{\unitlength}{80pt}'. If the graph is required to be really small then the number of points to draw the graph needs to reduced otherwise the LaTeX .tex file will not compile.
-d Do not check set of derived predicates for stratification. Actions are also not checked in case a derived predicate appears as an effect.
-i An invariant may include comparisons with continuously changing numerical expressions in it that are too complex to verify. This option allows the validator to assume that the conditions hold and continues to validate the plan. The plan is then valid subject to these conditions holding -- which may be trivial to prove (or disprove) to a human.
-m Forces the metric to be makespan in temporal plans, regardless of whether another metric was specified.

The validator parses and typechecks domains, problems and plans before confirming that plans are valid. Plans that will not typecheck are listed as failed plans. Plans that fail for reasons that are not clear are listed as queries (verbose mode should clarify what caused this).

You can also build a parser alone, using "make parser" which will build the executable "parser", taking any number of files to syntax check as arguments. The check on problem files requires the associated domain as a preceding argument.

If you find any bugs, have problems compiling or running the system or have any comments please contact:

Derek Long or Maria Fox

Note:
By releasing this code we imply no warranty as to its reliability and its use is entirely at your own risk.

Note that the installation expects to have flex++ if you build it from clean, but the distribution includes the lex.yy.cc file built from pddl+.lex and the FlexLexer.h header file to avoid this dependency being too great a problem.