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

* src/tgbaalgos/emptinesscheck.cc (emptiness_check::accepting_path)

Browse source 
Fix handling of PATH when backtracking.  Report from Soheib Baarir.
This commit is contained in:
Alexandre Duret-Lutz 2004-03-23 09:33:27 +00:00
parent cf6602a3be
commit aba2dc75d7
2 changed files with 19 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
ChangeLog
View file

@ -1,3 +1,8 @@
2004-03-23 Alexandre DURET-LUTZ <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::accepting_path)
Fix handling of PATH when backtracking. Report from Soheib Baarir.
2004-03-18 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-03-18 Alexandre Duret-Lutz <adl@src.lip6.fr>
Move the free_list management into a separate class for reuse. Move the free_list management into a separate class for reuse.

15
src/tgbaalgos/emptinesscheck.cc
View file

@ -712,7 +712,11 @@ namespace spot
todo.pop(); todo.pop();
delete iter; delete iter;
seen.erase(s); seen.erase(s);
if (todo.size())
{
assert(path.size());
path.pop_back(); path.pop_back();
}
continue; continue;
} }
@ -762,7 +766,7 @@ namespace spot
if (best_acc_restrict == acc_restrict) if (best_acc_restrict == acc_restrict)
{ {
if (best_path.size() <= path.size()) if (best_path.size() <= path.size())
continue; goto backtrack_path;
} }
else else
{ {
@ -774,13 +778,20 @@ namespace spot
// FIXME: It would be better to count the number // FIXME: It would be better to count the number
// of acceptance conditions. // of acceptance conditions.
if (bddtrue != (best_acc_restrict >> acc_restrict)) if (bddtrue != (best_acc_restrict >> acc_restrict))
continue; goto backtrack_path;
} }
} }
// The current path the best one. // The current path the best one.
best_path = path; best_path = path;
best_acc = acc; best_acc = acc;
backtrack_path:
// Continue exploration from parent to find better paths.
// (Do not pop PATH if ITER is done, because that will be
// done at the top of the loop, among other things.)
if (!iter->done())
path.pop_back();
} }
// Append our best path to the period. // Append our best path to the period.