* spot/ltsmin/ltsmin.cc,
spot/mc/ec.hh, spot/mc/intersect.hh,
spot/mc/reachability.hh, spot/mc/unionfind.cc,
spot/mc/utils.hh, spot/twacube/cube.cc,
spot/twacube/twacube.cc,
spot/twacube/twacube.hh,
spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh,
tests/core/bricks.cc,
tests/core/cube.cc,
tests/core/twacube.cc,
tests/ltsmin/modelcheck.cc: here.

* spot/ltsmin/ltsmin.cc: here.

* bricks/brick-hash.h, bricks/brick-shmem.h: here.

* Makefile.am, README, bricks/brick-assert.h,
bricks/brick-bitlevel.h, bricks/brick-hash.h,
bricks/brick-hashset.h, bricks/brick-shmem.h,
bricks/brick-types.h, configure.ac,
debian/copyright, debian/libspot-dev.install,
m4/bricks.m4, tests/Makefile.am,
tests/core/.gitignore, tests/core/bricks.cc: here.

* tests/Makefile.am, tests/ltsmin/check.test,
tests/ltsmin/finite.test, tests/ltsmin/finite2.test,
tests/ltsmin/kripke.test, tests/ltsmin/modelcheck.cc: here.

Warning! this patch introduces redundancy (or difference)
between wether you ask for a kripkecube or a kripke.

* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh: here.

* spot/mc/Makefile.am, spot/mc/utils.hh: here.

In order to reuse the computation of the
intersection between kripke and twa efficiently,
we use template inheritance through the
"mixin templates" technique.

* spot/Makefile.am, spot/mc/Makefile.am,
spot/mc/ec.hh, spot/mc/unionfind.cc,
spot/mc/unionfind.hh: here.

* spot/mc/Makefile.am, spot/mc/intersect.hh: here.

* README, configure.ac, spot/mc/Makefile.am,
spot/mc/reachability.hh: here.

* spot/kripke/kripke.hh: here.

* spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
tests/core/twacube.cc, tests/core/twacube.test: here.

* spot/twacube/Makefile.am, spot/twacube/twacube.cc,
spot/twacube/twacube.hh, spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh, tests/Makefile.am,
tests/core/.gitignore, tests/core/twacube.cc,
tests/core/twacube.test: here.

* README, configure.ac, spot/Makefile.am,
spot/twacube_algos/Makefile.am, spot/twacube_algos/convert.cc
spot/twacube_algos/convert.hh, tests/core/cube.cc,
tests/core/cube.test: here.

* README, configure.ac, spot/Makefile.am,
spot/twacube/Makefile.am, spot/twacube/cube.cc,
spot/twacube/cube.hh, tests/Makefile.am,
tests/core/.gitignore, tests/core/cube.cc,
tests/core/cube.test: here.

* spot/tl/simplify.hh, spot/tl/simplify.cc,
spot/twaalgos/translate.cc: Update the tl_simplification
options after all preferences have been given.
* bin/ltlsynt.cc: Display the size of the translation output.
* tests/core/ltlsynt.test: Add test case.

* spot/tl/formula.hh: Add variant of formula::is that support 4
arguments.
* spot/tl/simplify.hh, spot/tl/simplify.cc: Add option keep_top_xor
to preserve Xor and Equiv at the top-level.
* spot/twaalgos/translate.cc: Adjust ltl-split to deal with Xor and
Equiv for the -D -G case.
* NEWS: Mention that.
* tests/core/ltl2tgba2.test: Add test case.
* tests/python/simstate.py: Adjust expected result.

* spot/twaalgos/product.cc, spot/twaalgos/product.hh: Add those
functions.
* tests/python/_product_weak.ipynb, tests/python/except.py: Test them.
* NEWS: Mention them.

* configure.ac, doc/org/setup.org, NEWS: Set version to 2.9.

It seems clang now warn about fallthrough case statements in C, but
ignore any /* fall through */ comment if that comes from a macro.

* src/bddop.c: Use the fallthrough attribute if available.

* bin/ltlsynt.cc: Add a --csv option to record the
duration of the various phases.
* tests/core/ltlsynt.test: Test the new option.
* NEWS: Mention it.

