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

remfin: avoid some loops in SCC that do not intersect any Fin

Browse source 
* src/twaalgos/remfin.cc: Here.
This commit is contained in:
Alexandre Duret-Lutz 2015-07-16 12:07:40 +02:00
parent d8a1dafad1
commit e6a5a743f7
1 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/twaalgos/remfin.cc
View file

@ -283,12 +283,17 @@ namespace spot
// What to keep and add into the main copy
acc_cond::mark_t main_sets = 0U;
acc_cond::mark_t main_add = 0U;
bool intersects_fin = false;
for (unsigned i = 0; i < cs; ++i)
if (!(m & rem[i]))
{
main_sets |= keep[i];
main_add |= add[i];
}
else
{
intersects_fin = true;
}
trace << "main_sets " << main_sets << "\nmain_add " << main_add << '\n';
// Create the main copy
@ -296,7 +301,9 @@ namespace spot
for (auto& t: aut->out(s))
res->new_edge(s, t.dst, t.cond, (t.acc & main_sets) | main_add);
if (si.is_rejecting_scc(n))
// We do not need any other copy if the SCC is non-accepting,
// of if it does not intersect any Fin.
if (!intersects_fin || si.is_rejecting_scc(n))
continue;
// Create clones