* spot/tl/simplify.hh, spot/tl/simplify.cc,
spot/twaalgos/translate.cc: Update the tl_simplification
options after all preferences have been given.
* bin/ltlsynt.cc: Display the size of the translation output.
* tests/core/ltlsynt.test: Add test case.
* bin/ltlsynt.cc: Make sure to_parity_old() receive a deterministic
automaton, for correctness. Also call reduce_parity() afterward,
to match what was done in 2.8.7.
* tests/core/ltlsynt.test: Include lar.old in the comparison of all
results to make sure it give the same result as the other 3
algorithms.
* spot/twaalgos/aiger.cc: Simplify some bit operatitions. Force the
ordering of operations in aig_and, that was causing a test case to
fail on ARM, and greatly simplify the code and data structures used in
remove_unused().
* tests/core/ltlsynt.test: Adjust expected output.
ltlsynt now offers two algorithms: one where splitting occurs before
determinization (the historical one) and one where determinization
occurs before splitting.
* bin/ltlsynt.cc: here
* tests/core/ltlsynt.test: test it and refactor test file
* NEWS: document it
* spot/misc/game.hh, spot/misc/game.cc: remove Calude's algorithm
Improve the way transitions are duplicated when preparing the turn-based
game for synthesis. The resulting arena should now be deterministic on
nodes owned by the environment. Also move the code to another file, so
that it is easier to test (e.g. in Python).
* bin/ltlsynt.cc: move the code
* spot/twaalgos/split.cc, spot/twaalgos/split.hh: move the code and
implement the improvements
* tests/Makefile.am, tests/python/split.py: test it
* tests/core/ltlsynt.test: update existing tests to reflect the changes
To ease debugging and testing, ltlsynt can output the synthesized
strategy as an automaton, not just an aiger circuit.
Also, its exit code has been changed to something meaningful.
* bin/ltlsynt.cc: Various improvements: options, exit code, code style
* spot/twaalgos/aiger.hh, spot/twaalgos/aiger.cc,
spot/twaalgos/Makefile.am: Move the aiger printer to separate files
* tests/core/ltlsynt.test: Clean up and update test file
* tests/Makefile.am: Add the test file to the test suite
* NEWS: document the new aiger printer
* doc/org/concepts.org: document the named property "synthesis-outputs",
used by print_aiger
