Tools

PyNuSMV

PyNuSMV is a Python framework for experimenting and prototyping symbolic model checking algorithms based on NuSMV. It gives access to main NuSMV functionalities, like model, BDD manipulation and reduction to propositional SAT problem, while hiding NuSMV implementation details by providing wrappers to NuSMV functions and data structures. In particular, NuSMV models can be read, parsed and compiled, giving full access to SMV's rich modeling language and vast collection of existing models.

The tool is composed of two layers. The lower interface is a complete Python interface to all NuSMV functions; the upper interface is a Python-like library giving access to main functionalities of NuSMV. While the lower interface does not provide any guards to avoid erroneous behaviors, the upper interface embeds garbage collection and exceptions mechanisms to hide implementation details to the user.

PyNuSMV has already been used to implement:

Tree-Like Annotated Counter-Example for CTL model checking, that is, rich branching counter-examples;
model checking algorithms for ARCTL, an extension of CTL reasoning about the actions of a model;
model checking algorithms for CTLK, an extension of CTL reasoning about knowledge of the agents of a system;
model checking algorithms for CTL and Fair CTL (a reimplementation);
model checking algorithms for ATL, an extension of CTL reasoning about the strategies of the agents of a system;
model checking algorithms for ATLK_irF, an extension of ATL reasoning about strategies under partial observability and fairness constraints.

The source code of these tools is available on GitHub and binaries on PyPI. Hence, these can easily be installed with pip3 install pynusmv-tools

Installation The source code of the framework is available on GitHub and can be installed on OS X an Linux with the following command: pip3 install pynusmv

Documentation The documentation of the project is to be found on ReadTheDocs.

Older versions