Hi Nikos and Martin,
You are both talking about complementation, so let me answer your two mails at once.
On 18/10/11 15:38, Nikos Gorogiannis wrote:
There seem to be at least three complementation algorithms in Spot. I have constructed an automaton as a TGBA; can all algorithms be used with it? From my reading, the kv and saba cannot, as they treat the TGBA as a states-based Bucchi automaton. Is this correct?
On Thu, Oct 20, 2011 at 2:47 PM, Nikos Gorogiannis nikos.gorogiannis@eecs.qmul.ac.uk wrote:
Hello and sorry for the too many questions!
No problem. I probably won't be very reactive in the upcoming days, I just arrived today in Paris after two weeks in Taiwan and I have a lot of catching up to do.
I think I have answered myself w.r.t the complementation algorithms. It seems that safra does what I want.
This would be my best bet, but I'm not very knowledgeable about these algorithms. Guillaume Sadegh, the student who implemented these, is no longer here, however he wrote two detailed technical reports that should be helpful to anyone poking around these algorithms: http://lrde.epita.fr/~sadegh/buchi-complementation-techrep.pdf http://www.lrde.epita.fr/dload//20100106-Seminar/sadegh-spot.pdf
Martin Dieguez Lodeiro (CCed) has sent me some concerns about the Safra implementation in a separate (private) mail a few days ago, but I haven't had the time to investigate. In his tests, computing the Safra complement of
% cat x.tgba acc = "1"; "1", "1", "1",; "1", "2", "p",; "2", "3", "p", "1"; "2", "2", "1",; "3", "3", "p", "1"; "3", "2", "1",;
would return an automaton without any acceptance states, which sounds bogus indeed.
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.
Yet another thing came up: even when I implement the method transition_annotation, the dotty output seems to ignore that. Am I doing something wrong? On the other hand replay_run seems to honour my method.
I think transition_annotation() was originally added to help interpret the counterexamples found while model checking (hence the use in replay-run), but I see no reason not to use it for dotty too. So I would call this a bug.