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

* src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::clear_todo,

Browse source 
couvreur99_check_shy::check): Sum all successors in the
todo stack AND all items on the stack.
This commit is contained in:
Alexandre Duret-Lutz 2005-01-18 10:52:23 +00:00
parent 2604b27008
commit 48dfd73cca
2 changed files with 19 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

13
ChangeLog
View file

@ -1,3 +1,16 @@
2005-01-18 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/gtec/gtec.cc (couvreur99_check_shy::clear_todo,
couvreur99_check_shy::check): Sum all successors in the
todo stack AND all items on the stack.
2005-01-17 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptiness_stats.hh (ec_statistics::depth): New function.
* 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.
2005-01-13 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr> 2005-01-13 Denis Poitrenaud <Denis.Poitrenaud@lip6.fr>
* src/tgbatest/randtgba.cc: Close the formula file and remove a trace. * src/tgbatest/randtgba.cc: Close the formula file and remove a trace.

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

@ -266,8 +266,8 @@ namespace spot
{ {
// Setup depth-first search from the initial state. // Setup depth-first search from the initial state.
todo.push_back(todo_item(0, 0)); todo.push_back(todo_item(0, 0));
inc_depth();
todo.back().q.push_front(successor(bddtrue, ecs_->aut->get_init_state())); todo.back().q.push_front(successor(bddtrue, ecs_->aut->get_init_state()));
inc_depth(2);
} }
couvreur99_check_shy::~couvreur99_check_shy() couvreur99_check_shy::~couvreur99_check_shy()
@ -292,7 +292,7 @@ namespace spot
if (spi.first == 0) if (spi.first == 0)
delete q->s; delete q->s;
} }
dec_depth(todo.back().q.size()); dec_depth(todo.back().q.size() + 1);
todo.pop_back(); todo.pop_back();
} }
assert(depth() == 0); assert(depth() == 0);
@ -317,10 +317,12 @@ 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.
set_states(ecs_->states()); set_states(ecs_->states());
assert(depth() == 0);
return 0; return 0;
} }
@ -374,6 +376,7 @@ 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;
@ -458,6 +461,7 @@ 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;
} }