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 01ee49290f
commit 1daffe12f0
3 changed files with 58 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

6
NEWS
View file

@ -18,6 +18,12 @@ New in spot 2.3.2.dev (not yet released)
- In bench/stutter/ the .cc files were not compiling due to warnings being
caught as errors.
- The code in charge of detecting DBA-type Rabin automata is
actually written to handle a slightly larger class of acceptance
conditions (e.g., Fin(0)|(Fin(1)&Inf(2))), however it failed to
correctly detect DBA-typeness in some of these non-Rabin
acceptance.
New in spot 2.3.2 (2017-03-15)
Tools: