.. _pynusmv-overview:

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 <http://www.swig.org>`_, 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.

.. figure:: images/architecture.*
    :align: center
    :width: 12cm
    
    PyNuSMV three-layer architecture
      
      
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 that ``start_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 :mod:`pynusmv.nusmv` Python package. Every NuSMV package gets its PyNuSMV package. For example, the `prop/` NuSMV package is wrapped into the :mod:`pynusmv.nusmv.prop` Python package; the `compile/symb_table/` NuSMV package is wrapped into the :mod:`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 :class:`PointerWrapper <pynusmv.utils.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 :class:`PointerWrapper <pynusmv.utils.PointerWrapper>` class does nothing. It is the responsibility of subclasses to reimplement this ``_free`` method if the pointer has to be freed. In fact, :class:`PointerWrapper <pynusmv.utils.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 :mod:`pynusmv.init` that allows to initialize and deinitialize NuSMV, with the :func:`init_nusmv <pynusmv.init.init_nusmv>` and :func:`deinit_nusmv <pynusmv.init.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 :class:`PointerWrapper <pynusmv.utils.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:

* :mod:`init <pynusmv.init>` contains all the functions needed to initialize and 
  close NuSMV. These functions need to be used before any other access to PyNuSMV.
* :mod:`glob <pynusmv.glob>` provides functionalities to read and build a model 
  from an SMV source file.
* :mod:`dd <pynusmv.dd>` provides BDD-related structures like generic BDD, lists 
  of BDDs and BDD-represented states and input values.
* :mod:`exception <pynusmv.exception>` groups all the PyNuSMV-related 
  exceptions.
* :mod:`fsm <pynusmv.fsm>` contains all the FSM-related structures like 
  BDD-represented FSM, BDD-represented transition relation, BDD encoding and 
  symbols table.
* :mod:`prop <pynusmv.prop>` defines structures related to propositions of a 
  model; this includes simple CTL specifications.
* :mod:`parser <pynusmv.parser>` gives access to NuSMV parser to parse simple 
  expressions of the SMV language.
* :mod:`mc <pynusmv.mc>` contains model checking features.
* :mod:`utils <pynusmv.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.