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

* src/tgbaalgos/emptinesscheck.cc: Remove some superfluous

Browse source 
`emptiness_check::'.
This commit is contained in:
Alexandre Duret-Lutz 2003-10-24 09:41:52 +00:00
parent 549c31605d
commit 26f15224fc
2 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

3
ChangeLog
View file

@ -1,5 +1,8 @@
2003-10-24 Alexandre Duret-Lutz <adl@src.lip6.fr> 2003-10-24 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.cc: Remove some superfluous
`emptiness_check::'.
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::remove_component): * src/tgbaalgos/emptinesscheck.cc (emptiness_check::remove_component):
Rewrite. Rewrite.

17
src/tgbaalgos/emptinesscheck.cc
View file

@ -85,7 +85,7 @@ namespace spot
while (!todo.empty()) while (!todo.empty())
{ {
pair_state_iter step = todo.top(); pair_state_iter step = todo.top();
if ((step.second)->done()) if (step.second->done())
{ {
todo.pop(); todo.pop();
assert(!root_component.empty()); assert(!root_component.empty());
@ -96,16 +96,15 @@ namespace spot
if (comp_tmp.index == i_0->second) if (comp_tmp.index == i_0->second)
{ {
// The current node is a root of a Strong Connected Component. // The current node is a root of a Strong Connected Component.
emptiness_check::remove_component(step.first); remove_component(step.first);
assert(!arc_accepting.empty()); assert(!arc_accepting.empty());
arc_accepting.pop(); arc_accepting.pop();
assert(root_component.size() == arc_accepting.size());
} }
else else
{ {
root_component.push(comp_tmp); root_component.push(comp_tmp);
assert(root_component.size() == arc_accepting.size());
} }
assert(root_component.size() == arc_accepting.size());
} }
else else
{ {
@ -355,7 +354,7 @@ namespace spot
iter_s->first(); iter_s->first();
for (iter_s->first(); !iter_s->done(); iter_s->next()) for (iter_s->first(); !iter_s->done(); iter_s->next())
{ {
const state* curr_state = (started_.second)->current_state(); const state* curr_state = started_.second->current_state();
if (comp_path.has_state(curr_state)) if (comp_path.has_state(curr_state))
{ {
if (curr_state->compare(to_state) == 0) if (curr_state->compare(to_state) == 0)
@ -369,8 +368,7 @@ namespace spot
complete_map[curr_father].second)); complete_map[curr_father].second));
curr_father = complete_map[curr_father].first; curr_father = complete_map[curr_father].first;
} }
emptiness_check::period.splice(period.end(), period.splice(period.end(), tmp_comp);
tmp_comp);
todo_complete.clear(); todo_complete.clear();
break; break;
} }
@ -479,13 +477,12 @@ namespace spot
} }
for (cycle_path::iterator it = best_lst.begin(); for (cycle_path::iterator it = best_lst.begin();
it != best_lst.end(); ++it) it != best_lst.end(); ++it)
emptiness_check::period.push_back(*it); period.push_back(*it);
if (best_acc != to_accept) if (best_acc != to_accept)
{ {
bdd rec_to_acc = to_accept - best_acc; bdd rec_to_acc = to_accept - best_acc;
emptiness_check::accepting_path(comp_path, period.back().first, accepting_path(comp_path, period.back().first, rec_to_acc);
rec_to_acc);
} }
else else
{ {