* spot/twaalgos/sccinfo.cc: Here.
* tests/python/sccinfo.py: Test it.

* python/spot/__init__.py: Recognize if the input is already a
formula.
* tests/python/formulas.ipynb: Test this.

* spot/twaalgos/stutter.hh, spot/twaalgos/stutter.cc: Introduce
is_stutter_invariant_forward_closed and
make_stutter_invariant_forward_closed_inplace.
* tests/python/stutter-inv.ipynb: Use them.

* configure.ac, NEWS: Update to 2.4.3.dev.

* NEWS, configure.ac, doc/org/setup.org: Update.

* spot/twaalgos/isdet.hh, spot/twaalgos/isdet.cc (check_determinism):
New function.
* NEWS: Mention it.
* tests/python/semidet.py: New file.
* tests/Makefile.am: Add it.

* doc/org/install.org: Here.

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

* doc/footer.html: Make the footer XML compatible.
* doc/mainpage.dox: Fix references to modules.
* spot/tl/formula.hh: Introduce a hierarchy module.
* spot/tl/hierarchy.hh: Use it.

* doc/org/install.org: Here.

This prevented static compilation on MinGW.

* bin/common_setup.cc: Here.

* tests/python/ipnbdoctest.py: Here.  It seems importlib
does not load importlib.util anymore.

Maximilien Colange authored Nov 22, 2017 and Alexandre Duret-Lutz committed Nov 28, 2017

* tests/sanity/namedprop.test: fix typo for proper output

* spot/misc/bitvect.cc, spot/misc/bitvect.hh, spot/tl/formula.cc,
spot/tl/formula.hh: Here.
* NEWS: Mention the bug.

This only occurs when doing the emptiness check of twa with allocated
states.

* spot/twaalgos/couvreurnew.cc: Here.
* NEWS: Mention the bug.

* spot/twaalgos/couvreurnew.cc: explicit operator bool is not used by
return.

This prevented static compilation on MinGW.

* bin/common_setup.cc: Here.

* Makefile.am: move the doc subdirectory to its own variable

* tests/core/ltl2dstar.test: Reduce the amount of tests performed on
one formula that is problematic for ltl2dstar.

Our use of
  ltl2tgba=ltl2tgba
  autfilt=autfilt
  ...
all over the test cases comes from the time where those tools were not
in PATH and we actually had something like
  ltl2tgba=../../bin/ltl2tgba
  autfilt=../../bin/autfilt

But today that is useless, and we prefer to write ltl2tgba rather than
$ltl2tgba, so let's remove this old cruft.

* tests/core/basimul.test, tests/core/det.test, tests/core/lbt.test,
tests/core/lenient.test, tests/core/ltl2dstar.test,
tests/core/ltl2dstar2.test, tests/core/ltl2dstar3.test,
tests/core/ltl2dstar4.test, tests/core/ltlcross2.test,
tests/core/ltlcross3.test, tests/core/ltlcross4.test,
tests/core/ltlcrossce2.test, tests/core/ltldo.test,
tests/core/ltlfilt.test, tests/core/optba.test,
tests/core/prodor.test, tests/core/rand.test,
tests/core/randomize.test, tests/core/remfin.test,
tests/core/satmin.test, tests/core/sbacc.test,
tests/core/strength.test, tests/core/stutter-ltl.test,
tests/core/stutter-tgba.test, tests/core/unabbrevwm.test,
tests/core/unambig.test: Get rid of all tool=tool assignments.

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.

* debian/rules: Build it last.
* configure.ac: Add missing comma.

* tests/core/ltlsynt.test: Escape newlines and test PGsolver printer

* spot/twaalgos/determinize.cc: a lot of optimizations (and refactoring)

* tests/python/ipnbdoctest.py: skip test when jupyter is not found

Fixes #306.

* spot/tl/formula.hh, python/spot/__init__.py: Implement this
in C++ and Python.
* doc/org/tut03.org: Document (and indirectly test) it.
* NEWS: Mention it.

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

* doc/Makefile.am (dist-hook): Remove.
* HACKING: Adjust.

Fixes #307.

* spot/tl/formula.hh: Here.
* tests/python/ltlparse.py: Test it.
* NEWS: Mention it.

Fixes #299.

* configure.ac, doc/Makefile.am: Adjust.
* NEWS, HACKING, README: Document the change.
* doc/dot.in: Delete, not used anymore.
* doc/Doxyfile.in: Adjust to not look for dot.
* debian/rules: Use --enable-doxygen.

* tests/python/ipnbdoctest.py: Here.  It seems importlib
does not load importlib.util anymore.

* tests/python/dca.test: Do not assume the run script is in the source
directory.

Suggested in #299.

* doc/org/autfilt.org, doc/org/concepts.org, doc/org/dstar2tgba.org,
doc/org/genaut.org, doc/org/hierarchy.org, doc/org/hoa.org,
doc/org/ltl2tgba.org, doc/org/ltl2tgta.org, doc/org/ltlcross.org,
doc/org/oaut.org, doc/org/randaut.org, doc/org/satmin.org,
doc/org/tut11.org, doc/org/tut23.org, doc/org/tut24.org,
doc/org/tut30.org, doc/org/tut31.org, doc/org/tut50.org,
doc/org/tut51.org: Adjust all dot outputs to produce svg.
* doc/org/arch.tex, doc/org/hierarchy.tex, doc/org/satmin.tex: Adjust
to produce a pdf with 12pt text.
* doc/Makefile.am: Adjust the generation of arch.svg, hierarchy.svg,
and satmin.svg: From above.
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Adjust dot arguments
to produce svg with 12pt text (the default was 14pt).
* doc/org/spot.css: Use Lato as the main font for consistency with
automata.
* HACKING: pdf2svg is now required to build the doc.

Suggested in #299.

* doc/Doxyfile.in: Here.

* tests/sanity/namedprop.test: fix typo for proper output

* spot/tl/hierarchy.cc: Rewrite is_recurrence(), is_persistence()
* spot/tl/hierarchy.hh: Fix typo.
* tests/core/hierarchy.test: Add tests.