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