Note

In case there is no suitable pre-compiled binary available for your platform and you still want to get started instantly to avoid the hassle of compiling pynusmv for yourself: just give a look at our docker images (https://github.com/LouvainVerificationLab/pynusmv-docker)

In particular, you might want to check the louvainverificationlab/pynusmv image which gives you an access to a running python shell having pynusmv installed. To use it, just

docker run -it louvainverificationlab/pynusmv

Dependencies

The first thing the build process performs in before even stating to try building PyNuSMV is to check the availability of the following system requirements. Unfortunately, no guarantee regarding the exhaustivity of this list can be given although we have strong confidence that it is sufficient.

• An ANSI C compiler (gcc will do, as will several versions of cc)

• A C++ compiler (g++ advised)

• GNU Flex version 2.5 or greater

• GNU Bison version 1.22 or greater

• GNU make utility version 3.74 or greater

• GNU tar, gzip and unzip (to unpack the sources of the dependencies)

• GNU patch (to fix some files in the original project distributions)

• GNU ar and ranlib to create static libraries

• GNU ln command

• SWIG version 2.0.6 or higher – http://www.swig.org/

• Python3 (version 3.4 or higher) – http://python.org/

• Setuptools 2.1 or higher – https://pypi.python.org/pypi/setuptools

• pyparsing version 2.0.2 or higher – http://pyparsing.wikispaces.com/

• Sphinx if you intend to re-build the project documentation.

Build process

To build and install your distribution of pynusmv from the sources, you should proceed with the following command: python3 setup.py install

This will start by unpacking, patching and building the following dependencies:

• MiniSat

• CUDD

• NuSMV

Once that is done, the actual core of setup.py will be executed. This involves building the dynamic libraries for the lower interface and package the python modules that build above that lower interface. As usual, depending on the command you pass to setuptools, the output will be produced under build or dist.

Verifying your build

To check if the compilation was successful and make sure you didn’t break anything in the expected behavior of the lib, you can run the unit tests as such: python3 setup.py test

Docker

If you don’t want to mess with the details of properly provisioning your environment to build pynusmv and simply want to tweak it and build it from the sources; the easiest way is to use one of our preconfigured docker container (https://github.com/LouvainVerificationLab/pynusmv-docker).

In particular, you will probably be interessed by one of the following two containers:

louvainverificationlab/pynusmv-build

if you intend to make a build that works just for you.

louvainverificationlab/pynusmv-manylinux

if you intend to make a build that can possibly run on many different linux flavors.

Note

Alongside with PyNuSMV, the following dependencies are brought to you under the following license terms:

• NuSMV : LGPL (same license as PyNuSMV).

• CUDD: MIT license

• MiniSat: MIT license

• ZChaff: Princeton License (Optional: Iff you decide to use it, –with-zchaff).