INVAL is the Independent PDDL plan Validator.
The Planning Domain Definition Language (PDDL) is a modelling language for expressing AI planning problems, and used as the input language of a large number of general-purpose AI planning systems. The role of a plan validator is to check if a plan (generated by an AI planner or manually written) is valid, according to the domain and problem specification. A validator is a very useful tool for debugging a domain/problem specification, a planner implementation, and indeed the specification of PDDL itself.
The existing PDDL plan validator, VAL, created by Derek Long et al., is a great tool, but, like all software, it does have bugs. INVAL is meant to complement VAL, not to replace it. The aim of INVAL is to have a simple (rather than capable and efficient) implementation of the PDDL semantics as they are defined in the literature. When both validators agree, you can have greater confidence that they are right; when they disagree, this points to either a flaw in one of them or an ambiguity in the language specification.
Compared to VAL, INVAL has some limitations. Most importantly, it does not handle temporal plans. It should, however, handle numeric and object-valued fluents, and derived predicates. And it's not efficient.
Compilation and usage
INVAL is written in LISP. For instructions on how to run it, see comments at the beginning of the main file ("inval.lsp").
Other PDDL tools
This package also includes a set of other PDDL tools:
rskis a domain/problem compiler that removes object fluents (PDDL version 3.1). It can either compile them away completely (producing standard ADL-like PDDL) or compile away only nested fluents (producing something analogous to SAS+).
simplifyis a domain/problem simplifier. It outputs "simple ADL", which may still have conditional effects but no quantifiers or disjunction.
nyatconverts PDDL into FastDownward's internal SAS+ format. In other words, it is a drop-in replacement for the FastDownward translator. Compared to the FD translator, it is much less efficient, and it does not automatically generate finite-domain variables from the propositional PDDL representation. Instead (and unlike the FD translator), it preserves any object fluents (i.e., SAS+ variables) in the PDDL input. This means that it gives you full control over the generated SAS+ representation.