Fixes#284, reported by Juraj Major.
* spot/twaalgos/totgba.cc: Fix the algorithm.
* spot/twa/acc.hh: More doc for future generations.
* tests/core/scc.test: More test cases.
* NEWS: Mention the issues.
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.
Fixes#282.
* spot/misc/bddlt.hh (bdd_less_than_stable): New function.
* spot/twa/twagraph.cc (merge_edges): Use it.
* tests/core/genltl.test: Adjust, and add an extra test
for the behavior of #282.
* tests/core/complement.test, tests/core/degenid.test,
tests/core/ltldo.test, tests/core/prodor.test,
tests/core/readsave.test, tests/core/sbacc.test,
tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
tests/python/decompose.ipynb, tests/python/dualize.py,
tests/python/highlighting.ipynb, tests/python/piperead.ipynb,
tests/python/product.ipynb, tests/python/simstate.py,
tests/python/tra2tba.py: Adjust all expected outputs.
* NEWS: Mention the bug.
* 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.
scc_info::used_acc() and spot::info::used_acc_of() have been renamed to
scc_info::marks() and scc_info::marks_of().
scc_info::acc() has been renamed to (the already existing and redundant)
scc_info::acc_sets_of().
Old names have been deprecated.
* spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: implement it.
* spot/twaalgos/dtwasat.cc, spot/twaalgos/isweakscc.cc,
spot/twaalgos/remfin.cc, spot/twaalgos/sccfilter.cc: update names.
* NEWS: documentate it.
* 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.
* spot/twa/acc.cc, spot/twa/acc.hh: Add a LaTeX output for acceptance
conditions.
* spot/twaalgos/dot.cc: Implement the 'x' option and refactor the code
a bit to limit duplication.
* tests/core/dot2tex.test: New test case (requires dot2tex).
* tests/Makefile.am: Add dot2tex.test.
* tests/core/alternating.test, tests/core/readsave.test,
tests/python/automata-io.ipynb: Adjust expected output.
* NEWS, doc/org/oaut.org: Mention the new option.
This way in 2.5 we can make 'a' the default, and tell people to use
SPOT_DOTDEFAULT=A if they want the old behavior in both 2.4 and 2.5.
* spot/twaalgos/dot.cc: Implement the option.
* NEWS, bin/common_aoutput.cc: Mention it.
* tests/core/readsave.test: Test it.
spot.complete() could complete an empty co-Büchi automaton into an
automaton accepting everything.
* NEWS: Document it
* spot/twaalgos/complete.cc: Fix it
* tests/core/complete.test, tests/core/prodor.test: Test it
* configure.ac: Compile in C++14 by default and rename
--enable-c++14 as c++17.
* doc/org/compile.org, doc/org/concepts.org, doc/org/index.org,
doc/org/install.org, doc/org/tut.org, doc/org/upgrade2.org, HACKING,
NEWS, README: Adjust all mentions of C++11.
* spot/twaalgos/stats.hh: Use std::make_unique.
* spot/twaalgos/remfin.cc: If no Inf set is used, set sbacc early so
that it is used in the algorithm.
* tests/core/remfin.test: Add more tests.
* NEWS: Mention the bug.
* spot/parseaut/parseaut.yy, spot/parseaut/parsedecl.hh,
spot/parseaut/public.hh, spot/parseaut/scanaut.ll: Use a reentrant
scanner, so that we can now parse multiple automaton streams at the
same time. This is needed for the future autcross, which is going to
read several individual automata produced by different tools, while
reading the stream of automata to process.
Operator &= used to always move Fin to the front, it does not anymore.
The only thing it does now is to merge Inf(x)&Inf(y) as Inf({x,y}).
Operator |= is now symmetrical and merges Fin()s.
Fixes#253.
* spot/twa/acc.cc, spot/twa/acc.hh: Simplify &= and make |= symmetrical.
* spot/twaalgos/cleanacc.cc: Fix conjunction order.
* tests/core/acc.test, tests/core/acc2.test, tests/core/parseaut.test,
tests/core/readsave.test, tests/core/satmin2.test,
tests/core/sccdot.test, tests/python/acc_cond.ipynb,
tests/python/accparse.ipynb, tests/python/automata.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
cases.
* NEWS: mention the modification.
* python/spot/impl.i: makes to_weak_alternating visible from python
* spot/twaalgos/Makefile.am, spot/twaalgos/toweak.cc,
spot/twaalgos/toweak.hh: Implements to_weak_alternating.
* tests/Makefile.am, tests/python/toweak.py: Test the results of
to_weak_alternating.
These two functions were doing almost identical work, the only
difference was the way to select the SCC to keep. Now we have a more
uniform way to do that. Closes#172.
* bin/autfilt.cc: Offer a unique --decompose-scc option, but keep
--decompose-strength as an alias for backward compatibility.
* spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: Rename
decompose_strength as decompose_scc, and handle a way to list
all SCC numers in the string specifier. This gets rid
of the nearly identical
* tests/core/scc.test, tests/core/strength.test,
tests/python/decompose.ipynb, tests/python/decompose_scc.py: Adjust
test cases.
* NEWS: Adjust.
