Commit 15b3b9e0 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 96a7a49c
2009-05-28 Alexandre Duret-Lutz <adl@lrde.epita.fr>
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 <adl@lrde.epita.fr> 2009-05-28 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Store the scc_map_ as a vector instead of a std::map. There is no Store the scc_map_ as a vector instead of a std::map. There is no
......
...@@ -44,29 +44,26 @@ namespace spot ...@@ -44,29 +44,26 @@ namespace spot
{ {
} }
int unsigned
scc_map::initial() const scc_map::initial() const
{ {
state* in = aut_->get_init_state(); state* in = aut_->get_init_state();
hash_type::const_iterator i = h_.find(in); int val = scc_of_state(in);
assert(i != h_.end());
int val = i->second;
delete in; delete in;
return val; return val;
} }
const scc_map::succ_type& 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); assert(scc_map_.size() > n);
return scc_map_[n].succ; return scc_map_[n].succ;
} }
bool 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* const tgba*
...@@ -82,13 +79,12 @@ namespace spot ...@@ -82,13 +79,12 @@ namespace spot
assert(!root_.front().states.empty()); assert(!root_.front().states.empty());
std::list<const state*>::iterator i; std::list<const state*>::iterator i;
int n = scc_map_.size(); int n = scc_map_.size();
n = -n - 1;
for (i = root_.front().states.begin(); i != root_.front().states.end(); ++i) for (i = root_.front().states.begin(); i != root_.front().states.end(); ++i)
{ {
hash_type::iterator spi = h_.find(*i); hash_type::iterator spi = h_.find(*i);
assert(spi != h_.end()); assert(spi != h_.end());
assert(spi->first == *i); assert(spi->first == *i);
assert(spi->second > 0); assert(spi->second < 0);
spi->second = n; spi->second = n;
} }
scc_map_.push_back(root_.front()); scc_map_.push_back(root_.front());
...@@ -101,9 +97,9 @@ namespace spot ...@@ -101,9 +97,9 @@ namespace spot
// Setup depth-first search from the initial state. // Setup depth-first search from the initial state.
{ {
state* init = aut_->get_init_state(); state* init = aut_->get_init_state();
num_ = 1; num_ = -1;
h_.insert(std::make_pair(init, 1)); h_.insert(std::make_pair(init, num_));
root_.push_front(scc(1)); root_.push_front(scc(num_));
arc_acc_.push(bddfalse); arc_acc_.push(bddfalse);
arc_cond_.push(bddfalse); arc_cond_.push(bddfalse);
tgba_succ_iterator* iter = aut_->succ_iter(init); tgba_succ_iterator* iter = aut_->succ_iter(init);
...@@ -176,7 +172,7 @@ namespace spot ...@@ -176,7 +172,7 @@ namespace spot
{ {
// Yes. Number it, stack it, and register its successors // Yes. Number it, stack it, and register its successors
// for later processing. // for later processing.
h_.insert(std::make_pair(dest, ++num_)); h_.insert(std::make_pair(dest, --num_));
root_.push_front(scc(num_)); root_.push_front(scc(num_));
arc_acc_.push(acc); arc_acc_.push(acc);
arc_cond_.push(cond); arc_cond_.push(cond);
...@@ -187,7 +183,7 @@ namespace spot ...@@ -187,7 +183,7 @@ namespace spot
} }
// Have we reached a maximal SCC? // Have we reached a maximal SCC?
if (spi->second < 0) if (spi->second >= 0)
{ {
int dest = spi->second; int dest = spi->second;
// Record that there is a transition from this SCC to the // Record that there is a transition from this SCC to the
...@@ -209,15 +205,15 @@ namespace spot ...@@ -209,15 +205,15 @@ namespace spot
// this S1 and S2 into this SCC. // this S1 and S2 into this SCC.
// //
// This merge is easy to do because the order of the SCC in // 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 // ROOT is descending: we just have to merge all SCCs from the
// top of ROOT that have an index greater to the one of // top of ROOT that have an index lesser than the one of
// the SCC of S2 (called the "threshold"). // the SCC of S2 (called the "threshold").
int threshold = spi->second; int threshold = spi->second;
std::list<const state*> states; std::list<const state*> states;
succ_type succs; succ_type succs;
cond_set conds; cond_set conds;
conds.insert(cond); conds.insert(cond);
while (threshold < root_.front().index) while (threshold > root_.front().index)
{ {
assert(!root_.empty()); assert(!root_.empty());
assert(!arc_acc_.empty()); assert(!arc_acc_.empty());
...@@ -238,7 +234,7 @@ namespace spot ...@@ -238,7 +234,7 @@ namespace spot
// Note that we do not always have // Note that we do not always have
// threshold == root_.front().index // threshold == root_.front().index
// after this loop, the SCC whose index is threshold might have // 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 // Accumulate all acceptance conditions, states, SCC
// successors, and conditions into the merged SCC. // successors, and conditions into the merged SCC.
...@@ -249,30 +245,27 @@ namespace spot ...@@ -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); hash_type::const_iterator i = h_.find(s);
assert(i != h_.end()); assert(i != h_.end());
return i->second; 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); assert(scc_map_.size() > n);
return scc_map_[n].conds; 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); assert(scc_map_.size() > n);
return scc_map_[n].acc; return scc_map_[n].acc;
} }
const std::list<const state*>& scc_map::states_of(int i) const const std::list<const state*>& scc_map::states_of(unsigned n) const
{ {
unsigned n = -i - 1;
assert(scc_map_.size() > n); assert(scc_map_.size() > n);
return scc_map_[n].states; return scc_map_[n].states;
} }
...@@ -363,9 +356,9 @@ namespace spot ...@@ -363,9 +356,9 @@ namespace spot
std::ostream& std::ostream&
dump_scc_dot(const scc_map& m, std::ostream& out, bool verbose) 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(); int start = m.initial();
out << " 0 -> " << -start << std::endl; out << " i -> " << start << std::endl;
typedef std::set<int> seen_map; typedef std::set<int> seen_map;
seen_map seen; seen_map seen;
...@@ -381,7 +374,7 @@ namespace spot ...@@ -381,7 +374,7 @@ namespace spot
const scc_map::cond_set& cs = m.cond_set_of(state); const scc_map::cond_set& cs = m.cond_set_of(state);
std::ostringstream ostr; std::ostringstream ostr;
ostr << -state; ostr << state;
if (verbose) if (verbose)
{ {
size_t n = m.states_of(state).size(); size_t n = m.states_of(state).size();
...@@ -402,7 +395,7 @@ namespace spot ...@@ -402,7 +395,7 @@ namespace spot
ostr << "]"; ostr << "]";
} }
std::cout << " " << -state << " [shape=box," std::cout << " " << state << " [shape=box,"
<< (m.accepting(state) ? "style=bold," : "") << (m.accepting(state) ? "style=bold," : "")
<< "label=\"" << ostr.str() << "\"]" << std::endl; << "label=\"" << ostr.str() << "\"]" << std::endl;
...@@ -414,7 +407,7 @@ namespace spot ...@@ -414,7 +407,7 @@ namespace spot
int dest = it->first; int dest = it->first;
bdd label = it->second; bdd label = it->second;
out << " " << -state << " -> " << -dest out << " " << state << " -> " << dest
<< " [label=\""; << " [label=\"";
bdd_print_formula(out, m.get_aut()->get_dict(), label); bdd_print_formula(out, m.get_aut()->get_dict(), label);
out << "\"]" << std::endl; out << "\"]" << std::endl;
......
...@@ -60,29 +60,31 @@ namespace spot ...@@ -60,29 +60,31 @@ namespace spot
class scc_map class scc_map
{ {
public: public:
typedef std::map<int, bdd> succ_type; typedef std::map<unsigned, bdd> succ_type;
typedef std::set<bdd, bdd_less_than> cond_set; typedef std::set<bdd, bdd_less_than> cond_set;
scc_map(const tgba* aut); scc_map(const tgba* aut);
void build_map(); 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<const state*>& states_of(int n) const;
const tgba* get_aut() const; const tgba* get_aut() const;
unsigned scc_count() const; unsigned scc_count() const;
int initial() const; unsigned initial() 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<const state*>& states_of(unsigned n) const;
const succ_type& succ(int i) const; unsigned scc_of_state(const state* s) const;
bool accepting(int i) const;
protected: protected:
int relabel_component();
struct scc struct scc
{ {
public: public:
...@@ -109,8 +111,11 @@ namespace spot ...@@ -109,8 +111,11 @@ namespace spot
// between each of these SCC. // between each of these SCC.
typedef Sgi::hash_map<const state*, int, typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type; state_ptr_hash, state_ptr_equal> hash_type;
hash_type h_; // Map of visited states. hash_type h_; // Map of visited states. Values >= 0
int num_; // Number of visited nodes. // 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<const spot::state*, tgba_succ_iterator*> pair_state_iter; typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
std::stack<pair_state_iter> todo_; // DFS stack. Holds (STATE, std::stack<pair_state_iter> todo_; // DFS stack. Holds (STATE,
// ITERATOR) pairs where // ITERATOR) pairs where
...@@ -124,7 +129,7 @@ namespace spot ...@@ -124,7 +129,7 @@ namespace spot
typedef std::vector<scc> scc_map_type; typedef std::vector<scc> scc_map_type;
scc_map_type scc_map_; // Map of constructed maximal SCC. scc_map_type scc_map_; // Map of constructed maximal SCC.
// SCC number "n" in H_ corresponds to entry // 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); scc_stats build_scc_stats(const tgba* a);
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment