From 15b3b9e07db3e9ba7a6e78f3eb52889404923e5d Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 28 May 2009 14:02:42 +0200 Subject: [PATCH] Number states using negative values and SCCs using nonnegative values. Before this change states were numbered using positive values and SCCs using negative values. That meant the user had to work with negative values. With this changes, the nonnegative values used to label SCCs can also directly be used as index in the scc_map_. * src/tgbaalgos/scc.hh (scc_map::scc_of_state, scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of, scc_map::initial, scc_map::scc_type, scc_map::succ, scc_map::accepting): Adjust prototypes to take or return unsigned arguments. * src/tgbaalgos/scc.cc: Adjust prototypes of the above functions. (scc_map::build_map, scc_map::relabel_component): Number states using negative values, and SCCs using nonnegative values. (dump_scc_dot): Adjust to use nonnegative values. --- ChangeLog | 20 ++++++++++++++++ src/tgbaalgos/scc.cc | 55 +++++++++++++++++++------------------------- src/tgbaalgos/scc.hh | 31 ++++++++++++++----------- 3 files changed, 62 insertions(+), 44 deletions(-) diff --git a/ChangeLog b/ChangeLog index 0758901de..f90fc2c77 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,23 @@ +2009-05-28 Alexandre Duret-Lutz + + Number states using negative values and SCCs using nonnegative + values. + + Before this change states were numbered using positive values and + SCCs using negative values. That meant the user had to work with + negative values. With this changes, the nonnegative values used + to label SCCs can also directly be used as index in the scc_map_. + + * src/tgbaalgos/scc.hh (scc_map::scc_of_state, + scc_map::cond_set_of, scc_map::acc_set_of, scc_map::states_of, + scc_map::initial, scc_map::scc_type, scc_map::succ, + scc_map::accepting): Adjust prototypes to take or return unsigned + arguments. + * src/tgbaalgos/scc.cc: Adjust prototypes of the above functions. + (scc_map::build_map, scc_map::relabel_component): Number states + using negative values, and SCCs using nonnegative values. + (dump_scc_dot): Adjust to use nonnegative values. + 2009-05-28 Alexandre Duret-Lutz Store the scc_map_ as a vector instead of a std::map. There is no diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index c92e3a482..c05c1409e 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -44,29 +44,26 @@ namespace spot { } - int + unsigned scc_map::initial() const { state* in = aut_->get_init_state(); - hash_type::const_iterator i = h_.find(in); - assert(i != h_.end()); - int val = i->second; + int val = scc_of_state(in); delete in; return val; } const scc_map::succ_type& - scc_map::succ(int i) const + scc_map::succ(unsigned n) const { - unsigned n = -i - 1; assert(scc_map_.size() > n); return scc_map_[n].succ; } bool - scc_map::accepting(int i) const + scc_map::accepting(unsigned n) const { - return acc_set_of(i) == aut_->all_acceptance_conditions(); + return acc_set_of(n) == aut_->all_acceptance_conditions(); } const tgba* @@ -82,13 +79,12 @@ namespace spot 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); assert(spi != h_.end()); assert(spi->first == *i); - assert(spi->second > 0); + assert(spi->second < 0); spi->second = n; } scc_map_.push_back(root_.front()); @@ -101,9 +97,9 @@ namespace spot // Setup depth-first search from the initial state. { state* init = aut_->get_init_state(); - num_ = 1; - h_.insert(std::make_pair(init, 1)); - root_.push_front(scc(1)); + num_ = -1; + h_.insert(std::make_pair(init, num_)); + root_.push_front(scc(num_)); arc_acc_.push(bddfalse); arc_cond_.push(bddfalse); tgba_succ_iterator* iter = aut_->succ_iter(init); @@ -176,7 +172,7 @@ namespace spot { // Yes. Number it, stack it, and register its successors // for later processing. - h_.insert(std::make_pair(dest, ++num_)); + h_.insert(std::make_pair(dest, --num_)); root_.push_front(scc(num_)); arc_acc_.push(acc); arc_cond_.push(cond); @@ -187,7 +183,7 @@ namespace spot } // Have we reached a maximal SCC? - if (spi->second < 0) + if (spi->second >= 0) { int dest = spi->second; // Record that there is a transition from this SCC to the @@ -209,15 +205,15 @@ namespace spot // this S1 and S2 into this SCC. // // This merge is easy to do because the order of the SCC in - // ROOT is ascending: we just have to merge all SCCs from the - // top of ROOT that have an index greater to the one of + // ROOT is descending: we just have to merge all SCCs from the + // top of ROOT that have an index lesser than the one of // the SCC of S2 (called the "threshold"). int threshold = spi->second; std::list states; succ_type succs; cond_set conds; conds.insert(cond); - while (threshold < root_.front().index) + while (threshold > root_.front().index) { assert(!root_.empty()); assert(!arc_acc_.empty()); @@ -238,7 +234,7 @@ namespace spot // Note that we do not always have // threshold == root_.front().index // after this loop, the SCC whose index is threshold might have - // been merged with a lower SCC. + // been merged with a higher SCC. // Accumulate all acceptance conditions, states, SCC // successors, and conditions into the merged SCC. @@ -249,30 +245,27 @@ namespace spot } } - int scc_map::scc_of_state(const state* s) const + unsigned scc_map::scc_of_state(const state* s) const { hash_type::const_iterator i = h_.find(s); assert(i != h_.end()); return i->second; } - const scc_map::cond_set& scc_map::cond_set_of(int i) const + const scc_map::cond_set& scc_map::cond_set_of(unsigned n) const { - unsigned n = -i - 1; assert(scc_map_.size() > n); return scc_map_[n].conds; } - bdd scc_map::acc_set_of(int i) const + bdd scc_map::acc_set_of(unsigned n) const { - unsigned n = -i - 1; assert(scc_map_.size() > n); return scc_map_[n].acc; } - const std::list& scc_map::states_of(int i) const + const std::list& scc_map::states_of(unsigned n) const { - unsigned n = -i - 1; assert(scc_map_.size() > n); return scc_map_[n].states; } @@ -363,9 +356,9 @@ namespace spot std::ostream& dump_scc_dot(const scc_map& m, std::ostream& out, bool verbose) { - out << "digraph G {\n 0 [label=\"\", style=invis, height=0]" << std::endl; + out << "digraph G {\n i [label=\"\", style=invis, height=0]" << std::endl; int start = m.initial(); - out << " 0 -> " << -start << std::endl; + out << " i -> " << start << std::endl; typedef std::set seen_map; seen_map seen; @@ -381,7 +374,7 @@ namespace spot const scc_map::cond_set& cs = m.cond_set_of(state); std::ostringstream ostr; - ostr << -state; + ostr << state; if (verbose) { size_t n = m.states_of(state).size(); @@ -402,7 +395,7 @@ namespace spot ostr << "]"; } - std::cout << " " << -state << " [shape=box," + std::cout << " " << state << " [shape=box," << (m.accepting(state) ? "style=bold," : "") << "label=\"" << ostr.str() << "\"]" << std::endl; @@ -414,7 +407,7 @@ namespace spot int dest = it->first; bdd label = it->second; - out << " " << -state << " -> " << -dest + out << " " << state << " -> " << dest << " [label=\""; bdd_print_formula(out, m.get_aut()->get_dict(), label); out << "\"]" << std::endl; diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index f41dca788..1f806590c 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -60,29 +60,31 @@ namespace spot class scc_map { public: - typedef std::map succ_type; + typedef std::map succ_type; typedef std::set cond_set; scc_map(const tgba* aut); void build_map(); - int relabel_component(); - - int scc_of_state(const state* s) const; - const cond_set& cond_set_of(int n) const; - bdd acc_set_of(int n) const; - const std::list& states_of(int n) const; const tgba* get_aut() const; unsigned scc_count() const; - int initial() const; + unsigned initial() const; - const succ_type& succ(int i) const; - bool accepting(int i) const; + const succ_type& succ(unsigned n) const; + bool accepting(unsigned n) const; + const cond_set& cond_set_of(unsigned n) const; + bdd acc_set_of(unsigned n) const; + const std::list& states_of(unsigned n) const; + + unsigned scc_of_state(const state* s) const; protected: + + int relabel_component(); + struct scc { public: @@ -109,8 +111,11 @@ namespace spot // between each of these SCC. typedef Sgi::hash_map hash_type; - hash_type h_; // Map of visited states. - int num_; // Number of visited nodes. + hash_type h_; // Map of visited states. Values >= 0 + // designate maximal SCC. Values < 0 + // number states that are part of + // incomplete SCCs being completed. + int num_; // Number of visited nodes, negated. typedef std::pair pair_state_iter; std::stack todo_; // DFS stack. Holds (STATE, // ITERATOR) pairs where @@ -124,7 +129,7 @@ namespace spot 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_. + // "n" in SCC_MAP_. }; scc_stats build_scc_stats(const tgba* a);