17 Nov
2021
17 Nov
'21
2:58 p.m.
Fatma Faruq <ffaruq(a)gmail.com> writes:
Hi,
I was wondering if someone could point me to resources in spot that
show how to evaluate an LTL word or trace on an automaton.
Or anyway to check whether a trace or word satisfies a particular LTL
formula.
Hi Fatma,
If you convert your word into another automaton, testing acceptance
can be reduced to an intersection between your two automata.
import spot
aut = spot.translate('a U b')
wrd =
spot.parse_word('a&!b;a&!b;cycle{a&b;!a&!b}').as_automaton()
print("aut {} wrd".format("accepts" if aut.intersects(wrd) else
"rejects"))
Alexandre