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

remfin: fix a corner case for rabin_to_buchi_maybe

Browse source 
when fin_alone sets where presents (i.e., not really Rabin condition),
the rabin_to_buchi_maybe() could fail to notice DBA-typeness.

* spot/twaalgos/remfin.cc: Don't set scc_ba_type to false when
fin_alone is present.
* tests/core/remfin.test: Add a test case.
This commit is contained in:
Alexandre Duret-Lutz 2017-04-04 13:53:16 +02:00
parent cebc4b00b5
commit b442d2bbd4
3 changed files with 58 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

13
spot/twaalgos/remfin.cc
View file

@ -73,7 +73,7 @@ namespace spot
// accepting, but which becomes non-accepting when extended with
// more states.
i -= f;
i |= (inf_alone & sets);
i |= inf_alone & sets;
if (!i)
{
// Check whether the SCC is accepting. We do that by simply
@ -192,14 +192,9 @@ namespace spot
ba_final_states[s] = true;
scc_ba_type = true;
}
// Conversely, if all fin_alone appear in the SCC, then it
// cannot be accepting.
else if (sets & fin_alone)
{
scc_ba_type = false;
}
// In the generale case (no fin_alone involved), we need
// a dedicated check.
// In the general case, we need a dedicated check. Note
// that the used fin_alone sets can be ignored, as they
// cannot contribute to Büchi-typeness,
else
{
scc_ba_type = is_scc_ba_type(aut, si.states_of(scc),