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

postproc: use scc_filter_states on SBA

Browse source 
* src/tgbaalgos/postproc.cc: Here.  Otherwise, reading
a neverclaim with autfilt would loose the SBA property
and degeneralize again.
This commit is contained in:
Alexandre Duret-Lutz 2015-01-09 22:23:55 +01:00
parent b2c2411bcc
commit 604971d651
1 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/tgbaalgos/postproc.cc
View file

@ -149,7 +149,12 @@ namespace spot
// ignored. // ignored.
a = scc_filter_states(a); a = scc_filter_states(a);
else if (scc_filter_ > 0) else if (scc_filter_ > 0)
a = scc_filter(a, scc_filter_ > 1); {
if (type_ == BA && a->is_sba())
a = scc_filter_states(a);
else
a = scc_filter(a, scc_filter_ > 1);
}
if (type_ == Monitor) if (type_ == Monitor)
{ {