alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Minor speedups in tgba_safra_complement().

Browse source 
* src/tgba/tgbasafracomplement.cc (safra_tree:succ_create): Do not
lookup *i twice, and do not copy it->second.
(safra_tree::normalize_siblings): Do not lookup *node_it before
insertion.
This commit is contained in:
Alexandre Duret-Lutz 2012-01-17 18:07:47 +01:00
parent ebfec98e31
commit 578c5894f5
2 changed files with 20 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,3 +1,12 @@
2012-01-17 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Minor speedups in tgba_safra_complement().
* src/tgba/tgbasafracomplement.cc (safra_tree:succ_create): Do not
lookup *i twice, and do not copy it->second.
(safra_tree::normalize_siblings): Do not lookup *node_it before
insertion.
2012-01-18 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2012-01-18 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/eltlparse/eltlparse.yy (realias): Add a useless return to * src/eltlparse/eltlparse.yy (realias): Add a useless return to

22
src/tgba/tgbasafracomplement.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -362,10 +362,11 @@ namespace spot
for (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i) for (subset_t::iterator i = nodes.begin(); i != nodes.end(); ++i)
{ {
if (cache_transition.find(*i) == cache_transition.end()) cache_t::const_iterator it = cache_transition.find(*i);
if (it == cache_transition.end())
continue; continue;
tr_cache_t transitions = cache_transition[*i]; const tr_cache_t& transitions = it->second;
for (tr_cache_t::const_iterator t_it = transitions.begin(); for (tr_cache_t::const_iterator t_it = transitions.begin();
t_it != transitions.end(); t_it != transitions.end();
++t_it) ++t_it)
@ -403,18 +404,17 @@ namespace spot
subset_t::iterator node_it = (*child_it)->nodes.begin(); subset_t::iterator node_it = (*child_it)->nodes.begin();
while (node_it != (*child_it)->nodes.end()) while (node_it != (*child_it)->nodes.end())
{ {
if (node_set.find(*node_it) != node_set.end()) if (!node_set.insert(*node_it).second)
{ {
const state* s = *node_it; const state* s = *node_it;
(*child_it)->remove_node_from_children(*node_it); (*child_it)->remove_node_from_children(*node_it);
(*child_it)->nodes.erase(node_it++); (*child_it)->nodes.erase(node_it++);
s->destroy(); s->destroy();
} }
else else
{ {
node_set.insert(*node_it); ++node_it;
++node_it; }
}
} }
(*child_it)->normalize_siblings(); (*child_it)->normalize_siblings();