* spot/misc/game.cc, spot/misc/game.hh: More efficient implementation
of Zielonka's algorithm to solve parity games. Now supports SCC
decomposition and efficient handling of certain special cases.
* doc/org/concepts.org: Document "strategy" and "state-winner"
properties.
* bin/ltlsynt.cc, tests/python/paritygame.ipynb: Adjust.
* tests/core/ltlsynt.test: Add more tests.
* spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh: Reimplement
print_aiger for speed gain, also heuristics to minimize the number
of gates as well as different encoding types have been added.
* bin/ltlsynt.cc: Make the new options for print-aiger available.
* tests/core/ltlsynt.test: Adjust tests.
This restricts the time spent in translating sub-formulas for
implication tests by limiting the associated automata to 64 states by
default. Doing so this does worsen any test case, and actually remove
all calls the BuDDy's GC in bdd.test.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh,
spot/tl/simplify.cc, spot/tl/simplify.hh, spot/tl/contain.hh,
spot/tl/contain.cc, spot/twaalgos/ltl2tgba_fm.cc,
spot/twaalgos/ltl2tgba_fm.hh: Add support for the option or
its constraint via an output_aborter.
* bin/spot-x.cc, NEWS: Document it.
* tests/core/bdd.test: Adjust and augment test case.
* python/spot/__init__.py (setup): Reduce the default maximal width of
automata so that Jupyter output does not add an horizontal scroll bar
for a few pixels.
* tests/python/automata-io.ipynb: Adjust.
* 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.
* python/spot/impl.i: Process game.hh.
* spot/misc/game.cc, spot/misc/game.hh: Make the output of
parity_game_solve() a solved_game object for easier manipulation in
Python.
* bin/ltlsynt.cc: Adjust usage.
* tests/python/paritygame.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* NEWS: Mention these bindings.
* bin/ltlsynt.cc (complete_env): Replace this function by...
* spot/misc/game.hh, spot/misc/game.cc (propagate_players): ... this
new one, hiding the "state-player" business from ltlsynt. Also do not
create a sink states unless necessary.
* tests/core/ltlsynt.test: Adjust expected number of states.
* spot/twaalgos/dot.cc: Honor the "state-player" property and draw
player 1 states using diamonds.
* doc/org/hoa.org: Show an example.
* tests/core/gamehoa.test: Make sure diamond is output.
* NEWS: Mention this.
* spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll,
spot/twaalgos/hoa.cc: Add input and output support.
* doc/org/hoa.org: Document the HOA extension.
* bin/ltlsynt.cc: Add a --print-game-hoa option to
produce such format.
* tests/core/gamehoa.test: New file to test this.
* tests/Makefile.am: Add it.
* NEWS: Mention this new feature.
This class was a simple wrapper on top of twa_graph_ptr, but it's
easier to simply use a twa_graph_ptr with a "state-player" property
instead, this way we will be able to modify the automata I/O routines
to support games directly.
* spot/misc/game.cc, spot/misc/game.hh: Rewrite the solver and
pg_printer interface.
* bin/ltlsynt.cc: Adjust.
* NEWS: Mention this change.
* doc/org/concepts.org: Mention the state-player property.
This patch addresses the BuDDy part of #396,
reported by Florian Renkin and Reed Oei.
* src/kernel.c, src/kernel.h: Declare a bddrecstack and
associated macros. Resize it when new variable are declared.
* src/cache.h: Add a BddCache_index macro.
* src/bddop.c (not_rec, apply_rec, quant_rec, appquant_rec,
support_rec, ite_rec, compose_rec, restrict_rec, satone_rec,
satoneset_rec): Rewrite using this stack to get rid of the recursion.
* spot/twaalgos/toparity.cc: Do not call prpagate_marks_here twice if
the automaton was not degeneralized.
* spot/twaalgos/toparity.hh: Typo in comment.
Under that option, !(a ^ b) was converted
to (!a <=> !b) instead of simply (a <=> b).
* spot/tl/simplify.cc (equiv_or_xor): Improve
rewriting.
* tests/core/ltl2tgba2.test, tests/python/simstate.py: Adjust test
cases.
