RuntimeError when checking CTL formula

Hi,

Model checking A (true R p) produces a runtime error. Although this formula does not make sense (it should be equivalent to p), it is a valid CTL formula. The following piece of code shows the problem:

import pyModelChecking
from pyModelChecking.CTL.language import A, R, Bool, AtomicProposition

kripke = pyModelChecking.kripke.Kripke(
    S  = [0, 1],
    S0 = {0},
    R  = [(0, 1), (1, 1)],
    L  = {0: set(), 1: set('p')}
)

formula = A(R(Bool(True), AtomicProposition('p')))

pyModelChecking.CTL.model_checking.modelcheck(kripke, formula)

Its output is this:

Traceback (most recent call last):
  File "example.py", line 13, in <module>
    pyModelChecking.CTL.model_checking.modelcheck(kripke, formula)
  File ".../pyModelChecking/CTL/model_checking.py", line 208, in modelcheck
    return _checkStateFormula(kripke, formula, L=dict())
  File ".../pyModelChecking/CTL/model_checking.py", line 158, in _checkStateFormula
    Lalter_formula = _checkStateFormula(kripke, restr_f, L)
  File ".../pyModelChecking/CTL/model_checking.py", line 126, in _checkStateFormula
    return _checkNot(kripke, formula, L)
  File ".../pyModelChecking/CTL/model_checking.py", line 40, in _checkNot
    Lphi = _checkStateFormula(kripke, formula.subformula(0), L)
  File ".../pyModelChecking/CTL/model_checking.py", line 151, in _checkStateFormula
    return _checkEU(kripke, formula, L)
  File ".../pyModelChecking/CTL/model_checking.py", line 99, in _checkEU
    L[formula] = subgraph.get_reachable_set_from(Lphi[1])
  File ".../pyModelChecking/graph.py", line 192, in get_reachable_set_from
    for d in self.next(s):
  File ".../pyModelChecking/graph.py", line 108, in next
    raise RuntimeError('src = \'{}\' is not a node '.format(src) +
RuntimeError: src = '0' is not a node of (V=dict_keys([]), E=[])

albertocasagrande / pyModelChecking

RuntimeError when checking CTL formula #4