Commit f83a21cf authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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

Check whether the state is in the current SCC before passing it
to h_filt().
parent 10b2511d
2003-11-13 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.cc (emptiness_check::complete_cycle):
Check whether the state is in the current SCC before passing it
to h_filt().
2003-11-07 Alexandre Duret-Lutz <adl@src.lip6.fr>
* iface/gspn/eesrg.cc (tgba_succ_iterator_gspn_eesrg::first_): New
......
......@@ -425,11 +425,15 @@ namespace spot
todo.pop_front();
for (i->first(); !i->done(); i->next())
{
const state* dest = h_filt(i->current_state());
const state* dest = i->current_state();
// Do not escape this SCC.
if (!scc.has_state(dest))
continue;
{
delete dest;
continue;
}
dest = h_filt(dest);
bdd cond = i->current_condition();
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment