31 Dec
2020
31 Dec
'20
5:45 p.m.
Hi Philip,
Philip Schwartz <pschwartz090(a)gmail.com> writes:
If I have a deterministic automata and an LTL or
python function which
gets a word and return T/F.
Is it possible to set model checking for the dfa? to get a
counterexample which distinguishes the dfa and the LTL/ python target
function?
I'm not sure what this means. The LTL formula can be converted into an
automaton. If you want to know if that automaton intersects another
one, you can call aut1.intersects(aut2), that usually what model
checkers do. The variant aut1.intersecting_word(aut2) will return a
word accepted by both automata. To obtain a word that is accepted by
one automaton and rejected by the other one, you may use
aut1.exclusive_word(aut2).