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);