albertocasagrande/pyModelChecking

The `modelcheck` function does not always return the same result

Closed this issue · 0 comments

The modelcheck function does not always return the same value. For instance, the program

from pyModelChecking import *
from pyModelChecking.LTL import *

psi=A(And('one',X(And('two',X('three')))))

K = Kripke(R=[(0, 1), (1, 2), (2, 3), (3, 3)],
           L={0: ['one'], 1: ['two'], 2: ['three']})

print(modelcheck(K, psi))

sometimes prints set() and sometimes {0}.