PyNuSMV¶

PyNuSMV is a Python framework for prototyping and experimenting with BDD-based model checking algorithms based on NuSMV. It gives access to some main NuSMV functionalities, such as model and BDD manipulation, 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. It makes it easy to implement new logic BDD-based model checking algorithms