"""
The :mod:`pynusmv.mc` module provides some functions of NuSMV dealing with
model checking, like CTL model checking.
"""
__all__ = ['check_ctl_spec', 'eval_simple_expression', 'eval_ctl_spec',
'ef', 'eg', 'ex', 'eu', 'au',
'explain', 'explainEX', 'explainEU', 'explainEG']
from pynusmv_lower_interface.nusmv.node import node as nsnode
from pynusmv_lower_interface.nusmv.dd import dd as nsdd
from pynusmv_lower_interface.nusmv.mc import mc as nsmc
from .dd import BDD, State, Inputs, BDDList
from .prop import atom
[docs]def check_ctl_spec(fsm, spec, context=None):
"""
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.
:param fsm: the concerned FSM
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param spec: a specification about `fsm`
:type spec: :class:`Spec <pynusmv.prop.Spec>`
:param context: the context in which evaluate `spec`
:type context: :class:`Spec <pynusmv.prop.Spec>`
:rtype: bool
"""
sat = eval_ctl_spec(fsm, spec, context)
unsatinit = fsm.init & fsm.state_constraints & fsm.fair_states & ~sat
return unsatinit.is_false()
[docs]def eval_simple_expression(fsm, sexp):
"""
Return the set of states of `fsm` satisfying `sexp`, as a BDD.
`sexp` is first parsed, then evaluated on `fsm`.
:param fsm: the concerned FSM
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param sexp: a simple expression, as a string
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
return eval_ctl_spec(fsm, atom(sexp))
[docs]def eval_ctl_spec(fsm, spec, context=None):
"""
Return the set of states of `fsm` satisfying `spec` in `context`, as a BDD.
:param fsm: the concerned FSM
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param spec: a specification about `fsm`
:type spec: :class:`Spec <pynusmv.prop.Spec>`
:param context: the context in which evaluate `spec`
:type context: :class:`Spec <pynusmv.prop.Spec>`
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
enc = fsm.bddEnc
specbdd = BDD(nsmc.eval_ctl_spec(fsm._ptr, enc._ptr,
spec._ptr,
context and context._ptr or None),
enc.DDmanager, freeit=True)
return specbdd
[docs]def ef(fsm, states):
"""
Return the set of states of `fsm` satisfying `EF states`, as a BDD.
:param fsm: the concerned FSM
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param states: a set of states of `fsm`
:type states: :class:`BDD <pynusmv.dd.BDD>`
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
return BDD(nsmc.ef(fsm._ptr, states._ptr),
fsm.bddEnc.DDmanager, freeit=True)
[docs]def eg(fsm, states):
"""
Return the set of states of `fsm` satisfying `EG states`, as a BDD.
:param fsm: the concerned FSM
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param states: a set of states of `fsm`
:type states: :class:`BDD <pynusmv.dd.BDD>`
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
return BDD(nsmc.eg(fsm._ptr, states._ptr),
fsm.bddEnc.DDmanager, freeit=True)
[docs]def ex(fsm, states):
"""
Return the set of states of `fsm` satisfying `EX states`, as a BDD.
:param fsm: the concerned FSM
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param states: a set of states of `fsm`
:type states: :class:`BDD <pynusmv.dd.BDD>`
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
return BDD(nsmc.ex(fsm._ptr, states._ptr),
fsm.bddEnc.DDmanager, freeit=True)
[docs]def eu(fsm, s1, s2):
"""
Return the set of states of `fsm` satisfying `E[s1 U s2]`, as a BDD.
:param fsm: the concerned FSM
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param s1: a set of states of `fsm`
:type s1: :class:`BDD <pynusmv.dd.BDD>`
:param s2: a set of states of `fsm`
:type s2: :class:`BDD <pynusmv.dd.BDD>`
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
return BDD(nsmc.eu(fsm._ptr, s1._ptr, s1._ptr),
fsm.bddEnc.DDmanager, freeit=True)
[docs]def au(fsm, s1, s2):
"""
Return the set of states of `fsm` satisfying `A[s1 U s2]`, as a BDD.
:param fsm: the concerned FSM
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param s1: a set of states of `fsm`
:type s1: :class:`BDD <pynusmv.dd.BDD>`
:param s2: a set of states of `fsm`
:type s2: :class:`BDD <pynusmv.dd.BDD>`
:rtype: :class:`BDD <pynusmv.dd.BDD>`
"""
return BDD(nsmc.au(fsm._ptr, s1._ptr, s1._ptr),
fsm.bddEnc.DDmanager, freeit=True)
[docs]def explain(fsm, state, spec, context=None):
"""
Explain why `state` of `fsm` satisfies `spec` in `context`.
:param fsm: the system
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param state: a state of `fsm`
:type state: :class:`State <pynusmv.dd.State>`
:param spec: a specification about `fsm`
:type spec: :class:`Spec <pynusmv.prop.Spec>`
:param context: the context in which evaluate `spec`
:type context: :class:`Spec <pynusmv.prop.Spec>`
Return a tuple `t` composed of states (:class:`State <pynusmv.dd.State>`)
and inputs (:class:`Inputs <pynusmv.dd.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.
"""
if context is not None:
context_ptr = context._ptr
else:
context_ptr = None
enc = fsm.bddEnc
manager = enc.DDmanager
path = nsnode.cons(nsnode.bdd2node(nsdd.bdd_dup(state._ptr)), None)
expl = nsmc.explain(fsm._ptr, enc._ptr, path, spec._ptr, context_ptr)
if expl is None:
expl = nsnode.cons(nsnode.bdd2node(nsdd.bdd_dup(state._ptr)), None)
bddlist = BDDList(expl, manager)
bddlist = bddlist.to_tuple()
path = []
path.insert(0, State.from_bdd(bddlist[0], fsm))
for i in range(1, len(bddlist), 2):
inputs = Inputs.from_bdd(bddlist[i], fsm)
state = State.from_bdd(bddlist[i + 1], fsm)
path.insert(0, inputs)
path.insert(0, state)
return tuple(path)
[docs]def explainEX(fsm, state, a):
"""
Explain why `state` of `fsm` satisfies `EX phi`, where `a` is
the set of states of `fsm` satisfying `phi`, represented by a BDD.
:param fsm: the system
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param state: a state of `fsm`
:type state: :class:`State <pynusmv.dd.State>`
:param a: the set of states of `fsm` satisfying `phi`
:type a: :class:`BDD <pynusmv.dd.BDD>`
Return `(s, i, s')` tuple where `s` (:class:`State <pynusmv.dd.State>`)
is the given state, `s'` (:class:`State <pynusmv.dd.State>`) is a successor
of `s` belonging to `a` and `i` (:class:`Inputs <pynusmv.dd.Inputs>`)
is the inputs to go from `s` to `s'` in `fsm`.
"""
enc = fsm.bddEnc
manager = enc.DDmanager
path = nsnode.cons(nsnode.bdd2node(nsdd.bdd_dup(state._ptr)), None)
bddlist = BDDList(nsmc.ex_explain(fsm._ptr, enc._ptr, path, a._ptr),
manager)
# bddlist is reversed!
statep = State.from_bdd(bddlist[0], fsm)
inputs = Inputs.from_bdd(bddlist[1], fsm)
state = State.from_bdd(bddlist[2], fsm)
return (state, inputs, statep)
[docs]def explainEU(fsm, state, a, b):
"""
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.
:param fsm: the system
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param state: a state of `fsm`
:type state: :class:`State <pynusmv.dd.State>`
:param a: the set of states of `fsm` satisfying `phi`
:type a: :class:`BDD <pynusmv.dd.BDD>`
:param b: the set of states of `fsm` satisfying `psi`
:type b: :class:`BDD <pynusmv.dd.BDD>`
Return a tuple `t` composed of states (:class:`State <pynusmv.dd.State>`)
and inputs (:class:`Inputs <pynusmv.dd.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`.
"""
enc = fsm.bddEnc
manager = enc.DDmanager
path = nsnode.cons(nsnode.bdd2node(nsdd.bdd_dup(state._ptr)), None)
bddlist = BDDList(nsmc.eu_explain(fsm._ptr, enc._ptr,
path, a._ptr, b._ptr), manager)
bddlist = bddlist.to_tuple()
path = []
path.insert(0, State.from_bdd(bddlist[0], fsm))
for i in range(1, len(bddlist), 2):
inputs = Inputs.from_bdd(bddlist[i], fsm)
state = State.from_bdd(bddlist[i + 1], fsm)
path.insert(0, inputs)
path.insert(0, state)
return tuple(path)
[docs]def explainEG(fsm, state, a):
"""
Explain why `state` of `fsm` satisfies `EG phi`, where `a` the set of
states of `fsm` satisfying `phi`, represented by a BDD.
:param fsm: the system
:type fsm: :class:`BddFsm <pynusmv.fsm.BddFsm>`
:param state: a state of `fsm`
:type state: :class:`State <pynusmv.dd.State>`
:param a: the set of states of `fsm` satisfying `phi`
:type a: :class:`BDD <pynusmv.dd.BDD>`
Return a tuple `(t, (i, loop))`
where `t` is a tuple composed of states (:class:`State <pynusmv.dd.State>`)
and inputs (:class:`Inputs <pynusmv.dd.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`.
"""
enc = fsm.bddEnc
manager = enc.DDmanager
path = nsnode.cons(nsnode.bdd2node(nsdd.bdd_dup(state._ptr)), None)
bddlist = BDDList(nsmc.eg_explain(fsm._ptr, enc._ptr, path, a._ptr),
manager)
bddlist = bddlist.to_tuple()
path = []
# Discard last state and input, store them as loop indicators
loopstate = State.from_bdd(bddlist[0], fsm)
loopinputs = Inputs.from_bdd(bddlist[1], fsm)
# Consume first state
curstate = State.from_bdd(bddlist[2], fsm)
if curstate._ptr == loopstate._ptr:
loopstate = curstate
path.insert(0, curstate)
for i in range(3, len(bddlist), 2):
inputs = Inputs.from_bdd(bddlist[i], fsm)
curstate = State.from_bdd(bddlist[i + 1], fsm)
if curstate._ptr == loopstate._ptr:
loopstate = curstate
path.insert(0, inputs)
path.insert(0, curstate)
return (tuple(path), (loopinputs, loopstate))