* spot/twaalgos/car.cc: Don't reserve colors when parity prefix is used
but the condition has no parity prefix and use colors of prefix in
apply_to_Buchi.
Reported by Florian Renkin.
* spot/twaalgos/cleanacc.cc: Do not rewrite
...Fin(0)&(Fin(1)|(Fin(3)&Inf(4)))... as Fin(0)&f when it appears that
{1,3} cannot receive {0}, because {1} is used elsewhere in the
acceptance.
* tests/python/simplacc.py: Add test case.
* spot/twaalgos/relabel.cc: Remove false transitions if
some of the propositions are equivalent to true or false.
* NEWS: Mention the bug.
* tests/core/ltl2tgba2.test: Test it.
* spot/twaalgos/degen.cc (keep_bottommost_copies): Fix intialisation
of bottommost_occurence.
* tests/python/pdegen.py: Add test case sent by Florian Renkin.
doing it too early breaks the "redirect all-accepting transitions"
optimization
* spot/twaalgos/degen.cc: move the original-states composition
code.
* tests/python/pdegen.py: Add test-case from Florian Renkin.
* bin/autfilt.cc: Add a --partial-degeneralize option.
* NEWS: Mention it.
* spot/twaalgos/degen.cc: Do not restrict partial_degeneralize() to
deterministic automata.
* spot/twaalgos/degen.hh: Adjust documentation.
* tests/core/pdegen.test: New test case.
* tests/Makefile.am: Add it.
* tests/python/pdegen.py: Adjust.
* spot/twaalgos/degen.cc: If an all-accepting transition has been
redirected, we need to force purge_unreachable_state() to be called,
otherwise we may have unreachable states.
* tests/python/pdegen.py: Add test case.
* spot/twaalgos/relabel.cc: Remove false transitions if
some of the propositions are equivalent to true or false.
* NEWS: Mention the bug.
* tests/core/ltl2tgba2.test: Test it.
Reported by Florian Renkin
* spot/twaalgos/degen.cc (partial_degeneralize): Update
original-state when partial_degeneralize is executed more
than once in a loop.
* tests/python/pdegen.py: Add test case.
* spot/twaalgos/degen.cc,
spot/twaalgos/degen.hh (is_partially_degeneralizable): New function.
(partial_degeneralize): New version without todegen argument.
* tests/python/pdegen.py: Add test cases.
* spot/twaalgos/degen.cc, spot/twaalgos/degen.hh: Implement this.
Also throw a runtime error in case were todegen does not match any
subformula.
* tests/python/pdegen.py: Add tests.
On these 4 cases, added to pdegen.py, and supplied by Florian Renkin,
partial_degeneralize() is now at least as good as degeneralize_tba(),
and sometimes better. This is achieved as follows: (1) a
propagate_marks procedure is introduced to propagate marks as far as
possible on the automaton (e.g., common outgoing marks can be push
onto the incoming transitions and vice-versa), (2) the
degeneralization order is compute dynamically, and (3) whenever and
fully-accepting transition is taken in the original automaton, the
destination level is chosen to be the highest existing level.
* spot/twaalgos/degen.cc,
spot/twaalgos/degen.hh (propagate_marks_vector, propagate_marks_here):
New functions.
(partial_degeneralize): Improve, as described above.
* tests/python/pdegen.py: Add test cases.
