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.
* configure.ac: Call CHECK_ATOMIC after setting the C++ options.
This is probably not necessary, but it makes more sense.
* m4/l_atomic.m4: Augment the test body with a scenario
that actually requires -latomic.
* bin/common_post.cc, bin/randaut.cc: Implement -b/--buchi.
Also add --sba as alias for -B, and --gba as alias for --tgba.
* NEWS: Document those changes.
* doc/org/ltl2tgba.org, doc/org/oaut.org: Adjust documentation.
* tests/core/ltl2tgba2.test, tests/core/ltlcross2.test,
tests/core/randaut.test: Add more tests.
* tests/core/sbacc.test: --sbacc cannot be abbreviated as --sba
anymore.
Mentioned in issue #298.
* spot/twaalgos/determinize.cc: Do not copy prop_complete of
the input if it is false.
* tests/python/298.py: Test it.
* NEWS: Mention the bug.
Related to issue #298.
* spot/twaalgos/determinize.cc: Recognize braces that are temporary
to avoid emitting colors when they become empty.
* tests/python/298.py: New file, showing a reduction of colors.
* tests/Makefile.am: Add it.
* tests/core/ltlsynt.test: Adjust expected output (now smaller).
* tests/core/genltl.test: Adjust one expected output (now larger).
* NEWS: Mention the issue.
This helped confirming a behavior observed in #298.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add support
for -x exprop.
* bin/spot-x.cc, NEWS: Document it.
* tests/core/ltl2tgba2.test: Test it.
* spot/twaalgos/game.hh, spot/twaalgos/game.cc: Rename
solve_reachability_game() as solve_safety_game(), rewrite it (the old
implementation incorrectly marked dead states as winning for their
owner).
* tests/python/paritygame.ipynb: Rename as...
* tests/python/games.ipynb: ... this, and illustrate
solve_safety_game().
* tests/Makefile.am, NEWS, doc/org/tut.org: Adjust.
* tests/python/except.py: Add more tests.
Part of #444.
* spot/twaalgos/minimize.cc (minimize_wdba): Terminal automata do not
need a product to decide which states are accepting in the DBA. This
is faster, and also determinize more formulas of #443.
* tests/core/ltl2tgba2.test: Adjust the expected iteration where
determinization will be aborted.
Part of #444.
* spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh: Implement
accepting sink handling.
* spot/twaalgos/minimize.cc (minimize_wdba): Pass sinks to
tgba_powerset.
* spot/misc/bitvect.hh: Add an interesects method.
* tests/core/ltl2tgba2.test: More tests.
* NEWS: Mention this new feature.
Fixes#443, reported by Roei Nahum. (However the fix
only works for the development version, where wdba-det-max
was introduced to work around that kind of problem.)
* spot/twaalgos/minimize.cc: Avoid aborter being implicitly
converted to Boolean.
* tests/core/ltl2tgba2.test: Add test case.
* THANKS: Add Roei Nahum.
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.
* doc/org/satmin.tex: Use a plain background color instead of some
hashed lines pattern. This reduces the size of the resulting SVG
file from 1.9MB to 50kB after minification.
* doc/org/satmin.org: Adjust to mention autfilt.
