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.
I'm new to Spot. So far I've been able to use the python notebook - word, (and other examples) to iterate over an automaton generated from an LTL formula.
Thank you so much,
Fatma Faruq ffaruq@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
-
Alexandre Duret-Lutz -
Fatma Faruq