16 Jan
2012
16 Jan
'12
3:16 p.m.
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?
17 Jan
17 Jan
3:39 p.m.
Hi Nikos,
On Mon, Jan 16, 2012 at 3:16 PM, Nikos Gorogiannis
<nikos.gorogiannis(a)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
4914
days inactive
4915
days old
1 comments
2 participants
participants (2)
-
Alexandre Duret-Lutz -
Nikos Gorogiannis