PyNuSMV Reference¶
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 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.
Warning
Before using any PyNuSMV functionality, make sure to call
init_nusmv
function to initialize NuSMV;
do not forget to also call deinit_nusmv
when you do not need PyNuSMV anymore to clean everything needed by NuSMV to
run.
init
Module¶
The pynusmv.init
module provides functions to initialize and quit NuSMV.
The init_nusmv()
function can be used as a context manager for the with
Python statement:
with init_nusmv():
...
Warning
init_nusmv()
should be called before any other call to
pynusmv functions; deinit_nusmv()
should be called after using
pynusmv.
-
pynusmv.init.
init_nusmv
(collecting=True)[source]¶ Initialize NuSMV. Must be called only once before calling
deinit_nusmv()
.Parameters: collecting – Whether or not collecting pointer wrappers to free them before deiniting nusmv.
-
pynusmv.init.
deinit_nusmv
(ddinfo=False)[source]¶ Quit NuSMV. Must be called only once, after calling
init_nusmv()
.Parameters: ddinfo – Whether or not display Decision Diagrams statistics.
-
pynusmv.init.
reset_nusmv
()[source]¶ Reset NuSMV, i.e. deinit it and init it again. Cannot be called before
init_nusmv()
.
glob
Module¶
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.
-
pynusmv.glob.
load
(*model)[source]¶ Load the given model. This model can be of several forms:
- a file path; in this case, the model is loaded from the file;
- NuSMV modelling code; in this case, model is the code for the model;
- a list of modules (list of
Module
subclasses); in this case, the model is represented by the set of modules.
-
pynusmv.glob.
flatten_hierarchy
(keep_single_enum=False)[source]¶ Flatten the read model and store it in global data structures.
Parameters: keep_single_enum (bool) – whether or not enumerations with single values should be converted into defines Raise: a NuSMVNoReadModelError
if no model is read yetRaise: a NuSMVCannotFlattenError
if an error occurred during flatteningRaise: a NuSMVModelAlreadyFlattenedError
if the model is already flattenedWarning
In case of type checking errors, a message is printed at stderr and a
NuSMVCannotFlattenError
is raised.
-
pynusmv.glob.
symb_table
()[source]¶ Return the main symbols table of the current model.
Return type: SymbTable
-
pynusmv.glob.
encode_variables
(layers={'model'}, variables_ordering=None)[source]¶ Encode the BDD variables of the current model and store it in global data structures. If variables_ordering is provided, use this ordering to encode the variables; otherwise, the default ordering method is used.
Parameters: - layers (
set
) – the set of layers variables to encode - variables_ordering (path to file) – the file containing a custom ordering
Raise: a
NuSMVNeedFlatHierarchyError
if the model is not flattenedRaise: a
NuSMVModelAlreadyEncodedError
if the variables are already encoded- layers (
-
pynusmv.glob.
encode_variables_for_layers
(layers={'model'}, init=False)[source]¶ Encode the BDD variables of the given layers and store them in global data structures.
Parameters: - layers (
set
) – the set of layers variables to encode - init (bool) – whether or not initialize the global encodings
- layers (
-
pynusmv.glob.
bdd_encoding
()[source]¶ Return the main bdd encoding of the current model.
Return type: BddEnc
-
pynusmv.glob.
build_flat_model
()[source]¶ 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 flattenedRaise: a NuSMVFlatModelAlreadyBuiltError
if the Sexp FSM is already built
-
pynusmv.glob.
build_model
()[source]¶ 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 yetRaise: a NuSMVNeedVariablesEncodedError
if the variables of the model are not encoded yetRaise: a NuSMVModelAlreadyBuiltError
if the BDD FSM of the model is already built
-
pynusmv.glob.
flat_hierarchy
()[source]¶ Return the global flat hierarchy.
Return type: FlatHierarchy
-
pynusmv.glob.
compute_model
(variables_ordering=None, keep_single_enum=False)[source]¶ Compute the read model and store its parts in global data structures. This function is a shortcut for calling all the steps of the model building that are not yet performed. If variables_ordering is not None, it is used as a file containing the order of variables used for encoding the model into BDDs.
Parameters: - variables_ordering (path to file) – the file containing a custom ordering
- keep_single_enum (bool) – whether or not enumerations with single values should be converted into defines
model
Module¶
The pynusmv.model
module provides a way to define NuSMV modules in
Python. The module is composed of several classes that fall in five sections:
Expression
sub-classes represent elements of expressions of the NuSMV modelling language. NuSMV expressions can be defined by combining these classes (e.g.Add(Identifier("c"), 1)
), by usingExpression
methods (e.g.Identifier("c").add(1)
) or by using built-in operators (e.g.Identifier("c") + 1
).Type
sub-classes represent types of NuSMV variables.Section
sub-classes represent the different sections (VAR, IVAR, TRANS, etc.) of a NuSMV module.Declaration
sub-classes are used in the declaration of a module to allow a more pythonic way of declaring NuSMV variables.Module
: theModule
class represents a generic NuSMV module, and must be subclassed to define specific NuSMV modules. See the documentation of theModule
class to get more information on how to declare a NuSMV module with this class.
-
pynusmv.model.
Comment
(element, string)[source]¶ Attach the given comment to the given element.
Parameters: - element (Element) – the element to attach the comment to.
- string (str) – the comment to attach.
Returns: the element itself.
-
class
pynusmv.model.
Identifier
(name, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Expression
An identifier.
-
class
pynusmv.model.
Self
(*args, **kwargs)[source]¶ Bases:
pynusmv.model.Identifier
The self identifier.
-
class
pynusmv.model.
Dot
(instance, element, *args, **kwargs)[source]¶ Bases:
pynusmv.model.ComplexIdentifier
Access to a part of a module instance.
-
class
pynusmv.model.
ArrayAccess
(array, index, *args, **kwargs)[source]¶ Bases:
pynusmv.model.ComplexIdentifier
Access to an index of an array.
-
class
pynusmv.model.
Trueexp
(*args, **kwargs)[source]¶ Bases:
pynusmv.model.BooleanConst
The TRUE constant.
-
class
pynusmv.model.
Falseexp
(*args, **kwargs)[source]¶ Bases:
pynusmv.model.BooleanConst
The FALSE constant.
-
class
pynusmv.model.
NumberWord
(value, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Constant
A word constant.
-
class
pynusmv.model.
RangeConst
(start, stop, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Constant
A range of integers.
-
class
pynusmv.model.
Conversion
(target_type, value, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Function
Converting an expression into a specific type.
-
class
pynusmv.model.
WordFunction
(function, value, size, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Function
A function applied on a word.
-
class
pynusmv.model.
Count
(values, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Function
A counting function.
-
class
pynusmv.model.
Next
(value, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Expression
A next expression.
-
class
pynusmv.model.
Smallinit
(value, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Expression
An init() expression.
-
class
pynusmv.model.
Case
(values, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Expression
A case expression.
-
class
pynusmv.model.
Subscript
(array, index, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Expression
Array subscript.
-
class
pynusmv.model.
BitSelection
(word, start, stop, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Expression
Word bit selection.
-
class
pynusmv.model.
Not
(value, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
A negated (-) expression.
-
class
pynusmv.model.
Concat
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
A concatenation (::) of expressions.
-
class
pynusmv.model.
Minus
(value, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
Minus (-) expression.
-
class
pynusmv.model.
Mult
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
A multiplication (*) of expressions.
-
class
pynusmv.model.
Div
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
A division (/) of expressions.
-
class
pynusmv.model.
Mod
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
A modulo (%) of expressions.
-
class
pynusmv.model.
Add
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
An addition (+) of expressions.
-
class
pynusmv.model.
Sub
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
A subtraction (-) of expressions.
-
class
pynusmv.model.
LShift
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
A left shift (<<) of expressions.
-
class
pynusmv.model.
RShift
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
A right shift (>>) of expressions.
-
class
pynusmv.model.
Union
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
A union (union) of expressions.
-
class
pynusmv.model.
In
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The in expression.
-
class
pynusmv.model.
Equal
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The = expression.
-
class
pynusmv.model.
NotEqual
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The != expression.
-
class
pynusmv.model.
Lt
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The < expression.
-
class
pynusmv.model.
Gt
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The > expression.
-
class
pynusmv.model.
Le
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The <= expression.
-
class
pynusmv.model.
Ge
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The >= expression.
-
class
pynusmv.model.
And
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The & expression.
-
class
pynusmv.model.
Or
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The | expression.
-
class
pynusmv.model.
Xor
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The xor expression.
-
class
pynusmv.model.
Xnor
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The xnor expression.
-
class
pynusmv.model.
Ite
(condition, left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The ? : expression.
-
class
pynusmv.model.
Iff
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The <-> expression.
-
class
pynusmv.model.
Implies
(left, right, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Operator
The -> expression.
-
class
pynusmv.model.
ArrayExpr
(array, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Element
An array define expression.
-
class
pynusmv.model.
Word
(size, sign=None, *args, **kwargs)[source]¶ Bases:
pynusmv.model.SimpleType
A word type.
-
class
pynusmv.model.
Scalar
(values, *args, **kwargs)[source]¶ Bases:
pynusmv.model.SimpleType
An enumeration type.
-
class
pynusmv.model.
Range
(start, stop, *args, **kwargs)[source]¶ Bases:
pynusmv.model.SimpleType
A range type.
-
class
pynusmv.model.
Array
(start, stop, elementtype, *args, **kwargs)[source]¶ Bases:
pynusmv.model.SimpleType
An array type.
-
class
pynusmv.model.
Modtype
(modulename, arguments, process=False, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Type
A module instantiation.
-
class
pynusmv.model.
Variables
(variables, *args, **kwargs)[source]¶ Bases:
pynusmv.model.MappingSection
Declaring variables.
-
class
pynusmv.model.
InputVariables
(ivariables, *args, **kwargs)[source]¶ Bases:
pynusmv.model.MappingSection
Declaring input variables.
-
class
pynusmv.model.
FrozenVariables
(fvariables, *args, **kwargs)[source]¶ Bases:
pynusmv.model.MappingSection
Declaring frozen variables.
-
class
pynusmv.model.
Defines
(defines, *args, **kwargs)[source]¶ Bases:
pynusmv.model.MappingSection
Declaring defines.
-
class
pynusmv.model.
Assigns
(assigns, *args, **kwargs)[source]¶ Bases:
pynusmv.model.MappingSection
Declaring assigns.
-
class
pynusmv.model.
Constants
(constants, *args, **kwargs)[source]¶ Bases:
pynusmv.model.ListingSection
Declaring constants.
-
class
pynusmv.model.
Trans
(body, *args, **kwargs)[source]¶ Bases:
pynusmv.model.ListingSection
A TRANS section.
-
class
pynusmv.model.
Init
(body, *args, **kwargs)[source]¶ Bases:
pynusmv.model.ListingSection
An INIT section.
-
class
pynusmv.model.
Invar
(body, *args, **kwargs)[source]¶ Bases:
pynusmv.model.ListingSection
An INVAR section.
-
class
pynusmv.model.
Fairness
(body, *args, **kwargs)[source]¶ Bases:
pynusmv.model.ListingSection
A FAIRNESS section.
-
class
pynusmv.model.
Justice
(body, *args, **kwargs)[source]¶ Bases:
pynusmv.model.ListingSection
A Justice section.
-
class
pynusmv.model.
Compassion
(body, *args, **kwargs)[source]¶ Bases:
pynusmv.model.ListingSection
A COMPASSION section.
-
class
pynusmv.model.
Var
(type_, name=None, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Declaration
A declared VAR.
-
class
pynusmv.model.
IVar
(type_, name=None, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Declaration
A declared IVAR.
-
class
pynusmv.model.
FVar
(type_, name=None, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Declaration
A declared FROZENVAR.
-
class
pynusmv.model.
Def
(type_, name=None, *args, **kwargs)[source]¶ Bases:
pynusmv.model.Declaration
A declared DEFINE.
-
class
pynusmv.model.
Module
(*args, **kwargs)[source]¶ Bases:
pynusmv.model.Modtype
A generic module.
To create a new module, the user must subclass the
Module
class and add class attributes with names corresponding to sections of NuSMV module definitions: VAR, IVAR, FROZENVAR, DEFINE, CONSTANTS, ASSIGN, TRANS, INIT, INVAR, FAIRNESS, JUSTICE, COMPASSION.In addition to these attributes, the ARGS, NAME and COMMENT attributes can be defined:
- If NAME is defined, it overrides module name for the NuSMV module name.
- If ARGS is defined, it must be a sequence object where each element’s string representation is an argument of the module.
- If COMMENT is defined, it will be used as the module’s header, that is, it will be added as a NuSMV comment just before the module declaration.
Treatment of the section depends of the type of the section and the value of the corresponding attribute.
- CONSTANTS section
- If the value of the section is a string (
str
), it is parsed as the body of the constants declaration. Otherwise, the value must be a sequence and it is parsed as the defined constants. - VAR, IVAR, FROZENVAR, DEFINE, ASSIGN sections
If the value of the section is a string (
str
), it is parsed as the body of the declaration. If it is a dictionary (dict
), keys are parsed as names of variables (or input variables, define, etc.) if they are strings, or used as they are otherwise, and values are parsed as bodies of the declaration (if strings, kept as they are otherwise). Otherwise, the value must be a sequence, and each element is treated separately:- if the element is a string (
str
), it is parsed as a declaration; - otherwise, the element must be a sequence, and the first element is used as the name of the variable (or input variable, define, etc.) and parsed if necessary, and the second one as the body of the declaration.
- if the element is a string (
- TRANS, INIT, INVAR, FAIRNESS, JUSTICE, COMPASSION sections
- If the value of the section is a string (
str
), it is parsed as the body of the section. Otherwise, it must be a sequence and the representation (parsed if necessary) of the elements of the sequence are declared as different sections.
In addition to these sections, the class body can contain instances of
pynsumv.model.Declaration
. These ones take the name of the corresponding variable, and are added to the corresponding section (VAR, IVAR, FROZENVAR or DEFINE) when creating the class.For example, the class
class TwoCounter(Module): COMMENT = "Two asynchronous counters" NAME = "twoCounter" ARGS = ["run"] c1 = Range(0, 2) VAR = {"c2": "0..2"} INIT = [c1 == 0 & "c2 = 0"] TRANS = [Next(c1) == Ite("run", (c1 + 1) % 2, c1), "next(c2) = run ? c2+1 mod 2 : c2"]
defines the module
-- Two asynchronous counters MODULE twoCounter(run) VAR c1 : 0..2; c2 : 0..2; INIT c1 = 0 & c2 = 0 TRANS next(c1) = run ? c1+1 mod 2 : c1 TRANS next(c2) = run ? c2+1 mod 2 : c2
After creation, module sections satisfy the following patterns:
- pair-based sections such as VAR, IVAR, FROZENVAR, DEFINE and ASSIGN are mapping objects (dictionaries) where keys are identifiers and values are types (for VAR, IVAR and FROZENVAR) or expressions (for DEFINE and ASSIGN).
- list-based sections such as CONSTANTS are enumerations composed of elements of the section.
- expression-based sections such as TRANS, INIT, INVAR, FAIRNESS, JUSTICE and COMPASSION are enumerations composed of expressions.
-
ARGS
= []¶
-
COMMENT
= ''¶
-
NAME
= 'Module'¶
-
members
= ('__module__', '__qualname__', '__doc__', '__init__', 'NAME', 'COMMENT', 'ARGS')¶
-
source
= None¶
node
Module¶
The pynusmv.node
module provides classes representing NuSMV internal
nodes, as well as a class FlatHierarchy
to represent a NuSMV flat
hierarchary.
-
pynusmv.node.
find_hierarchy
(node)[source]¶ Traverse the hierarchy represented by node and transfer it to the node hash table.
Parameters: node (a SWIG wrapper for a NuSMV node_ptr) – the node
-
class
pynusmv.node.
Node
(left, right, type_=None)[source]¶ Bases:
pynusmv.utils.PointerWrapper
A generic NuSMV node.
-
car
¶ The left branch of this node.
-
cdr
¶ The right branch of this node.
-
-
class
pynusmv.node.
Module
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Section
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
A generic section.
-
class
pynusmv.node.
Trans
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Init
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Invar
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Assign
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Fairness
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Justice
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Compassion
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Spec
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Ltlspec
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Pslspec
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Invarspec
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Compute
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Define
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
ArrayDef
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Isa
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Constants
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Var
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Frozenvar
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Ivar
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Section
-
class
pynusmv.node.
Type
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
A generic type node.
-
class
pynusmv.node.
Boolean
[source]¶ Bases:
pynusmv.node.Type
The boolean type.
-
class
pynusmv.node.
UnsignedWord
(length)[source]¶ Bases:
pynusmv.node.Type
An unsigned word type.
-
length
¶
-
-
class
pynusmv.node.
Word
(length)[source]¶ Bases:
pynusmv.node.UnsignedWord
An unsigned word type.
-
class
pynusmv.node.
SignedWord
(length)[source]¶ Bases:
pynusmv.node.Type
A signed word type.
-
length
¶
-
-
class
pynusmv.node.
Range
(start, stop)[source]¶ Bases:
pynusmv.node.Type
A range type.
-
start
¶
-
stop
¶
-
-
class
pynusmv.node.
ArrayType
(start, stop, elementtype)[source]¶ Bases:
pynusmv.node.Type
An array type.
-
start
¶
-
stop
¶
-
elementtype
¶
-
-
class
pynusmv.node.
Scalar
(values)[source]¶ Bases:
pynusmv.node.Type
The enumeration type.
-
values
¶ The values of this enumration.
-
-
class
pynusmv.node.
Modtype
(name, arguments)[source]¶ Bases:
pynusmv.node.Type
A module instantiation type.
-
name
¶
-
arguments
¶
-
-
class
pynusmv.node.
Process
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Type
The process type.
Warning
This type is deprecated.
-
class
pynusmv.node.
Integer
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Type
The integer number type.
Warning
This node type is not supported by NuSMV.
-
class
pynusmv.node.
Real
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Type
The real number type.
Warning
This node type is not supported by NuSMV.
-
class
pynusmv.node.
Wordarray
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Type
The word array type.
Warning
This type is not documented in NuSMV documentation.
-
class
pynusmv.node.
Expression
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
A generic expression node.
-
static
from_string
(expression)[source]¶ Parse the string representation of the given expression and return the corresponding node.
Parameters: expression – the string to parse Return type: Expression
subclass
-
static
-
class
pynusmv.node.
Leaf
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Failure
(message, kind)[source]¶ Bases:
pynusmv.node.Leaf
A FAILURE node.
-
message
¶
-
kind
¶
-
-
class
pynusmv.node.
Falseexp
[source]¶ Bases:
pynusmv.node.Leaf
The FALSE expression.
-
class
pynusmv.node.
Trueexp
[source]¶ Bases:
pynusmv.node.Leaf
The TRUE expression.
-
class
pynusmv.node.
Self
[source]¶ Bases:
pynusmv.node.Leaf
The self expression.
-
class
pynusmv.node.
Atom
(name)[source]¶ Bases:
pynusmv.node.Leaf
An ATOM node.
-
name
¶
-
-
class
pynusmv.node.
Number
(value)[source]¶ Bases:
pynusmv.node.Leaf
A node containing an integer.
-
value
¶
-
-
class
pynusmv.node.
NumberUnsignedWord
(value)[source]¶ Bases:
pynusmv.node.Leaf
A node containing an unsigned word value.
-
value
¶
-
-
class
pynusmv.node.
NumberSignedWord
(value)[source]¶ Bases:
pynusmv.node.Leaf
A node containing a signed word value.
-
value
¶
-
-
class
pynusmv.node.
NumberFrac
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Leaf
A rational number.
Warning
This node type is not supported by NuSMV.
-
class
pynusmv.node.
NumberReal
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Leaf
A real number.
Warning
This node type is not supported by NuSMV.
-
class
pynusmv.node.
NumberExp
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Leaf
An exponential-formed number.
Warning
This node type is not supported by NuSMV.
-
class
pynusmv.node.
Context
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
A CONTEXT node.
-
context
¶
-
expression
¶
-
-
class
pynusmv.node.
Array
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
An ARRAY node.
-
array
¶
-
index
¶
-
-
class
pynusmv.node.
Twodots
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
A range of integers.
-
start
¶
-
stop
¶
-
-
class
pynusmv.node.
Case
(values)[source]¶ Bases:
pynusmv.node.Expression
A set of cases.
-
values
¶ The mapping values of this Case expression.
Warning
The returned mapping should not be modified. Modifying the returned mapping will not change the actual NuSMV values of this node.
-
-
class
pynusmv.node.
Ifthenelse
(condition, true, false)[source]¶ Bases:
pynusmv.node.Expression
The cond ? truebranch : falsebranch expression.
-
condition
¶
-
true
¶
-
false
¶
-
-
class
pynusmv.node.
Implies
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Iff
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Or
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Xor
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Xnor
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
And
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Not
(expression)[source]¶ Bases:
pynusmv.node.Expression
A NOT expression.
-
expression
¶
-
-
class
pynusmv.node.
Equal
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Notequal
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Lt
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Gt
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Le
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Ge
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Union
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Setin
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Mod
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Plus
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Minus
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Times
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Divide
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Uminus
(expression)[source]¶ Bases:
pynusmv.node.Expression
A unitary minus expression.
-
expression
¶
-
-
class
pynusmv.node.
Next
(expression)[source]¶ Bases:
pynusmv.node.Expression
A NEXT expression.
-
expression
¶
-
-
class
pynusmv.node.
Dot
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Lshift
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Rshift
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Lrotate
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Rrotate
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
BitSelection
(word, start, stop)[source]¶ Bases:
pynusmv.node.Expression
A Bit selection node.
-
word
¶
-
start
¶
-
stop
¶
-
-
class
pynusmv.node.
Concatenation
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
CastBool
(expression)[source]¶ Bases:
pynusmv.node.Expression
A boolean casting node.
-
expression
¶
-
-
class
pynusmv.node.
CastWord1
(expression)[source]¶ Bases:
pynusmv.node.Expression
A word-1 casting node.
-
expression
¶
-
-
class
pynusmv.node.
CastSigned
(expression)[source]¶ Bases:
pynusmv.node.Expression
A signed number casting node.
-
expression
¶
-
-
class
pynusmv.node.
CastUnsigned
(expression)[source]¶ Bases:
pynusmv.node.Expression
An unsigned number casting node.
-
expression
¶
-
-
class
pynusmv.node.
Extend
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Waread
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Wawrite
(first, second, third)[source]¶ Bases:
pynusmv.node.Expression
A WAWRITE node.
-
class
pynusmv.node.
Uwconst
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Swconst
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Wresize
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Wsizeof
(expression)[source]¶ Bases:
pynusmv.node.Expression
A size-of-word node.
-
expression
¶
-
-
class
pynusmv.node.
CastToint
(expression)[source]¶ Bases:
pynusmv.node.Expression
An integer casting node.
-
expression
¶
-
-
class
pynusmv.node.
Count
(values)[source]¶ Bases:
pynusmv.node.Expression
A set expression.
-
values
¶ The values of this count.
-
-
class
pynusmv.node.
CustomExpression
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
A generic custom expression.
-
class
pynusmv.node.
Set
(values)[source]¶ Bases:
pynusmv.node.CustomExpression
A set expression.
-
values
¶ The values of this set.
-
-
class
pynusmv.node.
Identifier
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.CustomExpression
A custom identifier.
-
class
pynusmv.node.
Property
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Expression
-
class
pynusmv.node.
Eu
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Au
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Ew
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Aw
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Ebu
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Abu
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Minu
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Maxu
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Ex
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Ax
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Ef
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Af
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Eg
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Ag
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Since
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Until
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Triggered
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Releases
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Ebf
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Ebg
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Abf
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Abg
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
OpNext
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
OpGlobal
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
OpFuture
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
OpPrec
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
OpNotprecnot
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
OpHistorical
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
OpOnce
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Property
-
class
pynusmv.node.
Cons
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Pred
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Attime
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
PredsList
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Mirror
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
SyntaxError_
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Simpwff
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Nextwff
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Ltlwff
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Ctlwff
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Compwff
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Compid
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Bdd
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Semi
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Eqdef
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Smallinit
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Bit
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Nfunction
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Goto
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Constraint
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Lambda
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Comma
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Colon
(left, right, type_=None)[source]¶ Bases:
pynusmv.node.Node
-
class
pynusmv.node.
Declaration
(type_, section, name=None)[source]¶ Bases:
pynusmv.node.Atom
A Declaration behaves like an atom, except that it knows which type it belongs to. Furthermore, it does not know its name for sure, and cannot be printed without giving it a name.
-
name
¶ The name of the declared identifier.
-
-
class
pynusmv.node.
DVar
(type_, name=None)[source]¶ Bases:
pynusmv.node.Declaration
A declared VAR.
-
class
pynusmv.node.
DIVar
(type_, name=None)[source]¶ Bases:
pynusmv.node.Declaration
A declared IVAR.
-
class
pynusmv.node.
DFVar
(type_, name=None)[source]¶ Bases:
pynusmv.node.Declaration
A declared FROZENVAR.
-
class
pynusmv.node.
DDef
(type_, name=None)[source]¶ Bases:
pynusmv.node.Declaration
A declared DEFINE.
-
class
pynusmv.node.
FlatHierarchy
(ptr, freeit=False)[source]¶ Bases:
pynusmv.utils.PointerWrapper
Python class for flat hiearchy. The flat hierarchy is a NuSMV model where all the modules instances are reduced to their variables.
A FlatHierarchy is used to store information obtained after flattening module hierarchy. It stores:
- the list of TRANS, INIT, INVAR, ASSIGN, SPEC, COMPUTE, LTLSPEC, PSLSPEC, INVARSPEC, JUSTICE, COMPASSION,
- a full list of variables declared in the hierarchy,
- a hash table associating variables to their assignments and constraints.
Note
There are a few assumptions about the content stored in this class:
- All expressions are stored in the same order as in the input file (in module body or module instantiation order).
- Assigns are stored as a list of pairs (process instance name, assignments in it).
- Variable list contains only vars declared in this hierarchy.
- The association var->assignments should be for assignments of this hierarchy only.
- The association var->constraints (init, trans, invar) should be for constraints of this hierarchy only.
-
symbTable
¶ The symbolic table of the hierarchy.
-
variables
¶ The set of variables declared in this hierarchy.
Warning
The returned variables must not be altered.
-
init
¶ The INIT section of the flat hierarchy.
-
invar
¶ The INVAR section of the flat hierarchy.
-
trans
¶ The TRANS section of the flat hierarchy.
-
justice
¶ The JUSTICE section of the flat hierarchy.
-
compassion
¶ The COMPASSION section of the flat hierarchy.
fsm
Module¶
The pynusmv.fsm
module provides some functionalities about FSMs
represented and stored by NuSMV:
BddFsm
represents the model encoded into BDDs. This gives access to elements of the FSM like BDD encoding, initial states, reachable states, transition relation, pre and post operations, etc.BddTrans
represents a transition relation encoded with BDDs. It provides access to pre and post operations.BddEnc
represents the BDD encoding, with some functionalities like getting the state mask or the input variables mask.SymbTable
represents the symbols table of the model.
-
class
pynusmv.fsm.
BddFsm
(ptr, freeit=False)[source]¶ 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.
-
bddEnc
¶ The BDD encoding of this FSM.
-
init
¶ The BDD of initial states of this FSM.
-
state_constraints
¶ The BDD of states satisfying the invariants of the FSM.
-
inputs_constraints
¶ The BDD of inputs satisfying the invariants of the FSM.
-
fairness_constraints
¶ The list of fairness constraints, as BDDs.
-
reachable_states
¶ The set of reachable states of this FSM, represented as a BDD.
-
deadlock_states
¶ The set of reachable states of the system with no successor.
-
fair_states
¶ The set of fair states of this FSM, represented as a BDD.
-
pre
(states, inputs=None)[source]¶ 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:
-
weak_pre
(states)[source]¶ 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-imageReturn type: BDD
-
post
(states, inputs=None)[source]¶ 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:
-
pick_one_state
(bdd)[source]¶ 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
-
pick_one_state_random
(bdd)[source]¶ Return a BDD representing a state of bdd, picked at random.
Return type: State
Raise: a NuSMVBddPickingError
if bdd is false or an error occurs while picking one state
-
pick_one_inputs
(bdd)[source]¶ 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
-
pick_one_inputs_random
(bdd)[source]¶ Return a BDD representing an inputs of bdd, picked at random.
Return type: Inputs
Raise: a NuSMVBddPickingError
if bdd is false or an error occurs while picking one inputs
-
pick_one_state_inputs
(bdd)[source]¶ 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
-
pick_one_state_inputs_random
(bdd)[source]¶ Return a BDD representing a state/inputs pair of bdd, picked at random.
Return type: StateInputs
Raise: a NuSMVBddPickingError
if bdd is false or an error occurs while picking one pair
-
get_inputs_between_states
(current, next_)[source]¶ Return the BDD representing the possible inputs between current and next_.
Parameters: Return type:
-
count_states
(bdd)[source]¶ Return the number of states of the given BDD.
Parameters: bdd ( BDD
) – the concerned BDD
-
count_inputs
(bdd)[source]¶ Return the number of inputs of the given BDD
Parameters: bdd ( BDD
) – the concerned BDD
-
count_states_inputs
(bdd)[source]¶ Return the number of state/inputs pairs of the given BDD
Parameters: bdd ( BDD
) – the concerned BDD
-
pick_all_states
(bdd)[source]¶ Return a tuple of all states belonging to bdd.
Parameters: bdd ( BDD
) – the concerned BDDReturn type: tuple( State
)Raise: a NuSMVBddPickingError
if something is wrong
-
pick_all_inputs
(bdd)[source]¶ Return a tuple of all inputs belonging to bdd.
Parameters: bdd ( BDD
) – the concerned BDDReturn type: tuple( Inputs
)Raise: a NuSMVBddPickingError
if something is wrong
-
pick_all_states_inputs
(bdd)[source]¶ Return a tuple of all states/inputs pairs belonging to bdd.
Parameters: bdd ( BDD
) – the concerned BDDReturn type: tuple( StateInputs
)Raise: a NuSMVBddPickingError
if something is wrong
-
static
from_filename
(filepath)[source]¶ Return the FSM corresponding to the model in filepath.
Parameters: filepath – the path to the SMV model
-
-
class
pynusmv.fsm.
BddTrans
(ptr, enc=None, manager=None, freeit=True)[source]¶ 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.
-
pre
(states, inputs=None)[source]¶ Compute the pre-image of states, through inputs if not None.
Parameters: Return type:
-
post
(states, inputs=None)[source]¶ Compute the post-image of states, through inputs if not None.
Parameters: Return type:
-
classmethod
from_trans
(symb_table, trans, context=None)[source]¶ Return a new BddTrans from the given trans.
Parameters: - symb_table (
SymbTable
) – the symbols table used to flatten the trans - trans – the parsed string of the trans, not flattened
- context – an additional parsed context, in which trans will be flattened, if not None
Return type: Raise: a
NuSMVFlatteningError
if trans cannot be flattened under context- symb_table (
-
classmethod
from_string
(symb_table, strtrans, strcontext=None)[source]¶ Return a new BddTrans from the given strtrans, in given strcontex.
Parameters: - symb_table (
SymbTable
) – the symbols table used to flatten the trans - strtrans (str) – the string representing the trans
- strcontext – an additional string representing a context, in which trans will be flattened, if not None
Return type: Raise: a
NuSMVTypeCheckingError
if strtrans is wrongly typed under context- symb_table (
-
-
class
pynusmv.fsm.
BddEnc
(pointer, freeit=False)[source]¶ 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.
-
cube_for_inputs_vars
(variables)[source]¶ Return the cube for the given input variables.
Parameters: variables – a list of input variable names Return type: BDD
-
cube_for_state_vars
(variables)[source]¶ Return the cube for the given state variables.
Parameters: variables – a list of state variable names Return type: BDD
-
inputsVars
¶ Return the set of inputs variables names.
Return type: frozenset(str)
-
stateVars
¶ Return the set of state variables names.
Return type: frozenset(str)
-
definedVars
¶ Return the set of defined variables names.
Return type: frozenset(str)
-
get_variables_ordering
(var_type='scalar')[source]¶ Return the order of variables.
Parameters: var_type – the type of variables needed; “scalar” for only scalar variables (one variable per model variable), “bits” for bits for each scalar variables (default: “scalar”) Return type: tuple(str)
-
force_variables_ordering
(order)[source]¶ Reorder variables based on the given order.
Parameters: order – a list of variables names (scalar and/or bits) of the system; variables that are not part of the system are ignored (a warning is printed), variables of the system that are not in order are put at the end of the new order. - ..note:: For more information on variables orders, see NuSMV
- documentation.
-
-
class
pynusmv.fsm.
SymbTable
(pointer, freeit=False)[source]¶ Bases:
pynusmv.utils.PointerWrapper
Python class for symbols table.
-
ins_policies
= {'SYMB_LAYER_POS_TOP': 2, 'SYMB_LAYER_POS_FORCE_TOP': 1, 'SYMB_LAYER_POS_DEFAULT': 0, 'SYMB_LAYER_POS_FORCE_BOTTOM': 4, 'SYMB_LAYER_POS_BOTTOM': 3}¶
-
SYMBOL_STATE_VAR
= 3¶
-
SYMBOL_FROZEN_VAR
= 2¶
-
SYMBOL_INPUT_VAR
= 4¶
-
layer_names
¶ The names of the layers of this symbol table.
-
create_layer
(layer_name, ins_policy=0)[source]¶ Create a new layer in this symbol table.
Parameters: - layer_name (
str
) – the name of the created layer - ins_policy – the insertion policy for inserting the new layer
- layer_name (
-
get_variable_type
(variable)[source]¶ Return the type of the given variable.
Parameters: variable ( Node
) – the name of the variableReturn type: a NuSMV SymbType_ptr Warning
The returned pointer must not be altered or freed.
-
can_declare_var
(layer, variable)[source]¶ Return whether the given variable name can be declared in layer.
Parameters: - layer (
str
) – the name of the layer - variable (
Node
) – the name of the variable
Return type: bool
- layer (
-
declare_input_var
(layer, ivar, type_)[source]¶ Declare a new input variable in this symbol table.
Parameters: Raise: a
NuSMVSymbTableError
if the variable is already defined in the given layerWarning
type_ must be already resolved, that is, the body of type_ must be leaf values.
-
declare_state_var
(layer, var, type_)[source]¶ Declare a new state variable in this symbol table.
Parameters: Raise: a
NuSMVSymbTableError
if the variable is already defined in the given layerWarning
type_ must be already resolved, that is, the body of type_ must be leaf values.
-
declare_frozen_var
(layer, fvar, type_)[source]¶ Declare a new frozen variable in this symbol table.
Parameters: Raise: a
NuSMVSymbTableError
if the variable is already defined in the given layerWarning
type_ must be already resolved, that is, the body of type_ must be leaf values.
-
declare_var
(layer, name, type_, kind)[source]¶ Declare a new variable in this symbol table.
Parameters: Raise: a
NuSMVSymbTableError
if the variable is already defined in the given layerWarning
type_ must be already resolved, that is, the body of type_ must be leaf values.
-
is_input_var
(ivar)[source]¶ Return whether the given var name is a declared input variable.
Parameters: ivar ( Node
) – the name of the input variableRaise: a NuSMVSymbTableError
if the variable is not defined in this symbol table
-
is_state_var
(var)[source]¶ Return whether the given var name is a declared state variable.
Parameters: var ( Node
) – the name of the state variableRaise: a NuSMVSymbTableError
if the variable is not defined in this symbol table
-
is_frozen_var
(fvar)[source]¶ Return whether the given var name is a declared frozen variable.
Parameters: fvar ( Node
) – the name of the frozen variableRaise: a NuSMVSymbTableError
if the variable is not defined in this symbol table
-
prop
Module¶
The pynusmv.prop
module contains classes and functions dealing with
properties and specifications of models.
-
pynusmv.prop.
propTypes
= {'LTL': 103, 'CTL': 102, 'NoType': 101, 'Comparison': 107, 'Compute': 106, 'Invariant': 105, 'PSL': 104}¶ The possible types of properties. This gives access to NuSMV internal types without dealing with pynusmv.nusmv modules.
-
class
pynusmv.prop.
Prop
(pointer, freeit=False)[source]¶ Bases:
pynusmv.utils.PointerWrapper
Python class for properties.
Properties are NuSMV data structures containing specifications but also pointers to models (FSM) and other things.
-
name
¶ The name of this property, as a string.
-
-
class
pynusmv.prop.
PropDb
(pointer, freeit=False)[source]¶ 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.
-
class
pynusmv.prop.
Spec
(ptr, freeit=False)[source]¶ 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.
-
type
¶ The type of this specification.
-
-
pynusmv.prop.
not_
(spec)[source]¶ Return a new specification corresponding to NOT spec.
Return type: Spec
-
pynusmv.prop.
and_
(left, right)[source]¶ Return a new specification corresponding to left AND right.
Return type: Spec
-
pynusmv.prop.
or_
(left, right)[source]¶ Return a new specification corresponding to left OR right.
Return type: Spec
-
pynusmv.prop.
imply
(left, right)[source]¶ Return a new specification corresponding to left IMPLIES right.
Return type: Spec
-
pynusmv.prop.
iff
(left, right)[source]¶ Return a new specification corresponding to left IFF right.
Return type: Spec
-
pynusmv.prop.
ex
(spec)[source]¶ Return a new specification corresponding to EX spec.
Return type: Spec
-
pynusmv.prop.
eg
(spec)[source]¶ Return a new specification corresponding to EG spec.
Return type: Spec
-
pynusmv.prop.
ef
(spec)[source]¶ Return a new specification corresponding to EF spec.
Return type: Spec
-
pynusmv.prop.
eu
(left, right)[source]¶ Return a new specification corresponding to E[left U right].
Return type: Spec
-
pynusmv.prop.
ew
(left, right)[source]¶ Return a new specification corresponding to E[left W right].
Return type: Spec
-
pynusmv.prop.
ax
(spec)[source]¶ Return a new specification corresponding to AX spec.
Return type: Spec
-
pynusmv.prop.
ag
(spec)[source]¶ Return a new specification corresponding to AG spec.
Return type: Spec
-
pynusmv.prop.
af
(spec)[source]¶ Return a new specification corresponding to AF spec.
Return type: Spec
-
pynusmv.prop.
au
(left, right)[source]¶ Return a new specification corresponding to A[left U right].
Return type: Spec
-
pynusmv.prop.
aw
(left, right)[source]¶ Return a new specification corresponding to A[left W right].
Return type: Spec
-
pynusmv.prop.
atom
(strrep, type_checking=True)[source]¶ Return a new specification corresponding to the given atom. strrep is parsed and type checked on the current model. A model needs to be read and with variables encoded to be able to type check the atomic proposition. If type_checking is False, type checking is not performed and a model is not needed anymore.
Parameters: - strrep – the string representation of the atom
- type_checking (bool) – whether or not type check the parsed string (default: True)
Return type:
dd
Module¶
The pynusmv.dd
module provides some BDD-related structures:
BDD
represents a BDD.BDDList
represents a list of BDDs.State
represents a particular state of the model.Inputs
represents input variables values, i.e. a particular action of the model.StateInputs
represents a particular state-inputs pair of the model.Cube
represents a particular cube of variables the model.DDManager
represents a NuSMV DD manager.
It also provides global methods to work on BDD variables reordering: enable_dynamic_reordering()
, disable_dynamic_reordering()
,
dynamic_reordering_enabled()
, reorder()
.
-
pynusmv.dd.
enable_dynamic_reordering
(DDmanager=None, method='sift')[source]¶ Enable dynamic reordering of BDD variables under control of DDmanager with the given method.
Parameters: - DDmanager (
DDManager
) – the concerned DD manager; if None, the global DD manager is used instead. - method (
str
) – the method to use for reordering: sift (default method), random, random_pivot, sift_converge, symmetry_sift, symmetry_sift_converge, window{2, 3, 4}, window{2, 3, 4}_converge, group_sift, group_sift_converge, annealing, genetic, exact, linear, linear_converge, same (the previously chosen method)
Raise: a
MissingManagerError
if the manager is missingNote
For more information on reordering methods, see NuSMV manual.
- DDmanager (
-
pynusmv.dd.
disable_dynamic_reordering
(DDmanager=None)[source]¶ Disable dynamic reordering of BDD variables under control of DDmanager.
Parameters: DDmanager ( DDManager
) – the concerned DD manager; if None, the global DD manager is used instead.Raise: a MissingManagerError
if the manager is missing
-
pynusmv.dd.
dynamic_reordering_enabled
(DDmanager=None)[source]¶ Return the dynamic reordering method used if reordering is enabled for BDD under control of DDmanager, None otherwise.
Parameters: DDmanager ( DDManager
) – the concerned DD manager; if None, the global DD manager is used instead.Return type: None, or a the name of the method used Raise: a MissingManagerError
if the manager is missing
-
pynusmv.dd.
reorder
(DDmanager=None, method='sift')[source]¶ Force a reordering of BDD variables under control of DDmanager.
Parameters: - DDmanager (
DDManager
) – the concerned DD manager; if None, the global DD manager is used instead. - method (
str
) – the method to use for reordering: sift (default method), random, random_pivot, sift_converge, symmetry_sift, symmetry_sift_converge, window{2, 3, 4}, window{2, 3, 4}_converge, group_sift, group_sift_converge, annealing, genetic, exact, linear, linear_converge, same (the previously chosen method)
Raise: a
MissingManagerError
if the manager is missingNote
For more information on reordering methods, see NuSMV manual.
- DDmanager (
-
class
pynusmv.dd.
BDD
(ptr, dd_manager=None, freeit=True)[source]¶ 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:
a + b
anda | b
compute the disjunction ofa
andb
a * b
anda & b
compute the conjunction ofa
andb
~a
and-a
compute the negation ofa
a - b
computesa & ~b
a ^ b
computes the exclusive-OR (XOR) ofa
andb
a == b
,a <= b
,a < b
,a > b
anda >= b
comparea
andb
Any BDD operation raises a
MissingManagerError
whenever the manager of the BDD is None and a manager is needed to perform the operation.-
size
¶ The number of BDD nodes of this BDD.
-
equal
(other)[source]¶ Determine whether this BDD is equal to other or not.
Parameters: other ( BDD
) – the BDD to compare
-
entailed
(other)[source]¶ Determine whether this BDD is included in other or not.
Parameters: other ( BDD
) – the BDD to compare
-
intersected
(other)[source]¶ Determine whether the intersection between this BDD and other is not empty.
Parameters: other ( BDD
) – the BDD to compare
-
leq
(other)[source]¶ Determine whether this BDD is less than or equal to other.
Parameters: other ( BDD
) – the BDD to compare
-
and_
(other)[source]¶ Compute the conjunction of this BDD and other.
Parameters: other ( BDD
) – the other BDD
-
or_
(other)[source]¶ Compute the conjunction of this BDD and other.
Parameters: other ( BDD
) – the other BDD
-
xor
(other)[source]¶ Compute the exclusive-OR of this BDD and other.
Parameters: other ( BDD
) – the other BDD
-
iff
(other)[source]¶ Compute the IFF operation on this BDD and other.
Parameters: other ( BDD
) – the other BDD
-
imply
(other)[source]¶ Compute the IMPLY operation on this BDD and other.
Parameters: other ( BDD
) – the other BDD
-
forsome
(cube)[source]¶ Existentially abstract all the variables in cube from this BDD.
Parameters: cube ( BDD
) – the cube
-
forall
(cube)[source]¶ Universally abstract all the variables in cube from this BDD.
Parameters: cube ( BDD
) – the cube
-
minimize
(c)[source]¶ Restrict this BDD with c, as described in Coudert et al. ICCAD90.
Parameters: c ( BDD
) – the BDD used to restrict this BDDNote
Always returns a BDD not larger than the this BDD.
-
class
pynusmv.dd.
BDDList
(ptr, ddmanager=None, freeit=True)[source]¶ 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.
-
to_tuple
()[source]¶ Return a tuple containing all BDDs of self. The returned BDDs are copies of the ones of self.
-
static
from_tuple
(bddtuple)[source]¶ 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 createdBDDList
is None.
-
-
class
pynusmv.dd.
State
(ptr, fsm, freeit=True)[source]¶ Bases:
pynusmv.dd.BDD
Python class for State structure.
A State is a
BDD
representing a single state of the model.
-
class
pynusmv.dd.
Inputs
(ptr, fsm, freeit=True)[source]¶ 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.
-
class
pynusmv.dd.
StateInputs
(ptr, fsm, freeit=True)[source]¶ Bases:
pynusmv.dd.BDD
Python class for State and Inputs structure.
A StateInputs is a
BDD
representing a single state/inputs pair of the model.
-
class
pynusmv.dd.
Cube
(ptr, dd_manager=None, freeit=True)[source]¶ Bases:
pynusmv.dd.BDD
Python class for Cube structure.
A Cube is a
BDD
representing a BDD cube of the model.-
diff
(other)[source]¶ Compute the difference between this cube and other
Parameters: other ( BDD
) – the other cube
-
-
class
pynusmv.dd.
DDManager
(pointer, freeit=False)[source]¶ Bases:
pynusmv.utils.PointerWrapper
Python class for NuSMV BDD managers.
-
size
¶ The number of variables handled by this manager.
-
reorderings
¶ Returns the number of times reordering has occurred in this manager.
-
parser
Module¶
The pynusmv.parser
module provides functions to parse strings
and return corresponding ASTs. This module includes three types of
functionalities:
parse_simple_expression()
,parse_next_expression()
,parse_identifier()
andparse_ctl_spec()
are direct access to NuSMV parser, returning wrappers to NuSMV internal data structures representing the language AST.identifier
,simple_expression
,constant
,next_expression
,type_identifier
,var_section
,ivar_section
,frozenvar_section
,define_section
,constants_section
,assign_constraint
,init_constraint
,trans_constraint
,invar_constraint
,fairness_constraint
,justice_constraint
,compassion_constraint
,module
andmodel
are pyparsing parsers parsing the corresponding elements of a NuSMV model (see NuSMV documentation for more information on these elements of the language).parseAllString()
is a helper function to directly return ASTs for strings parsed with pyparsing parsers.
-
pynusmv.parser.
parse_simple_expression
(expression)[source]¶ Parse a simple expression.
Parameters: expression (string) – the expression to parse Raise: a NuSMVParsingError
if a parsing error occursWarning
Returned value is a SWIG wrapper for the NuSMV node_ptr. It is the responsibility of the caller to manage it.
-
pynusmv.parser.
parse_next_expression
(expression)[source]¶ Parse a “next” expression.
Parameters: expression (string) – the expression to parse Raise: a NuSMVParsingError
if a parsing error occursWarning
Returned value is a SWIG wrapper for the NuSMV node_ptr. It is the responsibility of the caller to manage it.
-
pynusmv.parser.
parse_identifier
(expression)[source]¶ Parse an identifier
Parameters: expression (string) – the identifier to parse Raise: a NuSMVParsingError
if a parsing error occursWarning
Returned value is a SWIG wrapper for the NuSMV node_ptr. It is the responsibility of the caller to manage it.
-
pynusmv.parser.
parse_ctl_spec
(spec)[source]¶ Parse a CTL specification
Parameters: spec (string) – the specification to parse Raise: a NuSMVParsingError
if a parsing error occursWarning
Returned value is a SWIG wrapper for the NuSMV node_ptr. It is the responsibility of the caller to manage it.
mc
Module¶
The pynusmv.mc
module provides some functions of NuSMV dealing with
model checking, like CTL model checking.
-
pynusmv.mc.
check_ctl_spec
(fsm, spec, context=None)[source]¶ Return whether the given fsm satisfies or not the given spec in context, if specified. That is, return whether all initial states of fsm satisfies spec in context or not.
Parameters: Return type:
-
pynusmv.mc.
eval_simple_expression
(fsm, sexp)[source]¶ Return the set of states of fsm satisfying sexp, as a BDD. sexp is first parsed, then evaluated on fsm.
Parameters: - fsm (
BddFsm
) – the concerned FSM - sexp – a simple expression, as a string
Return type: - fsm (
-
pynusmv.mc.
eval_ctl_spec
(fsm, spec, context=None)[source]¶ Return the set of states of fsm satisfying spec in context, as a BDD.
Parameters: Return type:
-
pynusmv.mc.
ef
(fsm, states)[source]¶ Return the set of states of fsm satisfying EF states, as a BDD.
Parameters: Return type:
-
pynusmv.mc.
eg
(fsm, states)[source]¶ Return the set of states of fsm satisfying EG states, as a BDD.
Parameters: Return type:
-
pynusmv.mc.
ex
(fsm, states)[source]¶ Return the set of states of fsm satisfying EX states, as a BDD.
Parameters: Return type:
-
pynusmv.mc.
eu
(fsm, s1, s2)[source]¶ Return the set of states of fsm satisfying E[s1 U s2], as a BDD.
Parameters: Return type:
-
pynusmv.mc.
au
(fsm, s1, s2)[source]¶ Return the set of states of fsm satisfying A[s1 U s2], as a BDD.
Parameters: Return type:
-
pynusmv.mc.
explain
(fsm, state, spec, context=None)[source]¶ Explain why state of fsm satisfies spec in context.
Parameters: Return a tuple t composed of states (
State
) and inputs (Inputs
), such that t[0] is state and t represents a path in fsm explaining why state satisfies spec in context. The returned path is looping if the last state of path is equal to a previous state along the path.
-
pynusmv.mc.
explainEX
(fsm, state, a)[source]¶ 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.
-
pynusmv.mc.
explainEU
(fsm, state, a, b)[source]¶ 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.
-
pynusmv.mc.
explainEG
(fsm, state, a)[source]¶ 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.
exception
Module¶
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.
-
exception
pynusmv.exception.
PyNuSMVError
[source]¶ Bases:
Exception
A generic PyNuSMV Error, superclass of all PyNuSMV Errors.
-
exception
pynusmv.exception.
MissingManagerError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception for missing BDD manager.
-
exception
pynusmv.exception.
NuSMVLexerError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception for NuSMV lexer error.
-
exception
pynusmv.exception.
NuSMVNoReadModelError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when no SMV model has been read yet.
-
exception
pynusmv.exception.
NuSMVModelAlreadyReadError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when a model is already read.
-
exception
pynusmv.exception.
NuSMVCannotFlattenError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when no SMV model has been read yet.
-
exception
pynusmv.exception.
NuSMVModelAlreadyFlattenedError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when the model is already flattened.
-
exception
pynusmv.exception.
NuSMVNeedFlatHierarchyError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when the model must be flattened.
-
exception
pynusmv.exception.
NuSMVModelAlreadyEncodedError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when the model is already encoded.
-
exception
pynusmv.exception.
NuSMVFlatModelAlreadyBuiltError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when the flat model is already built.
-
exception
pynusmv.exception.
NuSMVNeedFlatModelError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when the model must be flattened.
-
exception
pynusmv.exception.
NuSMVModelAlreadyBuiltError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when the BDD model is already built.
-
exception
pynusmv.exception.
NuSMVNeedVariablesEncodedError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when the variables of the model must be encoded.
-
exception
pynusmv.exception.
NuSMVInitError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
NuSMV initialisation-related exception.
-
exception
pynusmv.exception.
NuSMVParserError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when an error occured while parsing a string with NuSMV.
-
exception
pynusmv.exception.
NuSMVTypeCheckingError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when an expression is wrongly typed.
-
exception
pynusmv.exception.
NuSMVFlatteningError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when an error occured while flattening some expression.
-
exception
pynusmv.exception.
NuSMVBddPickingError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when an error occured while picking a state/inputs from a BDD.
-
exception
pynusmv.exception.
NuSMVParsingError
(errors)[source]¶ Bases:
pynusmv.exception.PyNuSMVError
A
NuSMVParsingError
is a NuSMV parsing exception. Contains several errors accessible through theerrors
attribute.-
static
from_nusmv_errors_list
(errors)[source]¶ Create a new NuSMVParsingError from the given list of NuSMV errors.
Parameters: errors – the list of errors from NuSMV
-
errors
¶ The tuple of errors of this exception. These errors are tuples (line, token, message) representing the line, the token and the message of the error.
-
static
-
exception
pynusmv.exception.
NuSMVModuleError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when an error occured while creating a module.
-
exception
pynusmv.exception.
NuSMVSymbTableError
[source]¶ Bases:
pynusmv.exception.PyNuSMVError
Exception raised when an error occured while working with symbol tables.
utils
Module¶
The pynusmv.utils
module contains some secondary functions and classes
used by PyNuSMV internals.
-
class
pynusmv.utils.
PointerWrapper
(pointer, freeit=False)[source]¶ Bases:
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.