From 96a7a49c52a0e2362993f09b5e9c3008ee9d46dc Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 28 May 2009 13:32:36 +0200 Subject: [PATCH] Store the scc_map_ as a vector instead of a std::map. There is no point in using a map since the SCC are numbered in sequence. * src/tgbaalgos/scc.hh (scc_map::relabel_component): Return the number of the SCC instead of taking it as argument. (scc_map::scc_num_): Delete this variable. scc_map_.size() gives the same information. (scc_map::scc_map_type): Define using std::vector instead of std::map. * src/tgbaalgos/scc.cc: Adjust all uses. --- ChangeLog | 13 ++++++++++++ src/tgbaalgos/scc.cc | 49 +++++++++++++++++++++++--------------------- src/tgbaalgos/scc.hh | 11 +++++----- 3 files changed, 45 insertions(+), 28 deletions(-) diff --git a/ChangeLog b/ChangeLog index cb8a4baaa..0758901de 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2009-05-28 Alexandre Duret-Lutz + + Store the scc_map_ as a vector instead of a std::map. There is no + point in using a map since the SCC are numbered in sequence. + + * src/tgbaalgos/scc.hh (scc_map::relabel_component): Return the + number of the SCC instead of taking it as argument. + (scc_map::scc_num_): Delete this variable. scc_map_.size() gives + the same information. + (scc_map::scc_map_type): Define using std::vector instead of + std::map. + * src/tgbaalgos/scc.cc: Adjust all uses. + 2009-05-28 Alexandre Duret-Lutz Keep track of conditions in SCC, and add a more verbose dump. diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 941883846..c92e3a482 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -58,17 +58,15 @@ namespace spot const scc_map::succ_type& scc_map::succ(int i) const { - std::map::const_iterator j = scc_map_.find(i); - assert (j != scc_map_.end()); - return j->second.succ; + unsigned n = -i - 1; + assert(scc_map_.size() > n); + return scc_map_[n].succ; } bool scc_map::accepting(int i) const { - std::map::const_iterator j = scc_map_.find(i); - assert (j != scc_map_.end()); - return j->second.acc == aut_->all_acceptance_conditions(); + return acc_set_of(i) == aut_->all_acceptance_conditions(); } const tgba* @@ -78,11 +76,13 @@ namespace spot } - void - scc_map::relabel_component(int n) + int + scc_map::relabel_component() { assert(!root_.front().states.empty()); std::list::iterator i; + int n = scc_map_.size(); + n = -n - 1; for (i = root_.front().states.begin(); i != root_.front().states.end(); ++i) { hash_type::iterator spi = h_.find(*i); @@ -91,7 +91,8 @@ namespace spot assert(spi->second > 0); spi->second = n; } - scc_map_.insert(std::make_pair(n, root_.front())); + scc_map_.push_back(root_.front()); + return n; } void @@ -101,7 +102,6 @@ namespace spot { state* init = aut_->get_init_state(); num_ = 1; - scc_num_ = 0; h_.insert(std::make_pair(init, 1)); root_.push_front(scc(1)); arc_acc_.push(bddfalse); @@ -146,13 +146,13 @@ namespace spot bdd cond = arc_cond_.top(); arc_cond_.pop(); arc_acc_.pop(); - relabel_component(--scc_num_); + int num = relabel_component(); root_.pop_front(); // Record the transition between the SCC being popped // and the previous SCC. if (!root_.empty()) - root_.front().succ.insert(std::make_pair(scc_num_, cond)); + root_.front().succ.insert(std::make_pair(num, cond)); } delete succ; @@ -256,27 +256,30 @@ namespace spot return i->second; } - const scc_map::cond_set& scc_map::cond_set_of(int n) const + const scc_map::cond_set& scc_map::cond_set_of(int i) const { - scc_map_type::const_iterator i = scc_map_.find(n); - return i->second.conds; + unsigned n = -i - 1; + assert(scc_map_.size() > n); + return scc_map_[n].conds; } - bdd scc_map::acc_set_of(int n) const + bdd scc_map::acc_set_of(int i) const { - scc_map_type::const_iterator i = scc_map_.find(n); - return i->second.acc; + unsigned n = -i - 1; + assert(scc_map_.size() > n); + return scc_map_[n].acc; } - const std::list& scc_map::states_of(int n) const + const std::list& scc_map::states_of(int i) const { - scc_map_type::const_iterator i = scc_map_.find(n); - return i->second.states; + unsigned n = -i - 1; + assert(scc_map_.size() > n); + return scc_map_[n].states; } - int scc_map::scc_count() const + unsigned scc_map::scc_count() const { - return -scc_num_; + return scc_map_.size(); } namespace diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index 02ff0d9d1..f41dca788 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -23,6 +23,7 @@ #include #include +#include #include "tgba/tgba.hh" #include #include "misc/hash.hh" @@ -65,7 +66,7 @@ namespace spot scc_map(const tgba* aut); void build_map(); - void relabel_component(int n); + int relabel_component(); int scc_of_state(const state* s) const; const cond_set& cond_set_of(int n) const; @@ -74,7 +75,7 @@ namespace spot const tgba* get_aut() const; - int scc_count() const; + unsigned scc_count() const; int initial() const; @@ -110,8 +111,6 @@ namespace spot state_ptr_hash, state_ptr_equal> hash_type; hash_type h_; // Map of visited states. int num_; // Number of visited nodes. - int scc_num_; // Opposite of the number of - // maximal SCC constructed. typedef std::pair pair_state_iter; std::stack todo_; // DFS stack. Holds (STATE, // ITERATOR) pairs where @@ -122,8 +121,10 @@ namespace spot // but STATE should not because // it is used as a key in H. - typedef std::map scc_map_type; + typedef std::vector scc_map_type; scc_map_type scc_map_; // Map of constructed maximal SCC. + // SCC number "n" in H_ corresponds to entry + // "-n-1" in SCC_MAP_. }; scc_stats build_scc_stats(const tgba* a);