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

* src/tgbaalgos/emptiness_stats.hh (ec_statistics::depth): New function.

Browse source 
* src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::clear_todo,
couvreur99_check_shy::check): Count all successors in the
todo stack rather than all items on the stack.
This commit is contained in:
Alexandre Duret-Lutz 2005-01-17 18:48:59 +00:00
parent addb3a30cd
commit 2604b27008
2 changed files with 16 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/tgbaalgos/emptiness_stats.hh
View file

@ -60,17 +60,17 @@ namespace spot
} }
void void
inc_depth() inc_depth(int n = 1)
{ {
++depth_; depth_ += n;
if (depth_ > max_depth_) if (depth_ > max_depth_)
max_depth_ = depth_; max_depth_ = depth_;
} }
void void
dec_depth() dec_depth(int n = 1)
{ {
--depth_; depth_ -= n;
} }
int int
@ -91,6 +91,12 @@ namespace spot
return max_depth_; return max_depth_;
} }
int
depth() const
{
return depth_;
}
private : private :
unsigned states_; /// number of disctint visited states unsigned states_; /// number of disctint visited states
unsigned transitions_; /// number of visited transitions unsigned transitions_; /// number of visited transitions

11
src/tgbaalgos/gtec/gtec.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
@ -292,9 +292,10 @@ namespace spot
if (spi.first == 0) if (spi.first == 0)
delete q->s; delete q->s;
} }
dec_depth(todo.back().q.size());
todo.pop_back(); todo.pop_back();
dec_depth();
} }
assert(depth() == 0);
} }
emptiness_check_result* emptiness_check_result*
@ -316,7 +317,6 @@ namespace spot
int index = todo.back().n; int index = todo.back().n;
// Backtrack TODO. // Backtrack TODO.
todo.pop_back(); todo.pop_back();
dec_depth();
if (todo.empty()) if (todo.empty())
{ {
// This automaton recognizes no word. // This automaton recognizes no word.
@ -341,6 +341,7 @@ namespace spot
// Pick one successor off the list. // Pick one successor off the list.
successor succ = queue.front(); successor succ = queue.front();
queue.pop_front(); queue.pop_front();
dec_depth();
int& n = ecs_->h->index_and_insert(succ.s); int& n = ecs_->h->index_and_insert(succ.s);
// Skip dead states. // Skip dead states.
@ -373,7 +374,6 @@ namespace spot
ecs_->root.push(num); ecs_->root.push(num);
arc.push(succ.acc); arc.push(succ.acc);
todo.push_back(todo_item(succ.s, num)); todo.push_back(todo_item(succ.s, num));
inc_depth();
succ_queue* new_queue = &todo.back().q; succ_queue* new_queue = &todo.back().q;
tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s); tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s);
succ_queue::iterator merge_end; succ_queue::iterator merge_end;
@ -389,6 +389,7 @@ namespace spot
if (!i) if (!i)
{ {
new_queue->push_back(successor(acc, dest)); new_queue->push_back(successor(acc, dest));
inc_depth();
continue; continue;
} }
// Skip dead states. // Skip dead states.
@ -457,7 +458,6 @@ namespace spot
} }
prev->q.splice(prev->q.end(), last->q); prev->q.splice(prev->q.end(), last->q);
todo.pop_back(); todo.pop_back();
dec_depth();
} }
new_queue = &todo.back().q; new_queue = &todo.back().q;
} }
@ -477,6 +477,7 @@ namespace spot
bdd acc = old->acc; bdd acc = old->acc;
// Delete other states. // Delete other states.
new_queue->erase(old); new_queue->erase(old);
dec_depth();
// Delete dead states. // Delete dead states.
if (*i == -1) if (*i == -1)
continue; continue;