remfin: do not clone transitions that are accepting in main

* spot/twaalgos/remfin.cc (default_strategy): Detect transitions
from the main copy that are completely accepting and that do not
need to be repeated in the clones.
* tests/python/remfin.py: Add a test case.
* tests/core/ltl2dstar4.test: Improve expected results.
* NEWS: Mention the change.
This commit is contained in:
Alexandre Duret-Lutz 2020-05-23 11:56:16 +02:00
parent 260a141b1c
commit 6074202b9b
4 changed files with 57 additions and 6 deletions

3
NEWS
View file

@ -32,6 +32,9 @@ New in spot 2.9.0.dev (not yet released)
spot::translator class when creating deterministic automata with
generic acceptance.
- remove_fin() learned a trick to remove some superfluous
transitions.
Bugs fixed:
- Work around undefined behavior reported by clang 10.0.0's UBsan.