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:

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

pynusmv.init.is_nusmv_init()[source]

Return whether NuSMV is initialized.

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

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 flattened

Raise:

a NuSMVModelAlreadyEncodedError if the variables are already encoded

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
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 flattened
Raise: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 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
pynusmv.glob.flat_hierarchy()[source]

Return the global flat hierarchy.

Return type:FlatHierarchy
pynusmv.glob.prop_database()[source]

Return the global properties database.

Return type:PropDb
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 using Expression 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: the Module class represents a generic NuSMV module, and must be subclassed to define specific NuSMV modules. See the documentation of the Module 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.

to_node()[source]
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.Set(elements, *args, **kwargs)[source]

Bases: pynusmv.model.Expression

A set.

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.Boolean(comments=None)[source]

Bases: pynusmv.model.SimpleType

A boolean type.

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

static from_ptr(ptr, freeit=False)[source]
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.

in_context(context)[source]
array(index)[source]
twodots(stop)[source]
ifthenelse(true, false)[source]
implies(expression)[source]
iff(expression)[source]
or_(expression)[source]
xor(expression)[source]
xnor(expression)[source]
and_(expression)[source]
not_()[source]
equal(expression)[source]
notequal(expression)[source]
lt(expression)[source]
gt(expression)[source]
le(expression)[source]
ge(expression)[source]
union(expression)[source]
setin(expression)[source]
in_(expression)[source]
mod(expression)[source]
plus(expression)[source]
minus(expression)[source]
times(expression)[source]
divide(expression)[source]
uminus()[source]
next()[source]
dot(expression)[source]
lshift(expression)[source]
rshift(expression)[source]
lrotate(expression)[source]
rrotate(expression)[source]
bit_selection(start, stop)[source]
concatenation(expression)[source]
concat(expression)[source]
castbool()[source]
bool()[source]
castword1()[source]
word1()[source]
castsigned()[source]
signed()[source]
castunsigned()[source]
unsigned()[source]
extend(size)[source]
waread(expression)[source]
read(expression)[source]
wawrite(second, third)[source]
write(second, third)[source]
uwconst(expression)[source]
swconst(expression)[source]
wresize(size)[source]
resize(size)[source]
wsizeof()[source]
sizeof()[source]
casttoint()[source]
toint()[source]
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
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.

static from_string(identifier)[source]

Return the node representation of identifier.

:param str identifier: the string representation of an
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:

  1. All expressions are stored in the same order as in the input file (in module body or module instantiation order).
  2. Assigns are stored as a list of pairs (process instance name, assignments in it).
  3. Variable list contains only vars declared in this hierarchy.
  4. The association var->assignments should be for assignments of this hierarchy only.
  5. 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.

trans

The transition relation (BddTrans) of this FSM. Can also be replaced.

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:
  • states (BDD) – the states from which getting the pre-image
  • inputs (BDD) – the inputs through which getting the pre-image
Return type:

BDD

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-image
Return 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:
  • states (BDD) – the states from which getting the post-image
  • inputs (BDD) – the inputs through which getting the post-image
Return type:

BDD

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:
  • current (BDD) – the source states
  • next (BDD) – the destination states
Return type:

BDD

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 BDD
Return 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 BDD
Return 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 BDD
Return 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
static from_string(model)[source]

Return the FSM corresponding to the model defined by the given string.

Parameters:model – a String representing the SMV model
static from_modules(*modules)[source]

Return the FSM corresponding to the model defined by the given list of modules.

Parameters:modules (a list of Module subclasses) – the modules defining the NuSMV model. Must contain a main module.
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.

monolithic

This transition relation represented as a monolithic BDD.

Return type:BDD
pre(states, inputs=None)[source]

Compute the pre-image of states, through inputs if not None.

Parameters:
  • states (BDD) – the concerned states
  • inputs (BDD) – possible inputs
Return type:

BDD

post(states, inputs=None)[source]

Compute the post-image of states, through inputs if not None.

Parameters:
  • states (BDD) – the concerned states
  • inputs (BDD) – possible inputs
Return type:

BDD

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:

BddTrans

Raise:

a NuSMVFlatteningError if trans cannot be flattened under context

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:

BddTrans

Raise:

a NuSMVTypeCheckingError if strtrans is wrongly typed under context

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.

DDmanager

The DD manager of this encoding.

Return type:DDManager
symbTable

The symbols table of this encoding.

