Presentation of PyNuSMV¶
PyNuSMV is a Python interface to NuSMV, allowing to use NuSMV as a Python library. It is composed of several classes representing NuSMV data structures and providing functionalities on these data. This page describes the goals behind PyNuSMV and the architecture of the library and, covers its limitations.
Goals¶
The main goal of PyNuSMV is to provide a Python interface for NuSMV functionalities. This interface can be used as a library of functions on models, BDDs, and other data structures of NuSMV.
One subgoal is to provide all the functionalities of NuSMV at the Python level, e.g. calling the bdd_and
function on two bdd_ptrs
. This is achieved by using SWIG, a wrapper generator, to generate a wrapper for every function of NuSMV. Thanks to this wrapper, there are no restrictions to calling NuSMV functions and using its data structures. On the other hand, no barriers are set to forbid erroneous behaviors or to help the user.
Another subgoal is to provide a Python-like library to access the main data structures and functions of NuSMV: FSM, BDD, parser, model checking algorithms, simulation, etc. For example, providing a class BDD
with a built-in operator &
, such that bdd1 & bdd2
computes bdd_and(bdd1, bdd2)
. This library would contain the error mechanisms required to ensure the correct usage of NuSMV.
In summary, PyNuSMV has two main goals:
- providing a complete Python interface for NuSMV functions and data structures;
- providing a Python-like interface to some major data structures and functionalities.
Architecture¶
PyNuSMV is composed of three main layers. The first layer is NuSMV. The second layer is called the lower interface; it contains all the functions of NuSMV, at Python level, wrapped by SWIG. The third layer is called the upper interface; it contains the Python-like functionalities built upon the lower interface.
NuSMV¶
The version of NuSMV used in PyNuSMV is the version 2.5.4. NuSMV code has been kept unchanged, except for very small details:
- some functions and macro declarations have been commented because they are defined twice;
- some static keywords have been removed to allow exporting the functions;
- in the src/cmd/cmdMisc.c file, at line 170, the
nusmv_assert
checking thatstart_time
is-1
has been commented. With this check, it is impossible to initialize, deinitialize and reinitialize NuSMV.
All these changes can be found by searching the commented string “sbusard” in NuSMV sources.
Lower Interface¶
The lower interface is composed of a set Python modules generated by SWIG. For every NuSMV package, i.e. for every sub-directory in the src/ directory of NuSMV, there is a SWIG interface and a Python module that provide wrappers for functions and data structures of the package. This section briefly discusses the structure and content of the lower interface and presents its limitations.
Structure¶
The structure of the lower interface is a copy of the one of NuSMV. Let’s consider as a NuSMV package any sub-directory of the src/ directory of NuSMV sources. For example, NuSMV contains the mc/ and fsm/bdd/ packages. The structure of the lower interface is the same. The lower interface is located in the pynusmv.nusmv
Python package. Every NuSMV package gets its PyNuSMV package. For example, the prop/ NuSMV package is wrapped into the pynusmv.nusmv.prop
Python package; the compile/symb_table/ NuSMV package is wrapped into the pynusmv.nusmv.compile.symb_table
package.
Furthermore, every wrapped function is automatically documented by SWIG with the corresponding C function signature. It allows the developer to know what types of arguments the wrapped function takes.
Content¶
The goal of the lower interface is to provide a wrapper for every function of NuSMV. In practice, for every package, only the set of functions that are considered as public are provided. This means that, for every package, all the headers are exported, except the ones with a name ending with Int.h, _int.h or _private.h.
Limitations¶
The lower interface has some limitations. First, it does not wrap all the functions, but only the ones present in the public headers, as described in the previous section.
Furthermore, there are some exceptions:
- SAT-based functionalities are not exported; the sat/solvers/ NuSMV package is not wrapped.
- the utils/lsort.h header is not wrapped because SWIG cannot process it.
- A set of functions, from different packages, are not wrapped because they have no implementation.
Upper Interface¶
The upper interface is composed of Python classes representing data structures of NuSMV as well as additional modules giving access to main functionalities that do not belong to a data structure, like CTL model checking. Each instance of these classes contains a pointer to the corresponding NuSMV data structure and provides a set of methods on this pointer. This section explains the way all pointers to data structures are wrapped, how the memory is managed and presents an overview of the classes and modules currently defined.
Wrapping pointers¶
Every pointer to a NuSMV data structure is wrapped into a Python class that is a subclass of the PointerWrapper
class. This class contains a _ptr
attribute (the wrapped pointer) and implements the __del__
destructor. All the other functionalities are left to subclasses. This provides a uniform way of wrapping all NuSMV pointers.
Garbage Collection¶
In PyNuSMV, we distinguish two types of pointers to NuSMV data structures: the pointers that have to be freed and the ones that do not. For example, a pointer to a BDD has to be freed after usage (with bdd_free
) while a pointer to the main FSM do not, because NuSMV frees it when deinitializing.
In addition to the wrapped pointer, the PointerWrapper class contains a flag called _freeit
that tells whether the pointer has to be freed when destroying the wrapper. If needed, the destructor calls the _free
method, that does the work. The _free
method of PointerWrapper
class does nothing. It is the responsibility of subclasses to reimplement this _free
method if the pointer has to be freed. In fact, PointerWrapper
cannot say how to free the pointer since the NuSMV function to call depends on the wrapped pointer (BDDs have to be freed with bdd_free
, other pointers need other functions).
Furthermore, we define the following conventions:
- wrappers containing pointers that do not have to be freed do not have to reimplement the
_free
method. - pointers that do not have to be freed can be shared between any number of wrappers. Since these pointers are not freed, there is no problem.
- wrappers containing pointers that have to be freed must reimplement the
_free
method to free the pointer when needed. - there must exist at most one wrapper for any pointer that has to be freed. This ensures that the pointer will be freed only once.
- if no wrapper is created to wrap a pointer, it is the responsibility of the one who got the pointer to free it.
By following these conventions, PyNuSMV can manage the memory and free it when needed.
Thanks to the specific _free
method implementations, pointers can be correctly freed when the wrapper is destroyed by Python. But pointers must not be freed after deinitializing NuSMV. So we need a way to free every pointer before deinitializing NuSMV.
To achieve this garbage collection, PyNuSMV comes with a specific module pynusmv.init
that allows to initialize and deinitialize NuSMV, with the init_nusmv
and deinit_nusmv
functions. Before using PyNuSMV, init_nusmv
must be called; after using PyNuSMV, it is necessary to deinitializing NuSMV by calling deinit_nusmv
. Furthermore, init_nusmv
creates a new list in which every newly created PointerWrapper
(or subclass of it) is registered. When deinit_nusmv
is called, all the wrappers of the list are freed before deinitializing NuSMV. This ensures that all NuSMV data pointers wrapped by PyNuSMV classes are freed before deinitializing NuSMV.
Classes and Modules¶
PyNuSMV is composed of several modules, each one proposing some NuSMV functionalities:
init
contains all the functions needed to initialize and close NuSMV. These functions need to be used before any other access to PyNuSMV.glob
provides functionalities to read and build a model from an SMV source file.dd
provides BDD-related structures like generic BDD, lists of BDDs and BDD-represented states and input values.exception
groups all the PyNuSMV-related exceptions.fsm
contains all the FSM-related structures like BDD-represented FSM, BDD-represented transition relation, BDD encoding and symbols table.prop
defines structures related to propositions of a model; this includes simple CTL specifications.parser
gives access to NuSMV parser to parse simple expressions of the SMV language.mc
contains model checking features.utils
contains some side functionalities.
Limitations¶
PyNuSMV has some limitations. Two major ones are the exposed functionalities and error management.
Exposed functionalities¶
Since the upper interface of PyNuSMV is written by hand, it needs some work to implement its functionalities (compared to the lower interface generated with SWIG). The number of exposed functionalities is relatively small for now. For example, PyNuSMV does not expose SAT-based functionalities like BMC, or LTL model checking and trace generation, simulation and management.
Error Management¶
NuSMV can react in various ways when an error occurs. It can output a message at stderr
and returns an error flag, e.g. when executing a command. It also integrates a try/fail mechanism using lonjmp
functionalities. And it can also abruptly exit using the exit()
function.
For now, there is little error management in PyNuSMV. When possible, the try/fail mechanism has been used to avoid NuSMV to completely exit()
when there is an error. Instead, exceptions are raised, with sometimes error messages from NuSMV. In some cases, errors are correctly raised but a message is printed at stderr
by NuSMV itself. Some future work on PyNuSMV includes a better error management.