Commit graph

4 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
b733d486be fix degeneralize_tba after accepting transition
* spot/twaalgos/degen.cc (degeneralize_tba): Here.
* tests/python/pdegen.py, tests/python/simstate.py: Adjust expected
values.
* NEWS: Mention the bug.
2020-02-03 15:38:51 +01:00
Alexandre Duret-Lutz
f9e75de647 partial_degeneralize: a support for disjunction of Fin
* 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.
2020-02-03 11:08:20 +01:00
Alexandre Duret-Lutz
f1008c156b improve partial_degeneralize() on several cases
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.
2020-02-03 09:52:54 +01:00
Alexandre Duret-Lutz
bf7ccfe7e6 new partial_degeneralize() algorithm
* spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Implement it.
* tests/python/pdegen.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the new function.
2019-12-11 17:09:55 +01:00