From 578c5894f50fc51b264efcff849980a593b04610 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 17 Jan 2012 18:07:47 +0100 Subject: [PATCH] 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. --- ChangeLog | 9 +++++++++ src/tgba/tgbasafracomplement.cc | 22 +++++++++++----------- 2 files changed, 20 insertions(+), 11 deletions(-) diff --git a/ChangeLog b/ChangeLog index 9b361ab73..bb598aa5f 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,12 @@ +2012-01-17 Alexandre Duret-Lutz + + 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 * src/eltlparse/eltlparse.yy (realias): Add a useless return to diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index 921f7c126..224044faa 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // 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) { - if (cache_transition.find(*i) == cache_transition.end()) + cache_t::const_iterator it = cache_transition.find(*i); + if (it == cache_transition.end()) 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(); t_it != transitions.end(); ++t_it) @@ -403,18 +404,17 @@ namespace spot subset_t::iterator node_it = (*child_it)->nodes.begin(); 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; (*child_it)->remove_node_from_children(*node_it); (*child_it)->nodes.erase(node_it++); s->destroy(); } - else - { - node_set.insert(*node_it); - ++node_it; - } + else + { + ++node_it; + } } (*child_it)->normalize_siblings();