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.
This commit is contained in:
parent
07ead6134e
commit
96a7a49c52
3 changed files with 45 additions and 28 deletions
13
ChangeLog
13
ChangeLog
|
|
@ -1,3 +1,16 @@
|
||||||
|
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
|
||||||
|
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 <adl@lrde.epita.fr>
|
2009-05-28 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
Keep track of conditions in SCC, and add a more verbose dump.
|
Keep track of conditions in SCC, and add a more verbose dump.
|
||||||
|
|
|
||||||
|
|
@ -58,17 +58,15 @@ namespace spot
|
||||||
const scc_map::succ_type&
|
const scc_map::succ_type&
|
||||||
scc_map::succ(int i) const
|
scc_map::succ(int i) const
|
||||||
{
|
{
|
||||||
std::map<int, scc>::const_iterator j = scc_map_.find(i);
|
unsigned n = -i - 1;
|
||||||
assert (j != scc_map_.end());
|
assert(scc_map_.size() > n);
|
||||||
return j->second.succ;
|
return scc_map_[n].succ;
|
||||||
}
|
}
|
||||||
|
|
||||||
bool
|
bool
|
||||||
scc_map::accepting(int i) const
|
scc_map::accepting(int i) const
|
||||||
{
|
{
|
||||||
std::map<int, scc>::const_iterator j = scc_map_.find(i);
|
return acc_set_of(i) == aut_->all_acceptance_conditions();
|
||||||
assert (j != scc_map_.end());
|
|
||||||
return j->second.acc == aut_->all_acceptance_conditions();
|
|
||||||
}
|
}
|
||||||
|
|
||||||
const tgba*
|
const tgba*
|
||||||
|
|
@ -78,11 +76,13 @@ namespace spot
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
void
|
int
|
||||||
scc_map::relabel_component(int n)
|
scc_map::relabel_component()
|
||||||
{
|
{
|
||||||
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();
|
||||||
|
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);
|
||||||
|
|
@ -91,7 +91,8 @@ namespace spot
|
||||||
assert(spi->second > 0);
|
assert(spi->second > 0);
|
||||||
spi->second = n;
|
spi->second = n;
|
||||||
}
|
}
|
||||||
scc_map_.insert(std::make_pair(n, root_.front()));
|
scc_map_.push_back(root_.front());
|
||||||
|
return n;
|
||||||
}
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
|
|
@ -101,7 +102,6 @@ namespace spot
|
||||||
{
|
{
|
||||||
state* init = aut_->get_init_state();
|
state* init = aut_->get_init_state();
|
||||||
num_ = 1;
|
num_ = 1;
|
||||||
scc_num_ = 0;
|
|
||||||
h_.insert(std::make_pair(init, 1));
|
h_.insert(std::make_pair(init, 1));
|
||||||
root_.push_front(scc(1));
|
root_.push_front(scc(1));
|
||||||
arc_acc_.push(bddfalse);
|
arc_acc_.push(bddfalse);
|
||||||
|
|
@ -146,13 +146,13 @@ namespace spot
|
||||||
bdd cond = arc_cond_.top();
|
bdd cond = arc_cond_.top();
|
||||||
arc_cond_.pop();
|
arc_cond_.pop();
|
||||||
arc_acc_.pop();
|
arc_acc_.pop();
|
||||||
relabel_component(--scc_num_);
|
int num = relabel_component();
|
||||||
root_.pop_front();
|
root_.pop_front();
|
||||||
|
|
||||||
// Record the transition between the SCC being popped
|
// Record the transition between the SCC being popped
|
||||||
// and the previous SCC.
|
// and the previous SCC.
|
||||||
if (!root_.empty())
|
if (!root_.empty())
|
||||||
root_.front().succ.insert(std::make_pair(scc_num_, cond));
|
root_.front().succ.insert(std::make_pair(num, cond));
|
||||||
}
|
}
|
||||||
|
|
||||||
delete succ;
|
delete succ;
|
||||||
|
|
@ -256,27 +256,30 @@ namespace spot
|
||||||
return i->second;
|
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);
|
unsigned n = -i - 1;
|
||||||
return i->second.conds;
|
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);
|
unsigned n = -i - 1;
|
||||||
return i->second.acc;
|
assert(scc_map_.size() > n);
|
||||||
|
return scc_map_[n].acc;
|
||||||
}
|
}
|
||||||
|
|
||||||
const std::list<const state*>& scc_map::states_of(int n) const
|
const std::list<const state*>& scc_map::states_of(int i) const
|
||||||
{
|
{
|
||||||
scc_map_type::const_iterator i = scc_map_.find(n);
|
unsigned n = -i - 1;
|
||||||
return i->second.states;
|
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
|
namespace
|
||||||
|
|
|
||||||
|
|
@ -23,6 +23,7 @@
|
||||||
|
|
||||||
#include <map>
|
#include <map>
|
||||||
#include <stack>
|
#include <stack>
|
||||||
|
#include <vector>
|
||||||
#include "tgba/tgba.hh"
|
#include "tgba/tgba.hh"
|
||||||
#include <iosfwd>
|
#include <iosfwd>
|
||||||
#include "misc/hash.hh"
|
#include "misc/hash.hh"
|
||||||
|
|
@ -65,7 +66,7 @@ namespace spot
|
||||||
scc_map(const tgba* aut);
|
scc_map(const tgba* aut);
|
||||||
|
|
||||||
void build_map();
|
void build_map();
|
||||||
void relabel_component(int n);
|
int relabel_component();
|
||||||
|
|
||||||
int scc_of_state(const state* s) const;
|
int scc_of_state(const state* s) const;
|
||||||
const cond_set& cond_set_of(int n) const;
|
const cond_set& cond_set_of(int n) const;
|
||||||
|
|
@ -74,7 +75,7 @@ namespace spot
|
||||||
|
|
||||||
const tgba* get_aut() const;
|
const tgba* get_aut() const;
|
||||||
|
|
||||||
int scc_count() const;
|
unsigned scc_count() const;
|
||||||
|
|
||||||
int initial() const;
|
int initial() const;
|
||||||
|
|
||||||
|
|
@ -110,8 +111,6 @@ namespace spot
|
||||||
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.
|
||||||
int num_; // Number of visited nodes.
|
int num_; // Number of visited nodes.
|
||||||
int scc_num_; // Opposite of the number of
|
|
||||||
// maximal SCC constructed.
|
|
||||||
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
|
||||||
|
|
@ -122,8 +121,10 @@ namespace spot
|
||||||
// but STATE should not because
|
// but STATE should not because
|
||||||
// it is used as a key in H.
|
// it is used as a key in H.
|
||||||
|
|
||||||
typedef std::map<int, 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
|
||||||
|
// "-n-1" in SCC_MAP_.
|
||||||
};
|
};
|
||||||
|
|
||||||
scc_stats build_scc_stats(const tgba* a);
|
scc_stats build_scc_stats(const tgba* a);
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue