* spot/twaalgos/cobuchi.cc, spot/twaalgos/cobuchi.hh (to_nca): New
function.
(weak_to_cobuchi): New internal function, used in to_nca and to_dca
when appropriate.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Implement
the CoBuchi option.
* python/spot/__init__.py: Support it in Python.
* bin/common_post.cc: Add support for --buchi.
* bin/autfilt.cc: Remove the --dca option.
* tests/core/dca.test, tests/python/automata.ipynb: Adjust and add
more tests. In particular, add more complex persistence and
recurrence formulas to the list of dca.test.
* tests/python/dca.test: Adjust and rename to...
* tests/core/dca2.test: ... this. Add more tests, to the point
that this is now failing, as described in issue #317.
* tests/python/dca.py: Remove.
* tests/Makefile.am: Adjust.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Add support
for a colored option.
* bin/common_post.cc, bin/common_post.hh bin/autfilt.cc,
bin/ltl2tgba.cc, bin/dstar2tgba.cc: Add support for --colored-parity.
* bin/ltldo.cc: Adjust as well for consistency, even if --parity and
--colored-parity is not used here.
* tests/core/parity2.test: Add tests.
* doc/org/autfilt.org, doc/org/ltl2tgba.org: Add examples.
* NEWS: Mention --colored-parity.
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Add parity
options.
* bin/common_post.cc: Add support for --parity.
* NEWS: Mention it.
* tests/core/parity2.test: New file.
* tests/Makefile.am: Add it.
Reported by František Blahoudek.
* bin/man/ltlcross.x: Remove obsolete paragraph with reference to
columns in_states, in_edges, in_transitions, and in_acc that
were removed in 1.99.3.
* spot/tl/hierarchy.hh, spot/tl/hierarchy.cc (nesting_depth): New
function.
* python/spot/__init__.py: Also make it a method of formula in Python
* bin/common_output.cc, bin/common_output.hh: Implement
--stats=%[OP]n.
* NEWS: Mention it.
* tests/core/format.test, tests/python/formulas.ipynb: Test it.
We currently have 3 printable_formula classes in Spot; let's reduce
this to 2.
* bin/common_output.cc (anonymous::printable_formula): Rename to...
(anonymous::printable_formula_with_location): ... this.
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
This is not optimal yet because it still construct a minimal WDBA
internally, but it's better than the previous way to call
minimize_obligation() since it can avoid constructing the minimized
automaton in a few more cases.
* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: Introduce
is_obligation().
* bin/ltlfilt.cc: Wire it to --obligation.
* spot/twaalgos/minimize.cc: Implement is_wdba_realizable(),
needed by the above.
* tests/core/obligation.test: Test it.
* bin/man/spot-x.x, NEWS: Document it.
Fixes#289.
* spot/twaalgos/stats.cc, spot/twaalgos/stats.hh,
bin/common_aoutput.cc, bin/common_aoutput.hh: plug %g and %G into
acc_cond::name() when arguments are given as %[arg]g. or %[arg]G.
* tests/core/acc2.test: Add test case.
* doc/org/randaut.org, NEWS: Document it.
Suggested by Tobias Meggendorfer. Fixes#295.
* bin/ltlcross.cc, bin/common_trans.hh, bin/common_trans.cc: Implement
this --reference option.
* NEWS, doc/org/ltlcross.org: Document it.
* tests/core/ltlcross3.test: Test it.
This is long overdue, and we probably want to use tls-impl=1 in
ltlsynt.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh:
Add support for tls-impl=N.
* tests/core/ltl2tgba.test: Test it.
* bin/spot-x.cc, NEWS: Document it.
* spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Add an optional
argument to abort on accepting SCC, to not keep track of SCC states,
and some one_accepting_scc() method.
* NEWS: Mention it.
* bin/ltlcross.cc, spot/twaalgos/alternation.cc,
spot/twaalgos/cobuchi.cc, spot/twaalgos/degen.cc,
spot/twaalgos/determinize.cc, spot/twaalgos/dtbasat.cc,
spot/twaalgos/dtwasat.cc, spot/twaalgos/isunamb.cc,
spot/twaalgos/powerset.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc,
spot/twaalgos/totgba.cc: Adjust arguments passed to scc_info.
Suggested by Maximilien Colange.
* spot/twaalgos/degen.cc: If the output has more SCC than the input,
detect useless SCCs and remove them.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/degen.hh: Add support for a degen-remscc option.
* bin/spot-x.cc, NEWS: Document it.
* tests/core/degenscc.test: New file.
* tests/Makefile.am: Add it.
* tests/core/det.test: Lower some expected size (yay!).
This also fixes some empty lines and unsorted options
that appeared in some tools.
* tests/sanity/bin.test: Ensure this is done.
* bin/README: Add a new paragraph about this.
* bin/autcross.cc, bin/ltlcross.cc: Move the
output options in their own section.
* bin/common_color.cc: Assume color options are
in group -15.
* bin/common_finput.cc, bin/common_finput.hh:
Add a headless variant.
* bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc,
bin/randaut.cc, bin/randltl.cc: Do not force the
children groups, so that the options are correctly sorted.
* bin/ltlsynt.cc: Add missing groups.
* spot/misc/game.cc, spot/misc/game.hh: Here.
* bin/ltlsynt.cc: Realizability is now done by checking if the winning
strategy contains the initial state.
For now, ltlsynt only handles LTL realizability. It uses a reduction to
parity game followed by Calude et al.'s reduction from parity game to
reachability game.
* bin/ltlsynt.cc, bin/Makefile.am, bin/man/ltlsynt.x,
bin/man/Makefile.am, bin/.gitignore: New binary.
* doc/org/arch.tex, doc/Makefile.am, doc/org/tools.org,
doc/org/ltlsynt.org: Document it.
* spot/misc/game.cc, spot/misc/game.hh, spot/misc/Makefile.am: Parity
game wrapper for parity automata + reachability game interface from
Calude et al.'s paper.
* NEWS: Update.
* spot/twaalgos/cobuchi.hh: Declare to_dca() and nsa_to_nca().
* spot/twaalgos/cobuchi.cc: Implement them.
* python/spot/impl.i: Include new file for python bindings.
* spot/twaalgos/Makefile.am: Add new file.
* bin/autfilt.cc: Add --dca command line option. This option does not
return a deterministic automaton yet, but it will.
* tests/core/dca.test: Add tests for Büchi automata.
* tests/python/dca.py: Add a python script that builds a nondet. Streett
automaton.
* tests/python/dca.test: Add tests for Streett automata.
* tests/Makefile.am: Add all tests.
* bin/common_output.cc: Make --stats an alias of --format.
* bin/common_aoutput.cc: Make --format an alias of --stats.
* tests/core/acc2.test, tests/core/format.test: Test these aliases.
* NEWS: Mention this.
As suggested in #263.
* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
these options.
* tests/core/genltl.test: Use them.
* NEWS: Mention them.
