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 NuSMV 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.
  • dd provides BDD-related structures like generic BDD, lists of BDDs and BDD-represented states and input values.
  • exception groups all the PyNuSMV-related exceptions.
  • 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 simple CTL specifications.
  • parser gives access to NuSMV parser to parse simple expressions of the SMV language.
  • mc contains model checking features.
  • utils contains some side functionalities.

Warning

Before using any PyNuSMV functionality, make sure to call pynusmv.init.init_nusmv() function to initialize NuSMV; do not forget to also call pynusmv.init.deinit_nusmv() when you do not need PyNuSMV anymore to clean everything needed by NuSMV to run.

dd Module

The pynusmv.dd module provides some BDD-related structures:

  • BDD represents a BDD.
  • BDDList represents a list of BDDs.
  • Inputs represents input variables values, i.e. a particular action of the model.
  • State represents a particular state of the model.
  • DDManager represents a NuSMV DD manager.
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.

andd(self, other)[source]

Compute the conjunction of this BDD and other.

Parameters:other (BDD) – the other BDD
dup(self)[source]

Return a copy of this BDD.

entailed(self, other)[source]

Determine whether this BDD is included in other or not.

Parameters:other (BDD) – the BDD to compare
equal(self, other)[source]

Determine whether this BDD is equal to other or not.

Parameters:other (BDD) – the BDD to compare
false(manager)[source]

Return the FALSE BDD.

Parameters:manager (DDManager) – the manager of the returned BDD
forall(self, cube)[source]

Universally abstract all the variables in cube from this BDD.

Parameters:cube (BDD) – the cube
forsome(self, cube)[source]

Existentially abstract all the variables in cube from this BDD.

Parameters:cube (BDD) – the cube
iff(self, other)[source]

Compute the IFF operation on this BDD and other.

Parameters:other (BDD) – the other BDD
imply(self, other)[source]

Compute the IMPLY operation on this BDD and other.

Parameters:other (BDD) – the other BDD
intersected(self, other)[source]

Determine whether the intersection between this BDD and other is not empty.

Parameters:other (BDD) – the BDD to compare
is_false(self)[source]

Determine whether this BDD is false or not.

is_true(self)[source]

Determine whether this BDD is true or not.

isnot_false(self)[source]

Determine whether this BDD is not false.

isnot_true(self)[source]

Determine whether this BDD is not true.

leq(self, other)[source]

Determine whether this BDD is less than or equal to other.

Parameters:other (BDD) – the BDD to compare
nott(self)[source]

Compute the complement of this BDD.

orr(self, other)[source]

Compute the conjunction of this BDD and other.

Parameters:other (BDD) – the other BDD
true(manager)[source]

Return the TRUE BDD.

Parameters:manager (DDManager) – the manager of the returned BDD
xor(self, other)[source]

Compute the exclusive-OR of this BDD and other.

Parameters:other (BDD) – the other 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.

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.

to_tuple(self)[source]

Return a tuple containing all BDDs of self. The returned BDDs are copies of the ones of self.

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.

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

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

Return type:a dictionary of pairs of strings.
class pynusmv.dd.DDManager(pointer, freeit=False)[source]

Bases: pynusmv.utils.PointerWrapper

Python class for NuSMV BDD managers.

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.

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

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

