"""
The :mod:`pynusmv.fsm` module provides some functionalities about FSMs
represented and stored by NuSMV:
* :class:`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.
* :class:`BddEnc` represents the BDD encoding, with some functionalities like
getting the state mask or the input variables mask.
* :class:`SymbTable` represents the symbols table of the model.
* :class:`BddTrans` represents a transition relation encoded with BDDs. It
provides access to pre and post operations.
"""
__all__ = ['BddFsm', 'BddEnc', 'SymbTable', 'BddTrans']
from .nusmv.fsm.bdd import bdd as bddFsm
from .nusmv.enc.bdd import bdd as bddEnc
from .nusmv.enc.base import base as nsbaseEnc
from .nusmv.cmd import cmd as nscmd
from .nusmv.trans.bdd import bdd as nsbddtrans
from .dd import BDD, State, Inputs, DDManager
from .utils import PointerWrapper, fixpoint
from .exception import NuSMVBddPickingError
[docs]class BddFsm(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.
"""
# BddFsm do not have to be freed.
def __init__(self, ptr, freeit = False):
"""
Create a new BddFsm.
:param ptr: the pointer of the NuSMV FSM
:param boolean freeit: whether or not free the pointer
"""
super().__init__(ptr, freeit = freeit)
self._reachable = None
@property
[docs] def bddEnc(self):
"""
The BDD encoding of this FSM.
"""
return BddEnc(bddFsm.BddFsm_get_bdd_encoding(self._ptr))
@property
[docs] def init(self):
"""
The BDD of initial states of this FSM.
"""
return BDD(bddFsm.BddFsm_get_init(self._ptr), self.bddEnc.DDmanager,
freeit = True)
@property
def trans(self):
"""
The transition relation (:class:`BddTrans`) of this FSM.
Can also be replaced.
"""
# Do not free the trans, this FSM is the owner of it
return BddTrans(bddFsm.BddFsm_get_trans(self._ptr),
self.bddEnc,
self.bddEnc.DDmanager,
freeit = False)
@trans.setter
[docs] def trans(self, new_trans):
"""
Set this FSM transition to `new_trans`.
"""
# Copy the transition such that this FSM is the owner
new_trans_ptr = nsbddtrans.BddTrans_copy(new_trans._ptr)
# Get old trans
old_trans_ptr = bddFsm.BddFsm_get_trans(self._ptr)
# Set the new trans
self._ptr.trans = new_trans_ptr
# Free old trans
nsbddtrans.BddTrans_free(old_trans_ptr)
@property
[docs] def state_constraints(self):
"""
The BDD of states satisfying the invariants of the FSM.
"""
return BDD(bddFsm.BddFsm_get_state_constraints(self._ptr),
self.bddEnc.DDmanager, freeit = True)
@property
@property
[docs] def fairness_constraints(self):
"""
The list of fairness constraints, as BDDs.
"""
justiceList = bddFsm.BddFsm_get_justice(self._ptr)
fairnessList = bddFsm.justiceList2fairnessList(justiceList)
ite = bddFsm.FairnessList_begin(fairnessList)
fairBdds = []
while not bddFsm.FairnessListIterator_is_end(ite):
fairBdds.append(
BDD(bddFsm.JusticeList_get_p(justiceList, ite),
self.bddEnc.DDmanager, freeit = True))
ite = bddFsm.FairnessListIterator_next(ite)
return fairBdds
[docs] def pre(self, states, inputs = None):
"""
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.
:param states: the states from which getting the pre-image
:type states: :class:`BDD <pynusmv.dd.BDD>`
:param inputs: the inputs through which getting the pre-image
:type inputs: :class:`BDD <pynusmv.dd.BDD>`
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
if inputs is None:
return BDD(bddFsm.BddFsm_get_backward_image(self._ptr, states._ptr),
self.bddEnc.DDmanager, freeit = True)
else:
return BDD(bddFsm.BddFsm_get_constrained_backward_image(
self._ptr, states._ptr, inputs._ptr),
self.bddEnc.DDmanager, freeit = True)
[docs] def post(self, states, inputs = None):
"""
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.
:param states: the states from which getting the post-image
:type states: :class:`BDD <pynusmv.dd.BDD>`
:param inputs: the inputs through which getting the post-image
:type inputs: :class:`BDD <pynusmv.dd.BDD>`
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
if inputs is None:
return BDD(bddFsm.BddFsm_get_forward_image(self._ptr, states._ptr),
self.bddEnc.DDmanager, freeit = True)
else:
return BDD(bddFsm.BddFsm_get_constrained_forward_image(
self._ptr, states._ptr, inputs._ptr),
self.bddEnc.DDmanager, freeit = True)
[docs] def pick_one_state(self, bdd):
"""
Return a BDD representing a state of `bdd`.
:rtype: :class:`State <pynusmv.dd.State>`
:raise: a :exc:`NuSMVBddPickingError
<pynusmv.exception.NuSMVBddPickingError>`
if `bdd` is false or an error occurs while picking one state
(for example if the bdd does not contain any state but inputs)
"""
if bdd.is_false():
raise NuSMVBddPickingError("Cannot pick state from false BDD.")
state = bddEnc.pick_one_state(self.bddEnc._ptr, bdd._ptr)
if state is None:
raise NuSMVBddPickingError("Cannot pick state from BDD.")
return State(state, self, freeit = True)
[docs] def count_states(self, bdd):
"""
Return the number of states of the given BDD.
:param bdd: the concerned BDD
:type bdd: :class:`BDD <pynusmv.dd.BDD>`
"""
# Apply mask before counting states
bdd = bdd & self.bddEnc.statesMask
return bddEnc.BddEnc_count_states_of_bdd(self.bddEnc._ptr, bdd._ptr)
[docs] def pick_all_states(self, bdd):
"""
Return a tuple of all states belonging to `bdd`.
:param bdd: the concerned BDD
:type bdd: :class:`BDD <pynusmv.dd.BDD>`
:rtype: tuple(:class:`State <pynusmv.dd.State>`)
:raise: a :exc:`NuSMVBddPickingError
<pynusmv.exception.NuSMVBddPickingError>`
if something is wrong
"""
# FIXME Still get segmentation faults. Need investigation.
# tests/pynusmv/testFsm.py seems to raise segmentation faults
# Apply mask
bdd = bdd & self.bddEnc.statesMask
# Get all states
(err, t) = bddEnc.pick_all_terms_states(self.bddEnc._ptr, bdd._ptr)
if err:
raise NuSMVBddPickingError("Cannot pick all states.")
else:
return tuple(State(te, self) for te in t)
@property
[docs] def reachable_states(self):
"""
Return a the set of reachable states of this FSM, represented as a BDD.
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
if self._reachable is None:
#self._reachable = fixpoint(lambda Z: (self.init | self.post(Z)),
# BDD.false(self.bddEnc.DDmanager))
self._reachable = BDD(bddFsm.BddFsm_get_reachable_states(self._ptr),
self.bddEnc.DDmanager)
return self._reachable
# ==========================================================================
# ===== Static methods =====================================================
# ==========================================================================
@staticmethod
[docs] def from_filename(filepath):
"""
Return the FSM corresponding to the model in `filepath`.
:param filepath: the path to the SMV model
"""
# This function modifies the global environment of NuSMV.
from . import glob
glob.load_from_file(filepath)
glob.compute_model()
propDb = glob.prop_database()
return propDb.master.bddFsm
# TODO Remove this and use glob module instead
[docs]class BddEnc(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.
"""
# BddEnc do not have to be freed.
@property
[docs] def DDmanager(self):
"""
The DD manager of this encoding.
:rtype: :class:`DDManager <pynusmv.dd.DDManager>`
"""
return DDManager(bddEnc.BddEnc_get_dd_manager(self._ptr))
@property
[docs] def symbTable(self):
"""
The symbols table of this encoding.
:rtype: :class:`SymbTable`
"""
base_enc = bddEnc.bddenc2baseenc(self._ptr)
return SymbTable(nsbaseEnc.BaseEnc_get_symb_table(base_enc))
@property
[docs] def statesMask(self):
"""
The mask for all state variables, represented as a BDD.
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
return BDD(bddEnc.BddEnc_get_state_frozen_vars_mask_bdd(self._ptr),
self.DDmanager, freeit = True)
@property
[docs]class SymbTable(PointerWrapper):
"""
Python class for symbols table.
"""
# Symbols tables are never freed. NuSMV takes care of it.
pass
[docs]class BddTrans(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.
"""
def __init__(self, ptr, enc = None, manager = None, freeit = True):
"""
Create a new BddTrans.
:param ptr: a NuSMV pointer to a BddTrans
:param enc: the BDD encoding of the transition relation
:type enc: :class:`BddEnc`
:param manager: the DD manager of the BDDs used to encode the relation
:type manager: :class:`DDManager <pynusmv.dd.DDManager>`
:param freeit: whether or not freeing the pointer
"""
super().__init__(ptr, freeit)
self._enc = enc
self._manager = manager
@property
[docs] def monolithic(self):
"""
This transition relation represented as a monolithic BDD.
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
ptr = nsbddtrans.BddTrans_get_monolithic_bdd(self._ptr)
return BDD(ptr, self._manager, freeit = True)
[docs] def pre(self, states, inputs=None):
"""
Compute the pre-image of `states`, through `inputs` if not `None`.
:param states: the concerned states
:type states: :class:`BDD <pynusmv.dd.BDD>`
:param inputs: possible inputs
:type inputs: :class:`BDD <pynusmv.dd.BDD>`
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
nexts = BDD(
bddEnc.BddEnc_state_var_to_next_state_var(self._enc._ptr,
states._ptr),
states._manager, freeit = True)
if inputs is not None:
nexts = nexts & inputs
img = nsbddtrans.BddTrans_get_backward_image_state(
self._ptr, nexts._ptr)
return BDD(img, self._manager, freeit = True)
[docs] def post(self, states, inputs=None):
"""
Compute the post-image of `states`, through `inputs` if not `None`.
:param states: the concerned states
:type states: :class:`BDD <pynusmv.dd.BDD>`
:param inputs: possible inputs
:type inputs: :class:`BDD <pynusmv.dd.BDD>`
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
if inputs is not None:
states = states & inputs
img = nsbddtrans.BddTrans_get_forward_image_state(
self._ptr, states._ptr)
img = bddEnc.BddEnc_next_state_var_to_state_var(self._enc._ptr, img)
return BDD(img, self._manager, freeit = True)