Probabilistic IC3: A prototype implementation of PrIC3: Property Directed Reachability for MDPs.
You can experiment with PrIC3 in a convenient Docker image, as was provided for the CAV submission.
Build the Docker image: docker build -t pric3 -f cav_artifact/Dockerfile .
More information can be found in cav_artifact/README.md
.
- Run tests with
pytest
: Just executemake test
in this directory (orpytest --doctest-modules -v
for more details). - We use the
yapf
formatter:yapf --recursive -i pric3/
andisort
.
You'll need sphinx
: pip3 install sphinx
.
- To build the documentation:
make docs
. - Then view the documentation in
docs/build/html/index.html
.
To add new modules to the documentation, edit docs/source/index.rst
accordingly.