Repository of the PlaJA (Planning in JANI) code base.
Models are to be provided in the automata-based input langauge JANI.
Neural networks (where applicable) are to be provided in NNet format.
Additionally, the policy learning module uses the PyTorch format (.pt).
The interface between a JANI model and a neural network is to be documented in Jani2NNet format.
Tree ensemble policies are to be provided in JSON format.
PlaJA uses the nlohmann JSON library for parsing JANI inputs.
The predicate abstraction module (and other SMT modules) depend on
Z3 and
a modified version of Marabou.
Marabou depends on Boost & CxxTest
and (optionally) OpenBLAS & Gurobi.
(Using both is the only configuration actively maintained though.)
The policy learning module depends on PyTorch's C++ distribution LibTorch.
To support tree ensemble policies, Veritas is required. For BDD based computations, CUDD is required.
PlaJA has been successfully build & run with the following versions of the dependencies listed above (on Linux and MacOS):
- nlohmann JSON library version 3.11.2
- Z3 version 4.8.12 commit 3a402ca2c14c3891d24658318406f80ce59b719f (July 13, 2021)
- Boost version 1.81.0 on Linux and on MacOS.
- OpenBlas version 0.3.19.
- Gurobi version 12.0.0.
- LibTorch version 1.8.1 on Linux and 1.12.1 on MacOS.
- CxxTest version 4.4 commit 191adddb3876ab389c0c856e1c03874bf70f8ee4 (June 4, 2014).
- Veritas commit (commit 1df3fc14b57ca58a62a5a77bfdf7e69beb941f5a)
- CUDD version3.0.0
The code base is built using CMake. See CMakeLists.txt and DependenciesConfig.cmake for configuration. Most notably, in the former you can enable/disable modules. This makes sense, if you are not willing to install dependencies of modules not required for your purposes. For instance, if the policy learning functionality is not needed, then you can disable it such that you do not have to install PyTorch.
Consider using cmake.sh, which allows to specify a build type (Release, Debug, ...) and a build directory.
It will use "CodeBlocks - Unix Makefiles".
You then have to run make in the respective build directory.
Alternatively, you might adapt the scripts to, e.g., use Ninja.
Here, you have to run ninja in the respective directory.
The cmake infrastructure has been successfully tested on Linux and MacOS.
After building the PlaJA executable can be found in the respective source directory.
To see basic commandline options you can run
./PlaJA --help
If you additionally set the engine option then commandline options specific to that engine will be provided. For instance,
./PlaJA --help --engine FAULT_ANALYSIS
will additionally output the commandline options specific to the BMC engine.
A basic usage of PlaJA would be
./PlaJA --model-file model.jani --engine EXPLORER
For property-based engines it might make sense to pick a specific property. For instance,
./PlaJA --model-file model.jani --prop 1 --engine BFS
will run BFS for the property with index 1 in the JANI properties array.
Additionally, PlaJA supports additional properties provided in an additional-properties-file which is used for fault analysis
./PlaJA --model-file model.jani --additional-properties additional_properties.jani --prop 1 --engine FAULT_ANALYSIS
The additional properties file must contain a single JSON object composed of a JANI properties array. PlaJA will treat this array as an extension of the properties array in the model file (if present).
To call PlaJA for FaultAnalysis, please use
./PlaJA --engine FAULT_ANALYSIS --help
PlaJA implements a basic search engine infrastructure adapting an extract of a stripped Fast Downward code base (non-public).
The probabilistic search module is an adaption of the Probabilistic Fast Downward implementation.
The successor generation has been designed under the impression of PRISM.
To allow disabling the Marabou dependency when SMT support is not required,
there is a reimplementation of Marabou's neural network parsing functionality.
Moreover, for customization purposes, PlaJA also adapts Marabou's input query generation.
Some auxiliary classes are plain Fast Downward imports, while other adapt from similar routines Fast Downward and Marabou.
For further notes see the reference files in the respective directories.
PlaJA is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.
PlaJA is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/.