Return type:SymbTable
statesMask

The mask for all state variables, represented as a BDD.

Return type:BDD
inputsMask

The mask for all input variables, represented as a BDD.

Return type:BDD
statesInputsMask

The mask for all input and state variables, represented as a BDD.

Return type:BDD
statesCube

The cube for all state variables, represented as a BDD.

Return type:BDD
inputsCube

The cube for all input variables, represented as a BDD.

Return type:BDD
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
get_variable_type(variable)[source]

Return the type of the given variable.

Parameters:variable (Node) – the name of the variable
Return 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

declare_input_var(layer, ivar, type_)[source]

Declare a new input variable in this symbol table.

Parameters:
  • layer (str) – the name of the layer in which insert the variable
  • ivar (Node) – the name of the input variable
  • type (Node) – the type of the declared input variable
Raise:

a NuSMVSymbTableError if the variable is already defined in the given layer

Warning

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:
  • layer (str) – the name of the layer in which insert the variable
  • var (Node) – the name of the state variable
  • type (Node) – the type of the declared state variable
Raise:

a NuSMVSymbTableError if the variable is already defined in the given layer

Warning

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:
  • layer (str) – the name of the layer in which insert the variable
  • fvar (Node) – the name of the frozen variable
  • type (Node) – the type of the declared frozen variable
Raise:

a NuSMVSymbTableError if the variable is already defined in the given layer

Warning

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:
  • layer (str) – the name of the layer in which insert the variable
  • name (Node) – the name of the variable
  • type (Node) – the type of the declared variable
  • kind – the kind of the declared variable
Raise:

a NuSMVSymbTableError if the variable is already defined in the given layer

Warning

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 variable
Raise: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 variable
Raise: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 variable
Raise: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.

type

The type of this property. It is one element of propTypes.

name

The name of this property, as a string.

expr

The expression of this property.

Return type:Spec
exprcore

The core expression of this property

Return type:Spec
bddFsm

The BDD-encoded FSM of this property.

Return type:BddFsm
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.

master

The master property of this database.

Return type:Prop
get_prop_at_index(index)[source]

Return the property stored at index.

Return type:Prop
get_size()[source]

Return the number of properties stored in this database.

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.

car

The left child of this specification.

Return type:Spec
cdr

The right child of this specification.

Return type:Spec
pynusmv.prop.true()[source]

Return a new specification corresponding to TRUE.

Return type:Spec
pynusmv.prop.false()[source]

Return a new specification corresponding to FALSE.

Return type:Spec
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:

Spec

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 missing

Note

For more information on reordering methods, see NuSMV manual.

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 missing

Note

For more information on reordering methods, see NuSMV manual.

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 and a | b compute the disjunction of a and b
  • a * b and a & b compute the conjunction of a and b
  • ~a and -a compute the negation of a
  • a - b computes a & ~b
  • a ^ b computes the exclusive-OR (XOR) of a and b
  • a == b, a <= b, a < b, a > b and a >= b compare a and b

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
dup()[source]

Return a copy of this BDD.

is_true()[source]

Determine whether this BDD is true or not.

is_false()[source]

Determine whether this BDD is false or not.

isnot_true()[source]

Determine whether this BDD is not true.

isnot_false()[source]

Determine whether this BDD is not false.

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
not_()[source]

Compute the complement of this BDD.

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
diff(other)[source]
intersection(other)[source]
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 BDD

Note

Always returns a BDD not larger than the this BDD.

static true(manager_or_fsm=None)[source]

Return the TRUE BDD.

Parameters:manager_or_fsm (DDManager or BddFsm) – if not None, the manager of the returned BDD or the FSM; otherwise, the global FSM is used.
static false(manager_or_fsm=None)[source]

Return the FALSE BDD.

Parameters:manager_or_fsm (DDManager or BddFsm) – if not None, the manager of the returned BDD or the FSM; otherwise, the global FSM is used.
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 created BDDList 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.

get_str_values(layers=None)[source]

Return a dictionary of the (variable, value) pairs of this State.

Parameters:layers – if not None, the set of names of the layers from which picking the string values
Return type:a dictionary of pairs of strings.
static from_bdd(bdd, fsm)[source]

Return a new State of fsm from bdd.

Parameters:
  • bdd (BDD) – a BDD representing a single state
  • fsm (BddFsm) – the FSM from which the BDD comes from
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.

get_str_values(layers=None)[source]

