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/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.
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.
* 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.
* spot/twaalgos/remfin.cc (tra_to_tba): Remove the SCC-emptiness
check that was done by creating a temporary automaton. Use the
scc_info::check_scc_emptiness() function instead.
* spot/twaalgos/sccinfo.cc,
spot/twaalgos/sccinfo.hh (scc_info::check_scc_emptiness): Mark
this function as const.
(scc_and_mark_filter): Make sure we only combine with a lower filter
of the same type.
* spot/twaalgos/genem.cc: Remove one stray debugging statement.
* tests/python/genem.py: Remove a duplicate test.
This is to workaround differences in minidom's pretty-printing that
occurred between Python 3.7 and 3.8.
* python/spot/jupyter.py (SVG): New class.
* python/spot/__init__.py: Use it.
* tests/python/_altscc.ipynb, tests/python/alternation.ipynb,
tests/python/automata.ipynb, tests/python/formulas.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb,
tests/python/testingaut.ipynb, tests/python/twagraph-internals.ipynb,
tests/python/word.ipynb: Adjust.
* spot/twa/acc.hh (acc_cond::mark_t): Diagnose mark_t with set numbers
that are too larges.
* tests/python/except.py: Adjust.
* tests/core/acc.cc: Remove most of asserts, as those can be disabled,
and adjust expected exception.
* spot/twa/acc.hh: Introduce parity_min_odd(n) and friends.
* spot/twaalgos/determinize.cc, spot/twaalgos/rabin2parity.cc,
spot/twaalgos/toparity.cc: Use them.
* tests/python/parity.py: Call each function exhaustively.
* NEWS: Mention the new functions.
This was prompted by reports by Andrew Wells and Yong Li.
* NEWS, doc/tl/tl.tex: Document the changes.
* THANKS: Add Andrew.
* bin/ltlfilt.cc: Match --ltl before --from-ltlf if needed.
* spot/parsetl/parsedecl.hh, spot/parsetl/parsetl.yy,
spot/parsetl/scantl.ll: Parse X[!].
* spot/tl/formula.cc, spot/tl/formula.hh: Declare the new operator.
* spot/tl/ltlf.cc: Adjust to handle op::X and op::strong_X correctly.
* spot/tl/dot.cc, spot/tl/mark.cc, spot/tl/mutation.cc,
spot/tl/print.cc, spot/tl/simplify.cc, spot/tl/snf.cc,
spot/tl/unabbrev.cc, spot/twa/formula2bdd.cc,
spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc,
tests/core/ltlgrind.test, tests/core/rand.test,
tests/core/sugar.test, tests/python/randltl.ipynb: Adjust.
* tests/core/ltlfilt.test, tests/core/sugar.test,
tests/core/utf8.test: More tests.
* spot/twaalgos/product.cc: The res pointer should be
passed by reference since we reset it to nullptr when
output_aborter says "too large".
* python/spot/impl.i: Add binding for powerset.hh,
so we can use output_aborter in Python.
* tests/python/prodexpt.py: Test it.
The previous patch triggered this issue again, failing
core/ltl2tgba2.test.
* spot/twaalgos/gfguarantee.cc: Separate the replaying of history from
the modification of the automaton.
* NEWS: Mention the bug.
* tests/python/twagraph-internals.ipynb, tests/python/automata.ipynb:
Adjust.
These rules come from Delag's paper, and help some cases
in issue #385.
* spot/tl/simplify.cc: Implement the simplification.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/385.test: New file.
* tests/Makefile.am: Add it.
* tests/core/reduccmp.test: More tests.
* tests/core/ltl2tgba2.test: Adjust one improved case.
* tests/python/automata.ipynb, tests/python/twagraph-internals.ipynb:
Adjust expected output, as the cnf/dnf reorder some subformulas.
* spot/twaalgos/alternation.cc, spot/twaalgos/alternation.hh,
spot/twaalgos/complement.cc, spot/twaalgos/complement.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh,
spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh,
spot/twaalgos/product.cc, spot/twaalgos/product.hh: Use an
output_aborter argument to abort if the output is too large.
* bin/ltlcross.cc: Use complement() with an output_aborter
so that ltlcross will not attempt to build complement larger
than 500 states or 5000 edges. Add --determinize-max-states
and --determinize-max-edges options.
* tests/core/ltlcross3.test, tests/core/ltlcrossce2.test,
tests/core/sccsimpl.test, tests/core/wdba2.test,
tests/python/stutter-inv.ipynb: Adjust test cases.
* NEWS: Document this.
* bin/spot-x.cc: Add documentation for postprocessor's
det-max-states and det-max-edges arguments.
* doc/org/ltlcross.org: Update description.
This allows fixing issue #388 reported by Victor Khomenko.
* spot/twaalgos/word.cc, spot/twaalgos/word.hh (use_all_aps): New
method.
* tests/python/stutter-inv.ipynb: Use it.
* tests/python/stutter.py: New file, with Victor's test case.
* tests/Makefile.am: Add python/stutter.py.
