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_lower_interface Python package. Every NuSMV package gets its PyNuSMV package. For example, the prop/ NuSMV package is wrapped into the pynusmv_lower_interface.nusmv.prop Python package; the compile/symb_table/ NuSMV package is wrapped into the pynusmv_lower_interface.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 (these are explicitly referred to as ‘internal’ or ‘private’ headers in the NuSMV codebase).

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:

• 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 concrete implementation so far.

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.
• model provides functionalities to define NuSMV models in Python.
• node provides a wrapper to NuSMV node structures.
• 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 CTL specifications.
• dd provides BDD-related structures like generic BDD, lists of BDDs and BDD-represented states, input values and cubes.
• parser gives access to NuSMV parser to parse simple expressions of the SMV language.
• mc contains model checking features.
• exception groups all the PyNuSMV-related exceptions.
• utils contains some side functionalities.
• sat contains classes and functions related to the operation and manipulation of the different sat solvers available in PyNuSMV.
• bmc.glob serves as a reference entry point for the bmc-related functions (commands) and global objects. It defines amongst other the function bmc_setup wich must be called before using any of the BMC related features + the class BmcSupport which acts as a context manager and frees you from the need of explicitly calling bmc_setup.
• bmc.ltlspec contains all the functionalities related to the bounded model checking of LTL properties: from end to end property verification to the translation of formulas to boolean expressions corresponding to the SAT problem necessary to verify these using LTL bounded semantics of the dumping of problem to file (in DIMACS format).
• bmc.invarspec contains all the functionalities related to the verification of INVARSPEC properties using a technique close to that of SAT-based bounded model checking for LTL. (See Niklas Eén and Niklas Sörensson. “Temporal induction by incremental sat solving.” for further details).
• bmc.utils contains bmc related utility functions.
• be.expression contains classes and functions related to the operation and manipulation of the boolean expressions.
• be.fsm contains classes and functions related to PyNuSMV’s description of an FSM when it is encoded in terms of boolean expressions.
• be.encoder provides the boolean expression encoder capabilities that make the interaction with a SAT solver easy.
• be.manager contains classes and functions related to the management of boolean expressions (conversion to reduced boolean circuits. Caveat: RBC representation is not exposed to the upper interface).
• collections impements pythonic wrappers around the internal collections and iterator structures used in NuSMV.
• wff encapsulates the notion of well formed formula as specified per the input language of NuSMV. It is particularly useful in the scope of BMC.
• trace defines the classes Trace and TraceStep which serve the purpose of representing traces (executions) in a PyNuSMV model.
• sexp.fsm contains a representation of the FSM in terms of simple expressions.