search

albertocasagrande / pyModelChecking

A Python model checking package
Other
58 stars 11 forks source link

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

Closed albertocasagrande closed 4 years ago

albertocasagrande commented 4 years ago

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}.