VAL

VAL, The Automatic Validation Tool For PDDL, including PDDL3 and PDDL+ Strathclyde Planning Group

VAL is 'The Automatic Validation Tool For PDDL, including PDDL3 and PDDL+' and is used with the executable validate as follows:

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

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

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:

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:

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:

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.

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.

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) }:

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.

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:

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:

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.

Links