On Thu, Oct 20, 2011 at 6:20 PM, Alexandre Duret-Lutz adl@lrde.epita.fr wrote:
When I run "./complement -S -a x.tgba" in the tgbatest directory, it displays an automaton with some acceptance states (using two different acceptance conditions: Acc["1$1"] and Acc["1$2"]), and although I have not checked every accepting path, I think it looks OK. However if I edit complementation.cc to output the automaton with tgba_save_reachable() instead of dotty_reachable(), the automaton still declares two acceptance conditions, but only one is used by the transitions (hence the language is empty, which is wrong). So there is definitively something fishy here. I believe maybe the encoding used for the acceptance conditions in Safra is wrong. I'll try to look at this more closely before next week.
Actually, the encoding of the the acceptance conditions used when converting the Streett automaton into a TGBA is really bogus when using more than one acceptance condition is needed. The attached patch should fix it. Could you try it? I plan to do further tests too.