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

scc_filter: add quick test for very-weak

Browse source 
Related to issue #351.

* spot/twaalgos/sccfilter.cc: When handling weak automata, we know
they are very-weak if the SCC count is equal to the number of states.
* tests/core/dca2.test, tests/core/monitor.test,
tests/core/parity2.test, tests/core/randomize.test,
tests/core/readsave.test, tests/core/remfin.test,
tests/core/sccsimpl.test, tests/core/wdba2.test,
tests/python/dualize.py, tests/python/remfin.py: Adjust output.
This commit is contained in:
Alexandre Duret-Lutz 2018-06-11 20:24:17 +02:00
parent 729921c0a0
commit fbc372e292
11 changed files with 35 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

14
spot/twaalgos/sccfilter.cc
View file

@ -436,14 +436,20 @@ namespace spot
scc_info* given_si)
{
twa_graph_ptr res;
scc_info* si = given_si;
if (aut->prop_inherently_weak())
{
// Create scc_info here, because we will need it to decide
// very-weakness.
if (!si)
si = new scc_info(aut, scc_info_options::TRACK_SUCCS
| scc_info_options::TRACK_STATES_IF_FIN_USED);
if (aut->acc().is_t() || aut->acc().is_co_buchi())
res =
scc_filter_apply<state_filter<weak_filter<false>>>(aut, given_si);
scc_filter_apply<state_filter<weak_filter<false>>>(aut, si);
else
res =
scc_filter_apply<state_filter<weak_filter<true>>>(aut, given_si);
scc_filter_apply<state_filter<weak_filter<true>>>(aut, si);
}
else if (aut->acc().is_generalized_buchi())
{
@ -485,6 +491,10 @@ namespace spot
{
res->prop_weak(true);
res->prop_state_acc(true);
if (si->scc_count() == aut->num_states())
res->prop_very_weak(true);
if (!given_si)
delete si;
}
return res;
}