Source code for pynusmv.sexp.fsm
'''
This module defines the classes wrapping the SEXP FSM structures.
In particular:
- :class:`SexpFsm` which wraps the basic SEXP fsm
- :class:`BoolSexpFsm` which wraps a boolean SEXP fsm
'''
from pynusmv_lower_interface.nusmv.fsm.sexp import sexp as _sexp
from pynusmv.fsm import SymbTable
from pynusmv.utils import PointerWrapper
from pynusmv.node import Node, FlatHierarchy
from pynusmv.collections import NodeList, NodeIterator
__all__ = ['SexpFsm', 'BoolSexpFsm']
[docs]class SexpFsm(PointerWrapper):
"""
This class encapsulates a generic SEXP FSM
"""
# NOT exposed because never used in NuSMV:
# - SexpFsm_create_predicate_normalised_copy
# - SexpFsm_apply_synchronous_product
# - SexpFsm_get_var_init
# - SexpFsm_get_var_invar
# - SexpFsm_get_var_input
# - SexpFsm_self_check
#
# NOT exposed for other reason:
# - SexpFsm_get_var_trans (only used in FsmBuilder_create_bdd_fsm_of_vars)
# - variables_set not exposed as it is useless once we have variables_list
def __init__(self, ptr, freeit=True):
"""
Creates a new instance from the given pointer
:param ptr: the pointer to wrap (SexpFsm_ptr)
:param freeit: a flag indicating whether or not the undeflying fsm
should be destroyed upon garbage collection
"""
super().__init__(ptr, freeit=freeit)
def _free(self):
"""
Destroys the underlying fsm if needed
"""
if self._freeit and self._ptr is not None:
_sexp.SexpFsm_destroy(self._as_SexpFsm_ptr())
self.freeit = False
self._ptr = None
def _as_SexpFsm_ptr(self):
"""
Returns a pointer representing this object of the type SexpFsm_ptr.
This method is useful to seamlessly implement the polymorphism of the
subclasses
"""
return self._ptr
[docs] def copy(self):
"""
Creates a copy of this object
:return: a copy of this object
"""
return SexpFsm(_sexp.BoolSexpFsm_copy(self._as_SexpFsm_ptr()))
def __copy__(self):
"""
Creates a copy of this object
:return: a copy of this object
"""
return self.copy()
@property
def symbol_table(self):
"""
:return: the symbol table associated to this FSM.
"""
return SymbTable(_sexp.SexpFsm_get_symb_table(self._as_SexpFsm_ptr()))
@property
def is_boolean(self):
"""
:return: true iff this fsm is a boolean SEXP FSM
"""
return bool(_sexp.SexpFsm_is_boolean(self._as_SexpFsm_ptr()))
@property
def hierarchy(self):
"""
:return: the flat hierarchy associated to this object
"""
return FlatHierarchy(_sexp.SexpFsm_get_hierarchy(self._as_SexpFsm_ptr()))
@property
def init(self):
"""
:return: an Expression that collects init states for all handled vars.
"""
return Node.from_ptr(_sexp.SexpFsm_get_init(self._as_SexpFsm_ptr()))
@property
def invariants(self):
"""
:return: an Expression that collects invar states for all handled vars.
"""
return Node.from_ptr(_sexp.SexpFsm_get_invar(self._as_SexpFsm_ptr()))
@property
def trans(self):
"""
:return: an Expression that collects all next states for all variables
"""
return Node.from_ptr(_sexp.SexpFsm_get_trans(self._as_SexpFsm_ptr()))
@property
def input(self):
"""
:return: an Expression that collects all input states for all variables
"""
# I don"t get it, this method always returns None
return Node.from_ptr(_sexp.SexpFsm_get_input(self._as_SexpFsm_ptr()))
@property
def justice(self):
"""
The list of sexp expressions defining the set of justice constraints
for this FSM.
.. note::
NUSMV supports two types of fairness constraints, namely justice
constraints and com- passion constraints. A justice constraint
consists of a formula f, which is assumed to be true infinitely
often in all the fair paths. In NUSMV, justice constraints are
identified by keywords JUSTICE and, for backward compatibility,
FAIRNESS.
:return: the list of sexp expressions defining the set of justice
constraints for this FSM.
"""
ptr = _sexp.SexpFsm_get_justice(self._as_SexpFsm_ptr())
return NodeIterator.from_pointer(ptr)
@property
def compassion(self):
"""
The list of sexp expressions defining the set of compassion constraints
for this FSM.
.. note::
NUSMV supports two types of fairness constraints, namely justice
constraints and compassion constraints. A justice constraint
consists of a formula f, which is assumed to be true infinitely
often in all the fair paths. A compassion constraint consists of a
pair of formulas (p,q); if property p is true infinitely often in a
fair path, then also formula q has to be true infinitely often in
the fair path. In NUSMV, compassion constraints are identified by
keyword COMPASSION. If compassion constraints are used, then the
model must not contain any input variables. Currently, NUSMV does
not enforce this so it is the responsibility of the user to
make sure that this is the case.
:return: the list of sexp expressions defining the set of compassion
constraints for this FSM.
"""
ptr = _sexp.SexpFsm_get_compassion(self._as_SexpFsm_ptr())
return NodeIterator.from_pointer(ptr)
@property
def variables_list(self):
"""
:return: the set of variables in the FSM
"""
return NodeList(_sexp.SexpFsm_get_vars_list(self._as_SexpFsm_ptr()))
@property
def symbols_list(self):
"""
:return: the set of symbols in the FSM
"""
return NodeList(_sexp.SexpFsm_get_symbols_list(self._as_SexpFsm_ptr()))
@property
def is_syntactically_universal(self):
"""
Checks if the SexpFsm is syntactically universal:
Checks INIT, INVAR, TRANS, INPUT, JUSTICE, COMPASSION to be empty
(ie: True Expr). In this case returns true, false otherwise
:return: true iff this fsm has no INIT, INVAR, TRANS, INPUT, JUSTICE or
COMPASSION.
"""
return bool(_sexp.SexpFsm_is_syntactically_universal(self._as_SexpFsm_ptr()))
[docs]class BoolSexpFsm(SexpFsm):
"""
This class encapsulates a boolean encoded SEXP FSM.
.. note::
Since it defines the same interface as the regular SexpFSM, the purpose
of this class is to correctly redefine the _free function and override
the _as_SexpFsm_ptr function so as to leverage the inheritance defined
in C.
"""
def __init__(self, ptr, freeit=True):
"""
Creates a new instance from the given pointer
:param ptr: the pointer to wrap (SexpFsm_ptr)
:param freeit: a flag indicating whether or not the undeflying fsm
should be destroyed upon garbage collection
"""
super().__init__(ptr, freeit=freeit)
def _free(self):
"""
Destroys the underlying fsm if needed
"""
if self._freeit and self._ptr is not None:
_sexp.BoolSexpFsm_destroy(self._as_SexpFsm_ptr())
self.freeit = False
self._ptr = None
def _as_SexpFsm_ptr(self):
"""
Returns a pointer representing this object of the type SexpFsm_ptr.
This method is useful to seamlessly implement the polymorphism of the
subclasses
.. note:: this method overrides that from SexpFsm
"""
return _sexp.boolsexpfsm_to_sexpfsm(self._ptr)
# TODO: complete with missing functions