* spot/twaalgos/dot.cc: Add support for option 'E', and default to
rectangle nodes for large labels.
* bin/common_aoutput.cc, NEWS: Document it.
* tests/core/alternating.test, tests/core/dstar.test,
tests/core/readsave.test, tests/core/sccdot.test,
tests/core/tgbagraph.test, tests/python/_product_weak.ipynb,
tests/python/alternation.ipynb, tests/python/atva16-fig2b.ipynb,
tests/python/automata.ipynb, tests/python/decompose.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
tests/python/parity.ipynb, tests/python/pdegen.py,
tests/python/satmin.ipynb, tests/python/stutter-inv.ipynb: Adjust all
test cases.

* spot/twaalgos/dot.cc: Add tooltips to "..." states and edges.
* tests/core/readsave.test: Test this.
* tests/python/highlighting.ipynb: Adjust.

* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/translate.cc: Introduce a gen-reduce-parity option and
use it on sub-automata built by ltl-split.
* bin/spot-x.cc: Document it.
* tests/core/ltl2tgba2.test: Add test case reported by Juraj Major.

* bin/ltlsynt.cc: Make sure to_parity_old() receive a deterministic
automaton, for correctness.   Also call reduce_parity() afterward,
to match what was done in 2.8.7.
* tests/core/ltlsynt.test: Include lar.old in the comparison of all
results to make sure it give the same result as the other 3
algorithms.

* bin/ltlsynt.cc: Add support for --algo=lar.old
* NEWS: Mention it.

count() may be implemented using a loop, so using it touch
check count() == 1 or count() > 1 is not advisable.

* spot/twa/acc.hh (mark_t::is_singleton, mark_t::has_many): Introduce
these two methods to replace count()==1 and count()>1
* spot/twa/acc.cc, spot/twaalgos/cleanacc.cc,
spot/twaalgos/determinize.cc, spot/twaalgos/dtwasat.cc,
spot/twaalgos/iscolored.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/toparity.cc: Adjust usage.

* spot/twaalgos/cleanacc.cc (remove_compl_rec): Rewrite to preserve
the original order of the acceptance condition while rewriting it.
* tests/core/sccdot.test, tests/python/merge.py,
tests/python/simplacc.py, tests/python/toparity.py: Adjust test cases.

Florian Renkin authored Apr 18, 2020 and Alexandre Duret-Lutz committed Apr 18, 2020

* spot/twa/acc.cc: Here.
* tests/core/acc.cc, tests/core/acc.test, tests/core/remfin.test:
Update tests.

Florian Renkin authored Apr 18, 2020 and Alexandre Duret-Lutz committed Apr 18, 2020

* spot/twaalgos/toparity.cc: Don't use the same color for every edges
when the condition is "true" or "false" after parity prefix.

* python/spot/__init__.py (to_options): Do not have options
explicitely default to to_parity_options(), because that would be
instantiated only once.

Calling reduce_parity() in to_parity() is confusing, because then
running to_parity() on one SCC does not necessarily produce the same
output as running to_parity() on the entire automaton.  However it is
necessary for the implementation of parity_prefix.  As a compromise,
disable reduce_parity() when parity_prefix is disabled, this way we
can use that to demonstrate how the algorithm works.

* spot/twaalgos/toparity.hh, spot/twaalgos/toparity.cc: Do not
call reduce_parity() when parity_prefix is disabled.
* tests/python/toparity.py: Adjust.

* spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Run the
simplifications in a loop until the condition does not change anymore.
* tests/python/simplacc.py, tests/core/accsimpl.test,
tests/core/remfin.test, tests/python/merge.py,
tests/python/simplacc.py, tests/python/toparity.py: Update expected
results.
* tests/python/automata.ipynb: Update the failing example to a more
interesting one, matching the one in doc/org/autfilt.org.

* spot/twaalgos/cleanacc.cc (fuse_mark_here): Fix incorrect cancelling
of n-ary subterms, causing an invalid acceptance condition, and then
an infinite loop.
* tests/python/simplacc.py: Add test case.

* tests/python/toparity.py: here.

* spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh:
Don't try to run the algorithm without degeneralization
with the option force_degen.

* spot/twaalgos/toparity.cc: Remove merge_states.
* tests/python/automata.ipynb, tests/python/toparity.py: Update tests.