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

degen: fix a memory leak

Browse source 
* src/tgbaalgos/degen.cc (degeneralize): Do not call i->current_state()
to get the current SCC, as we already have the state in d.first.
This commit is contained in:
Alexandre Duret-Lutz 2013-02-11 14:01:02 +01:00
parent 63cb925f1f
commit 1b2f9fe5d8
1 changed files with 15 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/tgbaalgos/degen.cc
View file

@ -381,11 +381,21 @@ namespace spot
names[d.first] = uniq.size();
#endif
// Check whether the target's SCC is accepting
bool is_scc_acc = false;
int scc = use_scc ? m.scc_of_state(i->current_state()) : -1;
if (!use_scc || m.accepting(scc))
is_scc_acc = true;
// Check whether the target SCC is accepting
bool is_scc_acc;
int scc;
if (use_scc)
{
scc = m.scc_of_state(d.first);
is_scc_acc = m.accepting(scc);
}
else
{
// If we have no SCC information, treat all SCCs as
// accepting.
scc = -1;
is_scc_acc = true;
}
// The old level is slevel. What should be the new one?
bdd acc = i->current_acceptance_conditions();