Hi Alexandre,
I have some code that uses the standard pattern for checking language inclusion between two automata, using tgba_safra_complementation. The automata have a small number of states (<100) and one acceptance condition.
Running my code under valgrind for time profiling reveals a curious time distribution: 30% of the execution time is spent in malloc and free (20%/10% resp). The call hierarchy is as follows:
malloc/free <- operator new/delete <- tgba_tba_proxy::succ_iter <- tgba_sba_proxy ctor <- safra_determinisation::create_safra_automaton <- tgba_safra_complement
I have eliminated the contribution of my code to the run time of malloc and free (basically by avoiding creating and destroying the same states repeatedly through memoizing).
Is there any workaround to this, i.e., could better/different memory management eliminate this 30% of overhead? Are other complementation algorithms better for this use-case?
Best regards Nikos
PS What is the preferred way of referencing Spot in a publication?
Hi Nikos,
On Mon, Jan 16, 2012 at 3:16 PM, Nikos Gorogiannis nikos.gorogiannis@eecs.qmul.ac.uk wrote:
I have some code that uses the standard pattern for checking language inclusion between two automata, using tgba_safra_complementation. The automata have a small number of states (<100) and one acceptance condition.
Running my code under valgrind for time profiling reveals a curious time distribution: 30% of the execution time is spent in malloc and free (20%/10% resp). The call hierarchy is as follows:
malloc/free <- operator new/delete <- tgba_tba_proxy::succ_iter <- tgba_sba_proxy ctor <- safra_determinisation::create_safra_automaton <- tgba_safra_complement
Safra complementation works only for classical Büchi automata, so the first thing tgba_safra_complement does is degeneralize the TGBA to be sure it is working on a "BA". This degeneralization is unfortunately performed on-the-fly by tgba_[st]ba_proxy. It would be more efficient to degeneralize the automaton first, and then browse the resulting automaton, but we don't have such an off-line degeneralization right now in Spot.
In your case, you said that the input had only one acceptance condition. Does this corresponds to a Büchi automaton (i.e., all outgoing transitions of a state are either accepting or not) ? It might be possible to specialize the tgba_safra_complement routine for such automata, bypassing any degeneralization.
I don't have any other idea for this. I wish I could understand Safra enough to write a version that works directly on TGBA (without degeneralization), but it is still black magic to me. Also the implementation for the other algorithm (the KV complementation) is a lot less efficient anyway.
PS What is the preferred way of referencing Spot in a publication?
You can cite this paper for a general introduction to the library: http://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.04.mascots And this VECOS'11 paper for LTL translation: http://www.lrde.epita.fr/~adl/dl/adl_bib.html#duret.11.vecos
That Mascots paper is getting old; we should probably try to publish a more up-to-date tool paper somewhere about what the library is now offering and how it has been used. (I'm curious about what you are actually building, by the way, and longing to read any paper you will publish on that subject. I know of very few people who have actually used Spot as a library, and not just as a command-line tool to translate LTL formulae.)
Best regards
-
Alexandre Duret-Lutz -
Nikos Gorogiannis