sbacc: fix a serious bug

Reported by Thibaud Michaud

* spot/twaalgos/sbacc.cc: Do not label rejecting SCCs with the empty
mark, as it might be accepting.
* tests/core/sbacc.test: Add test cases.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2017-04-19 18:46:35 +02:00
parent ba15788a94
commit f02ca87f07
3 changed files with 85 additions and 2 deletions

5
NEWS
View file

@ -1,6 +1,9 @@
New in spot 2.3.3.dev (not yet released)
Nothing yet.
Bugs fixed:
- the transformation to state-based acceptance (spot::sbacc()) was
incorrect on automata where the empty acceptance mark is accepting.
New in spot 2.3.3 (2017-04-11)