alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Fix tracking of SCCs on the search stack

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2008-12-11 12:56:34 +01:00
parent c44d6277f2
commit b2f7c2d76d
3 changed files with 34 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,3 +1,13 @@
2008-12-11 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix tracking of SCCs on the search stack.
* src/tgbaalgos/scc.hh (scc::arc_): Rename as ...
(scc::arc_acc_): ... this.
(scc::arc_cond_): New attribute.
* src/tgbaalgos/scc.cc (build_map): Adjust and keep
track of transitions between SCCs on the search stack.
2008-12-10 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc: New files.

29
src/tgbaalgos/scc.cc
View file

@ -99,7 +99,8 @@ namespace spot
scc_num_ = 0;
h_.insert(std::make_pair(init, 1));
root_.push_front(scc(1));
arc_.push(bddfalse);
arc_acc_.push(bddfalse);
arc_cond_.push(bddfalse);
tgba_succ_iterator* iter = aut_->succ_iter(init);
iter->first();
todo_.push(pair_state_iter(init, iter));
@ -107,7 +108,8 @@ namespace spot
while (!todo_.empty())
{
assert(root_.size() == arc_.size());
assert(root_.size() == arc_acc_.size());
assert(root_.size() == arc_cond_.size());
// We are looking at the next successor in SUCC.
tgba_succ_iterator* succ = todo_.top().second;
@ -134,10 +136,18 @@ namespace spot
assert(!root_.empty());
if (root_.front().index == spi->second)
{
assert(!arc_.empty());
arc_.pop();
assert(!arc_acc_.empty());
assert(arc_cond_.size() == arc_acc_.size());
bdd cond = arc_cond_.top();
arc_cond_.pop();
arc_acc_.pop();
relabel_component(--scc_num_);
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));
}
delete succ;
@ -164,7 +174,8 @@ namespace spot
// for later processing.
h_.insert(std::make_pair(dest, ++num_));
root_.push_front(scc(num_));
arc_.push(acc);
arc_acc_.push(acc);
arc_cond_.push(cond);
tgba_succ_iterator* iter = aut_->succ_iter(dest);
iter->first();
todo_.push(pair_state_iter(dest, iter));
@ -203,14 +214,16 @@ namespace spot
while (threshold < root_.front().index)
{
assert(!root_.empty());
assert(!arc_.empty());
assert(!arc_acc_.empty());
assert(arc_acc_.size() == arc_cond_.size());
acc |= root_.front().acc;
acc |= arc_.top();
acc |= arc_acc_.top();
states.splice(states.end(), root_.front().states);
succs.insert(root_.front().succ.begin(),
root_.front().succ.end());
root_.pop_front();
arc_.pop();
arc_acc_.pop();
arc_cond_.pop();
}
// Note that we do not always have
// threshold == root_.front().index

4
src/tgbaalgos/scc.hh
View file

@ -74,7 +74,9 @@ namespace spot
const tgba* aut_; // Automata to decompose.
typedef std::list<scc> stack_type;
stack_type root_; // Stack of SCC roots.
std::stack<bdd> arc_; // A stack of acceptance conditions
std::stack<bdd> arc_acc_; // A stack of acceptance conditions
// between each of these SCC.
std::stack<bdd> arc_cond_; // A stack of conditions
// between each of these SCC.
typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;