"""
The :mod:`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.
"""
__all__ = ['load', 'symb_table', 'bdd_encoding', 'prop_database',
'flatten_hierarchy', 'encode_variables', 'build_flat_model',
'build_model', 'compute_model', 'encode_variables_for_layers',
'flat_hierarchy']
import tempfile
import os
from pynusmv_lower_interface.nusmv.parser import parser as nsparser
from pynusmv_lower_interface.nusmv.opt import opt as nsopt
from pynusmv_lower_interface.nusmv.compile import compile as nscompile
from pynusmv_lower_interface.nusmv.enc import enc as nsenc
from pynusmv_lower_interface.nusmv.enc.bool import bool as nsboolenc
from pynusmv_lower_interface.nusmv.enc.bdd import bdd as nsbddenc
from pynusmv_lower_interface.nusmv.enc.base import base as nsbaseenc
from pynusmv_lower_interface.nusmv.prop import prop as nsprop
from pynusmv_lower_interface.nusmv.compile.symb_table import symb_table as nssymb_table
from pynusmv_lower_interface.nusmv.fsm import fsm as nsfsm
from pynusmv_lower_interface.nusmv.set import set as nsset
from pynusmv_lower_interface.nusmv.fsm.bdd import bdd as nsbddfsm
from pynusmv_lower_interface.nusmv.trace import trace as nstrace
from pynusmv_lower_interface.nusmv.trace.exec_ import exec_ as nstraceexec
from .fsm import BddEnc, SymbTable
from .node import FlatHierarchy
from .parser import NuSMVParsingError
from .prop import PropDb
from .exception import (NuSMVLexerError,
NuSMVNoReadModelError,
NuSMVModelAlreadyReadError,
NuSMVCannotFlattenError,
NuSMVModelAlreadyFlattenedError,
NuSMVNeedFlatHierarchyError,
NuSMVModelAlreadyEncodedError,
NuSMVFlatModelAlreadyBuiltError,
NuSMVNeedFlatModelError,
NuSMVModelAlreadyBuiltError,
NuSMVNeedVariablesEncodedError)
__bdd_encoding = None
__prop_database = None
__symb_table = None
__flat_hierarchy = None
def _reset_globals():
"""
Reset the global variables of the module, keeping track of global data
structures.
"""
global __bdd_encoding, __prop_database, __symb_table, __flat_hierarchy
__bdd_encoding = None
__prop_database = None
__symb_table = None
__flat_hierarchy = None
# Reset cmps
nscompile.cmp_struct_reset(nscompile.cvar.cmps)
[docs]def load(*model):
"""
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 :class:`Module <pynusmv.model.Module>`
subclasses); in this case, the model is represented by the set of
modules.
"""
if len(model) == 1 and isinstance(model[0], str):
if os.path.isfile(model[0]):
load_from_file(model[0])
else:
load_from_string(model[0])
else: # model must be a list of modules
load_from_modules(*model)
def load_from_string(model):
"""
Load a model from a string representing the model.
:param model: a String representing the model
:type model: str
"""
# Create temp file
with tempfile.NamedTemporaryFile(suffix=".smv") as tmp:
tmp.write(model.encode("UTF-8"))
tmp.flush()
load_from_file(tmp.name)
def load_from_modules(*modules):
"""
Load a model from a set of modules representing the model.
:param modules: the modules defining the NuSMV model. Must contain a
`main` module.
:type modules: a list of :class:`Module <pynusmv.model.Module>`
subclasses
"""
load_from_string("\n".join(str(module) for module in modules))
def load_from_file(filepath):
"""
Load a model from an SMV file and store it in global data structures.
:param filepath: the path to the SMV file
:type filepath: str
"""
# Check file
if not os.path.exists(filepath):
raise IOError("File {} does not exist".format(filepath))
# Check cmps. Need reset_nusmv if a model is already read
if nscompile.cmp_struct_get_read_model(nscompile.cvar.cmps):
raise NuSMVModelAlreadyReadError("A model is already read.")
# Set the input file
nsopt.set_input_file(nsopt.OptsHandler_get_instance(), filepath)
# Call the parser
# ret = 0 => OK
# ret = 1 => syntax error (and there are registered syntax errors)
# ret = 2 => lexer error
ret = nsparser.Parser_ReadSMVFromFile(filepath)
if ret == 2:
# ret = 2 means lexer error
raise NuSMVLexerError("An error with NuSMV lexer occured.")
# When parsing a model with parser_is_lax enabled (this is the case
# since this is enabled in init_nusmv), the parser gets
# as many correct parts of the model as possible and build a partial
# model with it.
# Raise exceptions if needed
errors = nsparser.Parser_get_syntax_errors_list()
if errors is not None:
raise NuSMVParsingError.from_nusmv_errors_list(errors)
# Update cmps
nscompile.cmp_struct_set_read_model(nscompile.cvar.cmps)
[docs]def flatten_hierarchy(keep_single_enum=False):
"""
Flatten the read model and store it in global data structures.
:param keep_single_enum: whether or not enumerations with single values
should be converted into defines
:type keep_single_enum: bool
:raise: a :exc:`NuSMVNoReadModelError
<pynusmv.exception.NuSMVNoReadModelError>` if no model is read yet
:raise: a :exc:`NuSMVCannotFlattenError
<pynusmv.exception.NuSMVCannotFlattenError>` if an error occurred
during flattening
:raise: a :exc:`NuSMVModelAlreadyFlattenedError
<pynusmv.exception.NuSMVModelAlreadyFlattenedError>` if the model
is already flattened
.. warning:: In case of type checking errors, a message is printed at
stderr and a :exc:`NuSMVCannotFlattenError
<pynusmv.exception.NuSMVCannotFlattenError>` is raised.
"""
# Check cmps
if not nscompile.cmp_struct_get_read_model(nscompile.cvar.cmps):
raise NuSMVNoReadModelError("Cannot flatten; no read model.")
if nscompile.cmp_struct_get_flatten_hrc(nscompile.cvar.cmps):
raise NuSMVModelAlreadyFlattenedError(
"Model already flattened.")
# Update options to reflect keep_single_enum
if keep_single_enum:
nsopt.set_keep_single_value_vars(nsopt.OptsHandler_get_instance())
else:
nsopt.unset_keep_single_value_vars(nsopt.OptsHandler_get_instance())
# Flatten hierarchy
ret = nscompile.flatten_hierarchy()
if ret != 0:
raise NuSMVCannotFlattenError("Cannot flatten the model.")
global __symb_table
__symb_table = SymbTable(nscompile.Compile_get_global_symb_table())
[docs]def symb_table():
"""
Return the main symbols table of the current model.
:rtype: :class:`SymbTable <pynusmv.fsm.SymbTable>`
"""
# Flatten hierarchy if needed
global __symb_table
if __symb_table is None:
if nscompile.cmp_struct_get_flatten_hrc(nscompile.cvar.cmps):
__symb_table = SymbTable(nscompile.Compile_get_global_symb_table())
else:
flatten_hierarchy()
return __symb_table
[docs]def encode_variables(layers={"model"}, variables_ordering=None):
"""
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.
:param layers: the set of layers variables to encode
:type layers: :class:`set`
:param variables_ordering: the file containing a custom ordering
:type variables_ordering: path to file
:raise: a :exc:`NuSMVNeedFlatHierarchyError
<pynusmv.exception.NuSMVNeedFlatHierarchyError>` if the model is
not flattened
:raise: a :exc:`NuSMVModelAlreadyEncodedError
<pynusmv.exception.NuSMVModelAlreadyEncodedError>`
if the variables are already encoded
"""
# Check cmps
if not nscompile.cmp_struct_get_flatten_hrc(nscompile.cvar.cmps):
raise NuSMVNeedFlatHierarchyError("Need flat hierarchy.")
if nscompile.cmp_struct_get_encode_variables(nscompile.cvar.cmps):
raise NuSMVModelAlreadyEncodedError(
"The variables are already encoded.")
if variables_ordering is not None:
nsopt.set_input_order_file(nsopt.OptsHandler_get_instance(),
variables_ordering)
encode_variables_for_layers(layers, init=True)
# Update cmps
nscompile.cmp_struct_set_encode_variables(nscompile.cvar.cmps)
# Get global encoding
global __bdd_encoding
__bdd_encoding = BddEnc(nsenc.Enc_get_bdd_encoding())
[docs]def encode_variables_for_layers(layers={"model"}, init=False):
"""
Encode the BDD variables of the given layers and store them in global data
structures.
:param layers: the set of layers variables to encode
:type layers: :class:`set`
:param bool init: whether or not initialize the global encodings
.. warning: Global encodings should be initialized only once, otherwise,
NuSMV quits unexpectingly. Note that :func:`encode_variables`
initializes them, and should be called before any call to
this function.
"""
if init:
nsenc.Enc_init_bool_encoding()
bool_enc = nsenc.Enc_get_bool_encoding()
base_enc = nsboolenc.boolenc2baseenc(bool_enc)
for layer in layers:
nsbaseenc.BaseEnc_commit_layer(base_enc, layer)
if init:
nsenc.Enc_init_bdd_encoding()
bdd_enc = nsenc.Enc_get_bdd_encoding()
base_enc = nsbddenc.bddenc2baseenc(bdd_enc)
for layer in layers:
nsbaseenc.BaseEnc_commit_layer(base_enc, layer)
[docs]def bdd_encoding():
"""
Return the main bdd encoding of the current model.
:rtype: :class:`BddEnc <pynusmv.dd.BddEnc>`
"""
# Encode variables if needed
global __bdd_encoding
if __bdd_encoding is None:
if nscompile.cmp_struct_get_encode_variables(nscompile.cvar.cmps):
__bdd_encoding = BddEnc(nsenc.Enc_get_bdd_encoding())
else:
encode_variables()
return __bdd_encoding
[docs]def build_flat_model():
"""
Build the Sexp FSM (Simple Expression FSM) of the current model and store
it in global data structures.
:raise: a :exc:`NuSMVNeedFlatHierarchyError
<pynusmv.exception.NuSMVNeedFlatHierarchyError>` if the model is
not flattened
:raise: a :exc:`NuSMVFlatModelAlreadyBuiltError
<pynusmv.exception.NuSMVFlatModelAlreadyBuiltError>` if the Sexp
FSM is already built
"""
# Check cmps
if not nscompile.cmp_struct_get_flatten_hrc(nscompile.cvar.cmps):
raise NuSMVNeedFlatHierarchyError("Need flat hierarchy.")
if nscompile.cmp_struct_get_build_flat_model(nscompile.cvar.cmps):
raise NuSMVFlatModelAlreadyBuiltError(
"The flat model is already built.")
# Simplify the model
st = nscompile.Compile_get_global_symb_table()
layer = nssymb_table.SymbTable_get_layer(st, "model")
ite = nssymb_table.gen_iter(layer, nssymb_table.STT_VAR)
variables = nssymb_table.SymbLayer_iter_to_set(layer, ite)
sexp_fsm = nsfsm.FsmBuilder_create_scalar_sexp_fsm(
nscompile.Compile_get_global_fsm_builder(),
nscompile.cvar.mainFlatHierarchy,
variables)
nsset.Set_ReleaseSet(variables)
nsprop.PropDb_master_set_scalar_sexp_fsm(
nsprop.PropPkg_get_prop_database(),
sexp_fsm)
# Update cmps
nscompile.cmp_struct_set_build_flat_model(nscompile.cvar.cmps)
[docs]def build_model():
"""
Build the BDD FSM of the current model and store it in global data
structures.
:raise: a :exc:`NuSMVNeedFlatModelError
<pynusmv.exception.NuSMVNeedFlatModelError>` if the Sexp FSM
of the model is not built yet
:raise: a :exc:`NuSMVNeedVariablesEncodedError
<pynusmv.exception.NuSMVNeedVariablesEncodedError>` if the
variables of the model are not encoded yet
:raise: a :exc:`NuSMVModelAlreadyBuiltError
<pynusmv.exception.NuSMVModelAlreadyBuiltError>` if the BDD FSM
of the model is already built
"""
# Check cmps
if not nscompile.cmp_struct_get_build_flat_model(nscompile.cvar.cmps):
raise NuSMVNeedFlatModelError("Need flat model.")
if not nscompile.cmp_struct_get_encode_variables(nscompile.cvar.cmps):
raise NuSMVNeedVariablesEncodedError("Need variables encoded.")
if nscompile.cmp_struct_get_build_model(nscompile.cvar.cmps):
raise NuSMVModelAlreadyBuiltError("The model is already built.")
# Build the model
pd = nsprop.PropPkg_get_prop_database()
sexp_fsm = nsprop.PropDb_master_get_scalar_sexp_fsm(pd)
bdd_fsm = nsfsm.FsmBuilder_create_bdd_fsm(
nscompile.Compile_get_global_fsm_builder(),
nsenc.Enc_get_bdd_encoding(),
sexp_fsm,
nsopt.get_partition_method(
nsopt.OptsHandler_get_instance()))
nsprop.PropDb_master_set_bdd_fsm(pd, bdd_fsm)
# Register executors
enc = nsbddfsm.BddFsm_get_bdd_encoding(bdd_fsm)
nstrace.TraceManager_register_complete_trace_executor(
nstrace.TracePkg_get_global_trace_manager(),
"bdd", "BDD partial trace execution",
nstraceexec.bddCompleteTraceExecutor2completeTraceExecutor(
nstraceexec.BDDCompleteTraceExecutor_create(bdd_fsm,
enc)))
nstrace.TraceManager_register_partial_trace_executor(
nstrace.TracePkg_get_global_trace_manager(),
"bdd", "BDD complete trace execution",
nstraceexec.bddPartialTraceExecutor2partialTraceExecutor(
nstraceexec.BDDPartialTraceExecutor_create(bdd_fsm,
enc)))
# Update cmps
nscompile.cmp_struct_set_build_model(nscompile.cvar.cmps)
[docs]def flat_hierarchy():
"""
Return the global flat hierarchy.
:rtype: :class:`FlatHierarchy <pynusmv.node.FlatHierarchy>`
"""
if not nscompile.cmp_struct_get_flatten_hrc(nscompile.cvar.cmps):
# Need a flat hierarchy
raise NuSMVNeedFlatHierarchyError("Need flat hierarchy.")
global __flat_hierarchy
if __flat_hierarchy is None:
__flat_hierarchy = FlatHierarchy(nscompile.cvar.mainFlatHierarchy)
return __flat_hierarchy
[docs]def prop_database():
"""
Return the global properties database.
:rtype: :class:`PropDb <pynusmv.prop.PropDb>`
"""
if not nscompile.cmp_struct_get_flatten_hrc(nscompile.cvar.cmps):
# Need a flat hierarchy
raise NuSMVNeedFlatHierarchyError("Need flat hierarchy.")
global __prop_database
if __prop_database is None:
__prop_database = PropDb(nsprop.PropPkg_get_prop_database())
return __prop_database
[docs]def compute_model(variables_ordering=None, keep_single_enum=False):
"""
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.
:param variables_ordering: the file containing a custom ordering
:type variables_ordering: path to file
:param keep_single_enum: whether or not enumerations with single values
should be converted into defines
:type keep_single_enum: bool
"""
if not nscompile.cmp_struct_get_read_model(nscompile.cvar.cmps):
raise NuSMVNoReadModelError("No read model.")
# Check cmps and perform what is needed
if not nscompile.cmp_struct_get_flatten_hrc(nscompile.cvar.cmps):
flatten_hierarchy(keep_single_enum=keep_single_enum)
if not nscompile.cmp_struct_get_encode_variables(nscompile.cvar.cmps):
encode_variables(variables_ordering=variables_ordering)
if not nscompile.cmp_struct_get_build_flat_model(nscompile.cvar.cmps):
build_flat_model()
if not nscompile.cmp_struct_get_build_model(nscompile.cvar.cmps):
build_model()