Dear SPOT developers,
I am doing a research on translation of LTL to BA and I am using the tool
"ltl2tgba" included in the SPOT 0.7.1 distribution as a reference.
While comparing "ltl2tgba" to some other translations using the "lbtt" tool, I
have noticed that it sometimes produces different results (regarding the size of
produced automata) without changing any parameters. It appers that for some
formulae it nondeterministicaly produces different automata. I attach an example
when "ltl2tgba" was executed four times in the row always producing a different
automaton. First three automata differs only by the names of states or the
ordering of transitions, while the last automaton has one state less than the
others. However, all automata seam to be correct and mutually equivalent.
After a closer examination, it seams that this behavior is caused be the -r7
option enabling tau03 formula reductions. Similar behavior can be observed using
-r5 or -r6 options as well. The question is whether such a nondeterminstic
behavior is expected while using language containment formula reductions or it
is caused by an implementation bug.
Thank you for your help.
Best regards,
Tomas Babiak
