Hello,

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?

Regards,
Phillip