Return a dictionary of the (variable, value) pairs of these Inputs.

Parameters:layers – if not None, the set of names of the layers from which picking the string values
Return type:a dictionary of pairs of strings.
static from_bdd(bdd, fsm)[source]

Return a new Inputs of fsm from bdd.

Parameters:
  • bdd (BDD) – a BDD representing a single inputs variables valuation
  • fsm (BddFsm) – the FSM from which the BDD comes from
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.

get_str_values()[source]

Return a dictionary of the (variable, value) pairs of this StateInputs.

Return type:a dictionary of pairs of strings.
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
intersection(other)[source]

Compute the intersection of this Cube and other.

Parameters:other (BDD) – the other Cube
union(other)[source]

Compute the union of this Cube and other.

Parameters:other (Cube) – 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() and parse_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 and model 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 occurs

Warning

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 occurs

Warning

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 occurs

Warning

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 occurs

Warning

Returned value is a SWIG wrapper for the NuSMV node_ptr. It is the responsibility of the caller to manage it.

pynusmv.parser.parseAllString(parser, string)[source]

Parse string completely with parser and set source of the result to string. parser is assumed to return a one-element list when parsing string.

Parameters:
  • parser – a pyparsing parser
  • string (str) – the string to parse

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:
  • fsm (BddFsm) – the concerned FSM
  • spec (Spec) – a specification about fsm
  • context (Spec) – the context in which evaluate spec
Return type:

bool

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:

BDD

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:
  • fsm (BddFsm) – the concerned FSM
  • spec (Spec) – a specification about fsm
  • context (Spec) – the context in which evaluate spec
Return type:

BDD

pynusmv.mc.ef(fsm, states)[source]

Return the set of states of fsm satisfying EF states, as a BDD.

Parameters:
  • fsm (BddFsm) – the concerned FSM
  • states (BDD) – a set of states of fsm
Return type:

BDD

pynusmv.mc.eg(fsm, states)[source]

Return the set of states of fsm satisfying EG states, as a BDD.

Parameters:
  • fsm (BddFsm) – the concerned FSM
  • states (BDD) – a set of states of fsm
Return type:

BDD

pynusmv.mc.ex(fsm, states)[source]

Return the set of states of fsm satisfying EX states, as a BDD.

Parameters:
  • fsm (BddFsm) – the concerned FSM
  • states (BDD) – a set of states of fsm
Return type:

BDD

pynusmv.mc.eu(fsm, s1, s2)[source]

Return the set of states of fsm satisfying E[s1 U s2], as a BDD.

Parameters:
  • fsm (BddFsm) – the concerned FSM
  • s1 (BDD) – a set of states of fsm
  • s2 (BDD) – a set of states of fsm
Return type:

BDD

pynusmv.mc.au(fsm, s1, s2)[source]

Return the set of states of fsm satisfying A[s1 U s2], as a BDD.

Parameters:
  • fsm (BddFsm) – the concerned FSM
  • s1 (BDD) – a set of states of fsm
  • s2 (BDD) – a set of states of fsm
Return type:

BDD

pynusmv.mc.explain(fsm, state, spec, context=None)[source]

Explain why state of fsm satisfies spec in context.

Parameters:
  • fsm (BddFsm) – the system
  • state (State) – a state of fsm
  • spec (Spec) – a specification about fsm
  • context (Spec) – the context in which evaluate spec

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:
  • fsm (BddFsm) – the system
  • state (State) – a state of fsm
  • a (BDD) – the set of states of fsm satisfying phi

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:
  • fsm (BddFsm) – the system
  • state (State) – a state of fsm
  • a (BDD) – the set of states of fsm satisfying phi
  • b (BDD) – the set of states of fsm satisfying psi

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:
  • fsm (BddFsm) – the system
  • state (State) – a state of fsm
  • a (BDD) – the set of states of fsm satisfying phi

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

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.

pynusmv.utils.fixpoint(funct, start)[source]

Return the fixpoint of funct, as a BDD, starting with start BDD.

Return type:BDD

Note

mu Z.f(Z) least fixpoint is implemented with fixpoint(funct, false). nu Z.f(Z) greatest fixpoint is implemented with fixpoint(funct, true).

pynusmv.utils.update(old, new)[source]

Update old with new. old is assumed to have the extend or update method, and new is assumed to be a good argument for the corresponding method.

Parameters:
  • old – the data to update.
  • new – the date to update with.