Return type:a dictionary of pairs of strings.

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: builtins.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.NuSMVNoReadFileError[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.

class pynusmv.exception.Error

Bases: builtins.tuple

An Error is a single parsing error generated by NuSMV parser.

line

Alias for field number 0

message

Alias for field number 2

token

Alias for field number 1

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.

errors[source]

The tuple of errors of this exception.

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.
  • 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.
  • BddTrans represents a transition relation encoded with BDDs. It provides access to pre and post operations.
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[source]

The BDD encoding of this FSM.

count_inputs(self, bdd)[source]

Return the number of inputs of the given BDD

Parameters:bdd (BDD) – the concerned BDD
count_states(self, bdd)[source]

Return the number of states of the given BDD.

Parameters:bdd (BDD) – the concerned BDD
fairness_constraints[source]

The list of fairness constraints, as BDDs.

from_filename(filepath)[source]

Return the FSM corresponding to the model in filepath.

Parameters:filepath – the path to the SMV model
get_inputs_between_states(self, current, next)[source]

Return the BDD representing the possible inputs between current and next.

Parameters:
  • current (BDD) – the source states
  • current – the destination states
Return type:

BDD

init[source]

The BDD of initial states of this FSM.

inputs_constraints[source]

The BDD of inputs satisfying the invariants of the FSM.

pick_all_inputs(self, 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(self, 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_states_inputs(self, bdd)

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
pick_one_inputs(self, 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_state(self, 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_inputs(self, bdd)

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
post(self, 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

pre(self, 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

reachable_states[source]

Return a the set of reachable states of this FSM, represented as a BDD.

Return type:BDD
state_constraints[source]

The BDD of states satisfying the invariants of the FSM.

trans[source]

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

weak_pre(self, states)

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
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[source]

The DD manager of this encoding.

Return type:DDManager
cube_for_inputs_vars(self, variables)

Return the cube for the given input variables.

Parameters:variables – a list of input variable names
Return type:BDD
inputsCube

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

Return type:BDD
inputsMask[source]

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

Return type:BDD
statesCube

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

Return type:BDD
statesInputsMask

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

Return type:BDD
statesMask[source]

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

Return type:BDD
symbTable[source]

The symbols table of this encoding.

Return type:SymbTable
class pynusmv.fsm.SymbTable(pointer, freeit=False)[source]

Bases: pynusmv.utils.PointerWrapper

Python class for symbols table.

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[source]

This transition relation represented as a monolithic BDD.

Return type:BDD
post(self, 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

pre(self, 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

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

Load a model from an SMV file and store it in global data structures.

Parameters:filepath – the path to the SMV file
pynusmv.glob.flatten_hierarchy()[source]

Flatten the read model and store it in global data structures.

Raise :a NuSMVNoReadFileError if no model is read yet
Raise :a NuSMVCannotFlattenError if an error occurred during flattening
Raise :a NuSMVModelAlreadyFlattenedError if the model is already flattened

Warning

In case of type checking errors, a message is printed at stderr and a NuSMVCannotFlattenError is raised.

pynusmv.glob.symb_table()[source]

Return the main symbols table of the current model.

Return type:SymbTable
pynusmv.glob.encode_variables()[source]

Encode the BDD variables of the current model and store it in global data structures.

Raise :a NuSMVNeedFlatHierarchyError if the model is not flattened
Raise :a NuSMVModelAlreadyEncodedError if the variables are already encoded
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 isalready 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.prop_database()[source]

Return the global properties database.

Return type:PropDb
pynusmv.glob.compute_model()[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.

init Module

The pynusmv.init module provides functions to initialize and quit NuSMV.

Warning

init_nusmv() should be called before any other call to pynusmv functions; deinit_nusmv() should be called after using pynusmv.

pynusmv.init.init_nusmv()[source]

Initialize NuSMV. Must be called only once before calling deinit_nusmv().

pynusmv.init.deinit_nusmv()[source]

Quit NuSMV. Must be called only once, after calling init_nusmv().

pynusmv.init.reset_nusmv()[source]

Reset NuSMV, i.e. deinit it and init it again. Cannot be called before init_nusmv().

mc Module

The pynusmv.mc module provides some functions of NuSMV dealing with model checking, like CTL model checking.

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

parser Module

The pynusmv.parser module provides functions to parse strings and return corresponding ASTs.

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.

prop Module

The pynusmv.prop module contains classes and functions dealing with properties and specifications of models.

pynusmv.prop.propTypes = {'LTL': 103, 'Comparison': 107, 'Compute': 106, 'NoType': 101, 'PSL': 104, 'CTL': 102, 'Invariant': 105}

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.

bddFsm[source]

The BDD-encoded FSM of this property.

Return type:BddFsm
expr[source]

The expression of this property.

Return type:Spec
exprcore[source]

The core expression of this property

Return type:Spec
name[source]

The name of this property, as a string.

type[source]

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

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.

get_prop_at_index(self, index)[source]

Return the property stored at index.

Return type:Prop
get_size(self)[source]

Return the number of properties stored in this database.

master[source]

The master property of this database.

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

car[source]

The left child of this specification.

Return type:Spec
cdr[source]

The right child of this specification.

Return type:Spec
type[source]

The type of this specification.

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.nott(spec)[source]

Return a new specification corresponding to NOT spec.

Return type:Spec
pynusmv.prop.andd(left, right)[source]

Return a new specification corresponding to left AND right.

Return type:Spec
pynusmv.prop.orr(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)[source]

Return a new specification corresponding to the given atom. strrep is parsed 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.

Return type:Spec

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: builtins.object

Superclass wrapper for NuSMV pointers.

Every pointer to a NuSMV structure is wrapped in a PointerWrapper or in a subclass of PointerWrapper. Every subclass instance takes a pointer to a NuSMV structure as constructor parameter.

It is the responsibility of PointerWrapper and its subclasses to free the wrapped pointer. Some pointers have to be freed like bdd_ptr, but other do not have to be freed since NuSMV takes care of this; for example, BddFrm_ptr does not have to be freed. To ensure that a pointer is freed only once, PyNuSMV ensures that any pointer is wrapped by only one PointerWrapper (or subclass of it) if the pointer have to be freed.

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

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

Return type:BDD

Note

μZ.f(Z) least fixpoint is implemented with fixpoint(funct, false). νZ.f(Z) greatest fixpoint is implemented with fixpoint(funct, true).

Table Of Contents

Previous topic

Presentation of PyNuSMV

This Page