* spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh (parse_aag_impl_): Do
not display source filename in user facing errors. Use GNU-style
"file:line: " prefixes for locations. Adjust all sscanf() calls
to check for ignored trailing data. Add some missing checks about the
order of input and output names, checks that output names do no
intersect input names. Fix incorrect line number for unexpected
input variable number, and avoid using std::stoi as that throws
an std::invalid_argument on parse error.
* tests/python/aiger.py: Add test cases for each error message.
* spot/twaalgos/synthesis.cc: here
* spot/twaalgos/synthesis.hh: introduce a realizability_code
* bin/ltlsynt.cc, spot/twaalgos/aiger.cc: use this enum
* tests/core/ltlsynt.test: update tests
* spot/twaalgos/dot.cc: Improve the aiger printer by using a more
traditional dot syntax, indenting the output, adding some hard-coded
colors, fixing a bug in the negation of latch inputs, and rotating the
triangles for horizontal output.
* tests/python/synthesis.ipynb: Adjust expected output, and add
an example of horizontal layout.
* spot/twaalgos/dot.cc (print_dot): Add some detection of Mealy
machines, and some code to render its I/O in a <table>.
* tests/python/synthesis.ipynb: Adjust expected output.
* tests/python/_mealy.ipynb: New file.
* tests/Makefile.am: Add python/_mealy.ipynb.
* NEWS: Mention the new feature.
* spot/twaalgos/game.cc, spot/twaalgos/game.hh (game_info): Move...
* spot/twaalgos/synthesis.cc,
spot/twaalgos/synthesis.hh (synthesis_info): ... here, because this
structure contains only synthesis stuff. Also rename "solver" to
"algo" to match the ltlsynt option.
(solve_game): Move the two argument version of this function here,
since that's the only game-related generic function that use
synthesis_info.
* bin/ltlsynt.cc, tests/core/ltlsynt.test, tests/python/games.ipynb,
tests/python/synthesis.py, NEWS: Adjust all uses and mentions.
* bin/ltlsynt.cc: Implement the new option, and make it default
to bisimulation with output assignment (a.k.a. bwoa).
* NEWS, bin/spot-x.cc, doc/org/ltlsynt.org: Update the documentation.
* spot/twaalgos/game.hh: Make bwoa the default.
* tests/core/ltlsynt.test: Add and adjust test cases.
* tests/python/games.ipynb: Adjust.
* bin/ltlsynt.cc: Implement the option, and enable it by default.
* doc/org/ltlsynt.org, doc/org/ltlsynt.tex, bin/spot-x.cc, NEWS:
Document it.
* tests/core/ltlsynt.test: Adjust test cases.
* spot/twaalgos/game.hh, spot/twaalgos/synthesis.hh,
spot/twaalgos/aiger.hh: Declare new Doxygen groups for games and
synthesis.
* doc/spot.bib: Cleanup.
This addresses a few points from #479.
* doc/org/ltlsynt.tex: New file.
* doc/Makefile.am: Add it.
* doc/org/ltlsynt.org: Show the architecture, and mention more
options.
* bin/spot-x.cc: Document ltlsynt's -x options.
* bin/ltlsynt.cc: Fix default value of --aiger, and typo in its
documentation.
* spot/tl/simplify.cc (tl_simplifier_cache::as_bdd): Fix the order in
which as_bdd() is called recursively in binary nodes, do not let the
choice to the compiler.
* tests/core/ltlsynt.test: Adjust expected output.
* spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh (acd::build_):
When processing a node identical to a node previously seen, simply
copy the children of that other node, and share its vectors.
* doc/org/tut40.org: Add more explanations and some cleanup.
* python/spot/__init__.py (set_state_players, get_state_winners,
get_state_players, set_state_player, get_state_winner,
get_state_player, get_strategy): Add these methods to the twa_graph
class for convenience.
* NEWS, doc/org/tut.org: Mention tut40.org.
* doc/org/tut40.org: Add a documentation on how to use games in a
pratical case. In this example, we compute simulation using
games. Fixes#445.
* doc/Makefile.am: Add tut40.org.
* spot/twaalgos/dtwasat.cc: Do not return a transition-based automaton
when state-based output is requested.
* tests/python/satmin.ipynb, spot/twaalgos/dtbasat.hh: Fix some typos.
* tests/python/satmin.py: Add test cases.
* NEWS: Mention the bugs.
* spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh: Add the
acd_options::ORDER_HEURISTIC and use it by default in
acd_transform_sbacc().
* spot/misc/bitvect.hh (bitvect::count, bitvect::add_common): New
methods.
* tests/python/zlktree.ipynb: Adjust examples and discuss this
heuristic.
Removing this option to guarante that all arenas
are alternating
* spot/twaalgos/synthesis.hh: Here
* spot/twaalgos/synthesis.cc: Here
* spot/twaalgos/mealy_machine.cc: API change
* tests/python/aiger.py: API change
* tests/python/mealy.py: API change
* tests/python/split.py: API change
Fixes#477.
* bin/common_finput.cc (job_processor::process_string): Fix return
value.
* bin/ltlsynt.cc: Fix handling of syntax errors. While we are here,
make sure game_info is destroyed before Spot's globals.
* tests/core/ltlsynt.test: Add a test case.
These occur when Spot is compiled with --enable-optimizations and
--disable-assert.
* spot/mc/unionfind.cc, spot/twaalgos/mealy_machine.cc,
spot/twaalgos/aiger.cc: Work around warnings about variables that are
only used in assert.
* spot/misc/common.hh [NDEBUG] (SPOT_ASSUME): Do not define
as assert() when it is disabled.
* spot/twaalgos/alternation.cc: Use insert instead of emplace
to work around a spurious possible nullptr dereference.
* spot/twaalgos/ltl2taa.cc, spot/twaalgos/ndfs_result.hxx,
spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc:
Work around spurious possible nullptr dereference.
* spot/twaalgos/sbacc.cc: Work around spurious "maybe uninitialized"
warning.
By default only propositions appearing in the strategy are
treated. By handing over propositions explicitly one
can force their appearance in the aig circuit.
* spot/twaalgos/aiger.cc: Here
* spot/twaalgos/aiger.hh: New doc
* tests/python/games.ipynb: New test
