20 Oct
2011
20 Oct
'11
6:54 p.m.
On Thu, Oct 20, 2011 at 6:20 PM, Alexandre Duret-Lutz <adl(a)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.
--
Alexandre Duret-Lutz