modelcheck results are not clear

[eladbenami]

hi, im running simple traffic-light automaton and i'm not sure i understand the result. with formula_a, i got empty set but with formula_b, i got {1,2,3} formula_a and formula_b are the same except of the order of the inner parts.

can you please help? is it my mistake?

from pyModelChecking.kripke import Kripke
from pyModelChecking.LTL import *

p = Parser()

K = Kripke(S=[1, 2, 3],
           S0=[1],
           R=[(1, 2), (2, 3), (3, 1)],
           L={1: set(['green']),
              2: set(['yellow']),
              3: set(['red'])}
           )

formula_a = 'A(G( (green or yellow or red) and not(green and yellow)  and not(green and red) and not(red and yellow)))'
formula_b = 'A(G(not(green and yellow) and not(green and red) and not(red and yellow) and (green or yellow or red) ))'

res = modelcheck(K, formula_a)
print(res)

[albertocasagrande]

Hi, you discovered a bug affecting the model checking procedure when the formula contains an Or with more than 2 subformulas. I fixed the bug in version 1.3.2 (you can update the package by using pip). Thank you so much for highlighting it.

As far as your code concerns, the parser is not needed. It is suggested, for efficiency purpose, if you want to parse many strings, but you are model checking only one string.

[eladbenami]

working! thank you !