Fixes#471, reported by Cambridge Yang.
* spot/twa/twa.cc (intersecting_run): Disable the product
optimization for weak automata.
* tests/python/471.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
Part of #471.
* spot/twaalgos/emptiness.cc: Throw an exception if
the cycle is rejecting.
* spot/twaalgos/emptiness.hh: Document this behavior.
* tests/python/except.py: Test it.
This fixes#469.
* spot/misc/bitset.hh (bitset::operator-): Rewrite.
I cannot follow the logic of the old implementation.
* tests/python/setacc.py: Add a test case, inspired from #469.
This fixes#462.
* spot/twaalgos/gfguarantee.cc (do_g_f_terminal_inplace): Replace the
redirect_src vector by a unique_ptr<unsigned[]>. Not only does this
remove the false positive diagnostic, but it also removes the unneeded
default initialization of the elements of that vector.
* bin/man/spot-x.x, bin/spot-x.cc: Improve documentation of SAT-based
minimization. It was still referring to TGBA although it works for
TwA.
* spot/twaalgos/postproc.cc: Typo.
Based on report by Michaël Cadilhac.
* spot/graph/graph.hh, spot/twa/twagraph.hh (defrag_state): Clarify
that only unreachable states are meant to be removed.
* spot/twa/twagraph.hh (merge_edges): Typo in comment. Fixes#457.
* THANKS: Add Michaël.
* spot/twa/twagraph.cc (dump_storage_as_dot): Prefer \n over a plain
new line to work around GraphViz issue 1931, which was causing
twagraph-internals.ipynb to fail in our test suite.
* spot/tl/formula.cc: Correctly set eventual and universal properties
for ->, <->, and xor. This wasn't really relevant before, but there
are now situation where those are not rewritten.
* tests/core/kind.test: Adjust expected output.
* tests/core/ltl2tgba2.test: New test case, reported by Florian
Renkin.
* NEWS: Mention the bug.
Reported by Florian Renkin.
* spot/graph/graph.hh, spot/twa/twagraph.hh (merge_edge): Document
that it is expected that state i can only be renamed as j if j≤i.
Fixes#449.
* spot/twaalgos/gfguarantee.cc (do_g_f_terminal_inplace): Save
edge additions to perform them after the loop. Otherwise,
reallocating the edge buffer might break the iteration.
Upgrading gnulib turned to be too difficult, so this only includes
updates to m4 files necessary to please Autoconf 2.70.
For issue #447.
* m4/extensions.m4, m4/malloc.m4, m4/std-gnu11.m4: Cherry-pick
from today's gnulib version.
Part of #447.
* configure.ac, m4/debug.m4, m4/devel.m4, m4/gccoptim.m4,
m4/ndebug.m4: Replace AC_ERROR and AC_HELP_STRING by
by AC_MSG_ERROR and AS_HELP_STRING.
Part of issue #447.
Autoconf 2.69 was released in 2012, so it now widely available. The
recent release of 2.70 is obsoleting some constructs, so it will be
easier on us if we do not have too many versions to support.
* HACKING, configure.ac: Require Autoconf 2.69.
This fixes#442.
* spot/twaalgos/simulation.cc (iterated_simulations_): Initialize next
so that we can exit after the first iteration if no change was made.
* NEWS: Mention the bug.
This fixes#441, reported by Jérôme Dubois.
* tests/python/mergedge.py: New file.
* tests/Makefile.am: Add it.
* spot/twa/twagraph.cc (merge_edges): Fix initialization of second
loop.
* NEWS: Mention the bug.
