* doc/org/oaut.org: Here.

* NEWS, configure.ac, doc/org/setup.org: Bump version.

Clément Gillard authored Apr 18, 2017 and Alexandre Duret-Lutz committed Sep 05, 2017

* bin/autfilt.cc, python/spot/__init__.py, spot/twa/twa.hh,
spot/twa/twaproduct.cc, spot/twaalgos/couvreurnew.cc,
tests/python/bugdet.py: Here.

* spot/twaalgos/dot.cc: Implement.
* doc/org/oaut.org: Illustrate.
* tests/core/dot2tex.test: Add some limited 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.

* doc/org/genaut.org: Output the result for the last example.

* spot/gen/automata.cc, spot/gen/automata.hh, bin/genaut.cc: Rename
the enum, function, and command-line option.
* tests/core/genaut.test, tests/python/gen.ipynb, tests/python/gen.py:
Adjust test cases.
* doc/org/genaut.org: Adjust doc.

This addresses part of #35, and is just a generalization of the rules
from 646c5170 for #263 (hence, no new documentation).

* spot/tl/simplify.cc: Implement this.
* tests/core/reduccmp.test: Add test cases.
* tests/core/stutter-tgba.test: Adjust to expect smaller automata.

Fixes #108.

* spot/tl/simplify.cc: Implement the reduction.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/reduccmp.test: Test it.

Fixes #277.

* spot/twaalgos/ltl2tgba_fm.cc: Improve the translation of f U g
when f is universal.  Suggested by Maximilien Colange.
* tests/core/ltl2tgba.test: Test it.

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.

For #263, reported by Mikuláš Klokočka.

G(a & Xe1 & F(b & e2)) = G(a & e1 & Fb & e2)
F(a | Xu1 | G(b | u2)) = F(a | u1 | Gb | u2)

* spot/tl/simplify.cc: Implement the rules.
* doc/tl/tl.tex, NEWS: Document them.
* tests/core/reduccmp.test, tests/core/eventuniv.test: Add test cases.
* tests/core/det.test, tests/core/ltl2tgba2.test: Adjust to expect
smaller automata.
* THANKS: Add Mikuláš.

* spot/priv/enumflags.hh: Delete.
* spot/priv/Makefile.am, debian/copyright: Adjust.
* spot/twaalgos/remfin.cc: Replace the complex enum
definition by a plain enum that is almost not used.

* spot/twaalgos/remfin.cc (remove_fin_impl): Apply the Rabin strategy
before the Streett one.

The generalization to Streett-like of 7b5b8f34 was incomplete for this
case.  Thanks to František Blahoudek for reporting the bug.
Fixes #279.

* spot/twaalgos/totgba.cc (streett_to_generalized_buchi): Here.
* tests/core/remfin.test: Add more tests.

This is probably an environment variable definition.

* bin/common_trans.cc: Here.  A use-case appears in the test of the
next patch.

* 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/twaalgos/dot.cc (print_acceptance_for_human): Add Rabin-like
and Streett-like checks.
* tests/core/sccdot.test, tests/python/decompose.ipynb,
tests/python/randaut.ipynb, tests/core/alternating.test: Adjust.

* doc/org/csv.org: Mention that %h must be double-quoted in CSV output.

* tests/python/dualize.py: test that an automaton and its dual have
  complementary languages.

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

* NEWS, doc/org/concepts.org, doc/org/hierarchy.org,
  spot/misc/optionmap.hh, spot/twa/acc.hh, spot/twaalgos/ltl2tgba_fm.hh,
  spot/twaalgos/sccinfo.hh, spot/twaalgos/translate.cc: fix typos

* 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.

* configure.ac: Here.  Rename --enable-c++14 into --enable-c++17.

* doc/org/arch.tex: Add autcross.
* tests/sanity/bin.test: Make sure all binaries appear in arch.tex.

* spot/twaalgos/dot.cc: Display common acceptance names.
* NEWS: Mention the change.
* doc/org/oaut.org: Adjust text.
* tests/core/alternating.test, tests/core/readsave.test,
tests/python/_altscc.ipynb, tests/python/alternation.ipynb,
tests/python/atva16-fig2a.ipynb, tests/python/atva16-fig2b.ipynb,
tests/python/automata.ipynb, tests/python/decompose.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb: Adjust test
cases.

Bug introduced in abe2c08b, visible in tests/python/product.ipynb,
and tests/python/acc_cond.ipynb.

* spot/twa/acc.hh: fix operator| and operator&.
* tests/python/acc_cond.ipynb: Adjust test case.

* spot/tl/hierarchy.cc (is_recurrence): Do not request state-based
acceptance, now that the Rabin->DBA conversionn works on
transition-based acceptance as well.

* doc/org/hierarchy.org: Update with small typos, and
notes about tra2tba.

* spot/twaalgos/remfin.cc (tra_to_tba, is_scc_tba_type): Here.

Fixes #278. Also adds a test ensuring non-regression.

* spot/twaalgos/toweak.cc: Fixes the bug.
* tests/python/toweak.py: Add a test case.

* 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.

* NEWS, spot/twaalgos/dualize.cc, spot/twaalgos/dualize.hh,
  spot/twaalgos/langmap.cc, spot/twaalgos/sum.hh,
  tests/python/streett_totgba.py: Fixes typo.