From 48dfd73ccacc8960258a39712f49f60607597751 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 18 Jan 2005 10:52:23 +0000 Subject: [PATCH] * 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. --- ChangeLog | 13 +++++++++++++ src/tgbaalgos/gtec/gtec.cc | 8 ++++++-- 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index f6289035d..821b6f164 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,16 @@ +2005-01-18 Alexandre Duret-Lutz + + * 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 + + * 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 * src/tgbatest/randtgba.cc: Close the formula file and remove a trace. diff --git a/src/tgbaalgos/gtec/gtec.cc b/src/tgbaalgos/gtec/gtec.cc index 8646005e2..5cfad5f96 100644 --- a/src/tgbaalgos/gtec/gtec.cc +++ b/src/tgbaalgos/gtec/gtec.cc @@ -266,8 +266,8 @@ namespace spot { // Setup depth-first search from the initial state. todo.push_back(todo_item(0, 0)); - inc_depth(); todo.back().q.push_front(successor(bddtrue, ecs_->aut->get_init_state())); + inc_depth(2); } couvreur99_check_shy::~couvreur99_check_shy() @@ -292,7 +292,7 @@ namespace spot if (spi.first == 0) delete q->s; } - dec_depth(todo.back().q.size()); + dec_depth(todo.back().q.size() + 1); todo.pop_back(); } assert(depth() == 0); @@ -317,10 +317,12 @@ namespace spot int index = todo.back().n; // Backtrack TODO. todo.pop_back(); + dec_depth(); if (todo.empty()) { // This automaton recognizes no word. set_states(ecs_->states()); + assert(depth() == 0); return 0; } @@ -374,6 +376,7 @@ namespace spot ecs_->root.push(num); arc.push(succ.acc); todo.push_back(todo_item(succ.s, num)); + inc_depth(); succ_queue* new_queue = &todo.back().q; tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s); succ_queue::iterator merge_end; @@ -458,6 +461,7 @@ namespace spot } prev->q.splice(prev->q.end(), last->q); todo.pop_back(); + dec_depth(); } new_queue = &todo.back().q; }