PyNuSMV is a Python framework for experimenting and prototyping BDD-based model checking algorithms based on NuSMV. It gives access to main BDD-related NuSMV functionalities, like model and BDD manipulation, while hiding NuSMV implementation details by providing wrappers to NuSMV functions and data structures. In particular, NuSMV models can be read, parsed and compiled, giving full access to SMV’s rich modeling language and vast collection of existing models.
PyNuSMV is composed of several modules, each one proposing some NuSMV functionalities:
Warning
Before using any PyNuSMV functionality, make sure to call pynusmv.init.init_nusmv() function to initialize NuSMV; do not forget to also call pynusmv.init.deinit_nusmv() when you do not need PyNuSMV anymore to clean everything needed by NuSMV to run.
The pynusmv.dd module provides some BDD-related structures:
Bases: pynusmv.utils.PointerWrapper
Python class for BDD structure.
The BDD represents a BDD in NuSMV and provides a set of operations on this BDD. Thanks to operator overloading, it is possible to write compact expressions on BDDs. The available operations are:
Any BDD operation raises a MissingManagerError whenever the manager of the BDD is None and a manager is needed to perform the operation.
Compute the conjunction of this BDD and other.
Parameters: | other (BDD) – the other BDD |
---|
Determine whether this BDD is included in other or not.
Parameters: | other (BDD) – the BDD to compare |
---|
Determine whether this BDD is equal to other or not.
Parameters: | other (BDD) – the BDD to compare |
---|
Return the FALSE BDD.
Parameters: | manager (DDManager) – the manager of the returned BDD |
---|
Universally abstract all the variables in cube from this BDD.
Parameters: | cube (BDD) – the cube |
---|
Existentially abstract all the variables in cube from this BDD.
Parameters: | cube (BDD) – the cube |
---|
Compute the IFF operation on this BDD and other.
Parameters: | other (BDD) – the other BDD |
---|
Compute the IMPLY operation on this BDD and other.
Parameters: | other (BDD) – the other BDD |
---|
Determine whether the intersection between this BDD and other is not empty.
Parameters: | other (BDD) – the BDD to compare |
---|
Determine whether this BDD is less than or equal to other.
Parameters: | other (BDD) – the BDD to compare |
---|
Compute the conjunction of this BDD and other.
Parameters: | other (BDD) – the other BDD |
---|
Bases: pynusmv.utils.PointerWrapper
A BDD list stored as NuSMV nodes.
The BDDList class implements a NuSMV nodes-based BDD list and can be used as any Python list.
Create a node-based list from the Python tuple bddtuple.
Parameters: | bddtuple – a Python tuple of BDDs |
---|
Return a BDDList representing the given tuple, using NuSMV nodes. All BDDs are assumed from the same DD manager; the created list contains the DD manager of the first non-None BDD. If all elements of bddtuple are None, the manager of the created BDDList is None.
Bases: pynusmv.dd.BDD
Python class for inputs structure.
An Inputs is a BDD representing a single valuation of the inputs variables of the model, i.e. an action of the model.
Bases: pynusmv.utils.PointerWrapper
Python class for NuSMV BDD managers.
The pynusmv.exception module provides all the exceptions used in PyNuSMV. Every particular exception raised by a PyNuSMV function is a sub-class of the PyNuSMVError class, such that one can catch all PyNuSMV by catching PyNuSMVError exceptions.
Bases: builtins.Exception
A generic PyNuSMV Error, superclass of all PyNuSMV Errors.
Bases: pynusmv.exception.PyNuSMVError
Exception for missing BDD manager.
Bases: pynusmv.exception.PyNuSMVError
Exception for NuSMV lexer error.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when no SMV model has been read yet.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when a model is already read.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when no SMV model has been read yet.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when the model is already flattened.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when the model must be flattened.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when the model is already encoded.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when the flat model is already built.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when the model must be flattened.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when the BDD model is already built.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when the variables of the model must be encoded.
Bases: pynusmv.exception.PyNuSMVError
NuSMV initialisation-related exception.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when an error occured while parsing a string with NuSMV.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when an expression is wrongly typed.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when an error occured while flattening some expression.
Bases: pynusmv.exception.PyNuSMVError
Exception raised when an error occured while picking a state/inputs from a BDD.
Bases: builtins.tuple
An Error is a single parsing error generated by NuSMV parser.
Alias for field number 0
Alias for field number 2
Alias for field number 1
Bases: pynusmv.exception.PyNuSMVError
A NuSMVParsingError is a NuSMV parsing exception. Contains several errors accessible through the “errors” attribute.
The pynusmv.fsm module provides some functionalities about FSMs represented and stored by NuSMV:
Bases: pynusmv.utils.PointerWrapper
Python class for FSM structure, encoded into BDDs.
The BddFsm provides some functionalities on the FSM: getting initial and reachable states as a BDD, getting or replacing the transition relation, getting fairness, state and inputs constraints, getting pre and post images of BDDs, possibly through particular actions, picking and counting states and actions of given BDDs.
Return the number of inputs of the given BDD
Parameters: | bdd (BDD) – the concerned BDD |
---|
Return the number of states of the given BDD.
Parameters: | bdd (BDD) – the concerned BDD |
---|
Return the FSM corresponding to the model in filepath.
Parameters: | filepath – the path to the SMV model |
---|
Return the BDD representing the possible inputs between current and next.
Parameters: |
|
---|---|
Return type: |
Return a tuple of all inputs belonging to bdd.
Parameters: | bdd (BDD) – the concerned BDD |
---|---|
Return type: | tuple(Inputs) |
Raise : | a NuSMVBddPickingError if something is wrong |
Return a tuple of all states belonging to bdd.
Parameters: | bdd (BDD) – the concerned BDD |
---|---|
Return type: | tuple(State) |
Raise : | a NuSMVBddPickingError if something is wrong |
Return a tuple of all states/inputs pairs belonging to bdd.
Parameters: | bdd (BDD) – the concerned BDD |
---|---|
Return type: | tuple(StateInputs) |
Raise : | a NuSMVBddPickingError if something is wrong |
Return a BDD representing an inputs of bdd.
Return type: | Inputs |
---|---|
Raise : | a NuSMVBddPickingError if bdd is false or an error occurs while picking one inputs |
Return a BDD representing a state of bdd.
Return type: | State |
---|---|
Raise : | a NuSMVBddPickingError if bdd is false or an error occurs while picking one state |
Return a BDD representing a state/inputs pair of bdd.
Return type: | StateInputs |
---|---|
Raise : | a NuSMVBddPickingError if bdd is false or an error occurs while picking one pair |
Return the post-image of states in this FSM. If inputs is not None, it is used as constraints to get post-states that are reachable through these inputs.
Parameters: | |
---|---|
Return type: |
Return the pre-image of states in this FSM. If inputs is not None, it is used as constraints to get pre-states that are reachable through these inputs.
Parameters: | |
---|---|
Return type: |
Return a the set of reachable states of this FSM, represented as a BDD.
Return type: | BDD |
---|
Return the weak pre-image of states in this FSM. This means that it returns a BDD representing the set of states with corresponding inputs <s,i> such that there is a state in state reachable from s through i.
Parameters: | states (BDD) – the states from which getting the weak pre-image |
---|---|
Return type: | BDD |
Bases: pynusmv.utils.PointerWrapper
Python class for BDD encoding.
A BddEnc provides some basic functionalities like getting the DD manager used to manage BDDs, the symbols table or the state and inputs masks.
Bases: pynusmv.utils.PointerWrapper
Python class for symbols table.
Bases: pynusmv.utils.PointerWrapper
Python class for transition relation encoded with BDDs.
A BddTrans represents a transition relation and provides pre and post operations on BDDs, possibly restricted to given actions.
The pynusmv.glob module provide some functions to access global NuSMV functionalities. These functions are used to feed an SMV model to NuSMV and build the different structures representing the model, like flattening the model, building its BDD encoding and getting the BDD-encoded FSM.
Besides the functions, this module provides an access to main globally stored data structures like the flat hierarchy, the BDD encoding, the symbols table and the propositions database.
Load a model from an SMV file and store it in global data structures.
Parameters: | filepath – the path to the SMV file |
---|
Flatten the read model and store it in global data structures.
Raise : | a NuSMVNoReadFileError if no model is read yet |
---|---|
Raise : | a NuSMVCannotFlattenError if an error occurred during flattening |
Raise : | a NuSMVModelAlreadyFlattenedError if the model is already flattened |
Warning
In case of type checking errors, a message is printed at stderr and a NuSMVCannotFlattenError is raised.
Return the main symbols table of the current model.
Return type: | SymbTable |
---|
Encode the BDD variables of the current model and store it in global data structures.
Raise : | a NuSMVNeedFlatHierarchyError if the model is not flattened |
---|---|
Raise : | a NuSMVModelAlreadyEncodedError if the variables are already encoded |
Return the main bdd encoding of the current model.
Return type: | BddEnc |
---|
Build the Sexp FSM (Simple Expression FSM) of the current model and store it in global data structures.
Raise : | a NuSMVNeedFlatHierarchyError if the model is not flattened |
---|---|
Raise : | a NuSMVFlatModelAlreadyBuiltError if the Sexp FSM isalready built |
Build the BDD FSM of the current model and store it in global data structures.
Raise : | a NuSMVNeedFlatModelError if the Sexp FSM of the model is not built yet |
---|---|
Raise : | a NuSMVNeedVariablesEncodedError if the variables of the model are not encoded yet |
Raise : | a NuSMVModelAlreadyBuiltError if the BDD FSM of the model is already built |
The pynusmv.init module provides functions to initialize and quit NuSMV.
Warning
init_nusmv() should be called before any other call to pynusmv functions; deinit_nusmv() should be called after using pynusmv.
Initialize NuSMV. Must be called only once before calling deinit_nusmv().
Quit NuSMV. Must be called only once, after calling init_nusmv().
Parameters: | ddinfo – Whether or not display Decision Diagrams statistics. |
---|
Reset NuSMV, i.e. deinit it and init it again. Cannot be called before init_nusmv().
The pynusmv.mc module provides some functions of NuSMV dealing with model checking, like CTL model checking.
Return the set of states of fsm satisfying sexp, as a BDD. sexp is first parsed, then evaluated on fsm.
Parameters: |
|
---|---|
Return type: |
Return the set of states of fsm satisfying spec in context, as a BDD.
Parameters: | |
---|---|
Return type: |
Explain why state of fsm satisfies EX phi, where a is the set of states of fsm satisfying phi, represented by a BDD.
Parameters: |
---|
Return (s, i, s’) tuple where s (State) is the given state, s’ (State) is a successor of s belonging to a and i (Inputs) is the inputs to go from s to s’ in fsm.
Explain why state of fsm satisfies E[phi U psi], where a is the set of states of `fsm satisfying phi and b is the set of states of fsm satisfying psi, both represented by BDDs.
Parameters: |
---|
Return a tuple t composed of states (State) and inputs (Inputs), such that t[0] is state, t[-1] belongs to b, and every other state of t belongs to a. The states of t are separated by inputs. Furthermore, t represents a path in fsm.
Explain why state of fsm satisfies EG phi, where a the set of states of fsm satisfying phi, represented by a BDD.
Parameters: |
---|
Return a tuple (t, (i, loop)) where t is a tuple composed of states (State) and inputs (Inputs), such that t[0] is state and every other state of t belongs to a. The states of t are separated by inputs. Furthermore, t represents a path in fsm. loop represents the start of the loop contained in t, i.e. t[-1] can lead to loop through i, and loop is a state of t.
The pynusmv.parser module provides functions to parse strings and return corresponding ASTs.
Parse a simple expression.
Parameters: | expression (string) – the expression to parse |
---|---|
Raise : | a NuSMVParsingError if a parsing error occurs |
Warning
Returned value is a SWIG wrapper for the NuSMV node_ptr. It is the responsibility of the caller to manage it.
Parse a “next” expression.
Parameters: | expression (string) – the expression to parse |
---|---|
Raise : | a NuSMVParsingError if a parsing error occurs |
Warning
Returned value is a SWIG wrapper for the NuSMV node_ptr. It is the responsibility of the caller to manage it.
Parse an identifier
Parameters: | expression (string) – the identifier to parse |
---|---|
Raise : | a NuSMVParsingError if a parsing error occurs |
Warning
Returned value is a SWIG wrapper for the NuSMV node_ptr. It is the responsibility of the caller to manage it.
The pynusmv.prop module contains classes and functions dealing with properties and specifications of models.
The possible types of properties. This gives access to NuSMV internal types without dealing with pynusmv.nusmv modules.
Bases: pynusmv.utils.PointerWrapper
Python class for properties.
Properties are NuSMV data structures containing specifications but also pointers to models (FSM) and other things.
Bases: pynusmv.utils.PointerWrapper
Python class for property database.
A property database is just a list of properties (Prop). Any PropDb can be used as a Python list.
Bases: pynusmv.utils.PointerWrapper
A CTL specification.
The Spec class implements a NuSMV nodes-based specification. No check is made to insure that the node is effectively a specification, i.e. the stored pointer is not checked against spec types.
Return a new specification corresponding to NOT spec.
Return type: | Spec |
---|
Return a new specification corresponding to left AND right.
Return type: | Spec |
---|
Return a new specification corresponding to left OR right.
Return type: | Spec |
---|
Return a new specification corresponding to left IMPLIES right.
Return type: | Spec |
---|
Return a new specification corresponding to left IFF right.
Return type: | Spec |
---|
Return a new specification corresponding to EX spec.
Return type: | Spec |
---|
Return a new specification corresponding to EG spec.
Return type: | Spec |
---|
Return a new specification corresponding to EF spec.
Return type: | Spec |
---|
Return a new specification corresponding to E[left U right].
Return type: | Spec |
---|
Return a new specification corresponding to E[left W right].
Return type: | Spec |
---|
Return a new specification corresponding to AX spec.
Return type: | Spec |
---|
Return a new specification corresponding to AG spec.
Return type: | Spec |
---|
Return a new specification corresponding to AF spec.
Return type: | Spec |
---|
Return a new specification corresponding to A[left U right].
Return type: | Spec |
---|
The pynusmv.utils module contains some secondary functions and classes used by PyNuSMV internals.
Bases: builtins.object
Superclass wrapper for NuSMV pointers.
Every pointer to a NuSMV structure is wrapped in a PointerWrapper or in a subclass of PointerWrapper. Every subclass instance takes a pointer to a NuSMV structure as constructor parameter.
It is the responsibility of PointerWrapper and its subclasses to free the wrapped pointer. Some pointers have to be freed like bdd_ptr, but other do not have to be freed since NuSMV takes care of this; for example, BddFrm_ptr does not have to be freed. To ensure that a pointer is freed only once, PyNuSMV ensures that any pointer is wrapped by only one PointerWrapper (or subclass of it) if the pointer have to be freed.