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.
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.