* doc/org/citing.org, doc/spot.bib: Here.

* 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/twa/acc.cc: Fix detection of single-pairs gen-Rabin and
gen-Streett.
* tests/core/randaut.test: Add test case.
* NEWS: Mention this issue.

* spot/twaalgos/degen.cc (degeneralize, partial_degeneralize): Here.
* spot/twaalgos/degen.hh: Mention it.

* 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.

* python/spot/__init__.py: Here.
* tests/python/except.py: Add test.
* NEWS: Mention the issue.

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/remfin.cc, spot/twaalgos/remfin.hh: Implement it.
* tests/python/tra2tba.py: Test it.
* NEWS: Mention it.

* 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: Implement this.
* tests/python/pdegen.py: Add tests.

* spot/twaalgos/degen.cc (degeneralize_tba): Here.
* tests/python/pdegen.py, tests/python/simstate.py: Adjust expected
values.
* NEWS: Mention the bug.

* 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.

Implement those rules in simplify_acceptance_here().

* NEWS: Mention the change.
* spot/twa/acc.cc,
spot/twa/acc.hh (acc_cond::acc_code::used_once_sets): New method.
* spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh:
Implement the above rule.
* tests/core/remfin.test: Adjust expected results.
* tests/python/simplacc.py: New file.
* tests/Makefile.am: Add it.

* tests/python/ipnbdoctest.py: Catch kernel deaths, wait a random
number of seconds, and try again up to three times.

Suggested by František Blahoudek.

* bin/ltlcross.cc: Implement this.
* NEWS, doc/org/ltlcross.org: Document it.
* tests/core/ltlcross4.test: Test it.

* NEWS, configure.ac, doc/org/setup.org: Bump version number.

* tests/python/ipnbdoctest.py: Use shorter timeouts, and flush the
shell messages without expecting them.

* tests/python/ipnbdoctest.py: Use shorter timeouts, and flush the
shell messages without expecting them.

* bin/common_setup.cc, debian/copyright: Here.

* bin/common_setup.cc, debian/copyright: Here.

Reported by František Blahoudek.

* spot/twa/twagraph.cc: Reset prop_universal() if edges are merged in
a non-deterministic automaton.
* tests/core/det.test: Add test case.
* NEWS: Mention the issue.

* bin/common_finput.cc, bin/ltl2tgba.cc, bin/ltldo.cc: Make sure
--negate is listed along with input options.

Reported by František Blahoudek.

* spot/twaalgos/postproc.cc: Turn "t" into "Inf(0)" for BA.
* tests/core/ltl2tgba.test: Add test case.
* NEWS: Mention the bug.

* spot/misc/tmpfile.cc: Display strerror(errno) plus some suggestions
that depend on the error.  Based on a report from Shengping Shaw.
* THANKS: Add reporter.
* tests/core/ltlcross5.test: New file.
* tests/Makefile.am: Add it.

Reported by František Blahoudek.

* spot/twa/twagraph.cc: Reset prop_universal() if edges are merged in
a non-deterministic automaton.
* tests/core/det.test: Add test case.
* NEWS: Mention the issue.

* bin/common_finput.cc, bin/ltl2tgba.cc, bin/ltldo.cc: Make sure
--negate is listed along with input options.

Reported by František Blahoudek.

* spot/twaalgos/postproc.cc: Turn "t" into "Inf(0)" for BA.
* tests/core/ltl2tgba.test: Add test case.
* NEWS: Mention the bug.

* spot/misc/tmpfile.cc: Display strerror(errno) plus some suggestions
that depend on the error.  Based on a report from Shengping Shaw.
* THANKS: Add reporter.
* tests/core/ltlcross5.test: New file.
* tests/Makefile.am: Add it.

* 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.