* spot/twaalgos/translate.cc: When producing Parity output, split LTL
as we do in the Generic case.
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use
acd_transform() and add an "acd" option to disable this.
* bin/spot-x.cc, NEWS: Document this.
* tests/core/genltl.test, tests/core/minusx.test,
tests/core/parity2.test: Adjust test cases for improved outputs.
For issue #512
* README: Update instructions.
* configure.ac: Add some code to warn if Python files will be
installed in a place that is not searched up by default. Add
--with-pythondir support.
* NEWS: Mention --with-pythondir.
As LRDE is being renamed LRE, gitlab is one of the first URL to
migrate. The old URL is still supported, but we want to only use the
new one eventually.
* .dir-locals.el, .gitlab-ci.yml, HACKING, NEWS, doc/org/concepts.org,
doc/org/install.org, doc/org/setup.org, elisp/Makefile.am,
elisp/hoa-mode.el, tests/ltsmin/README: Update to the new gitlab URL.
Based on a mail from Edmond Irani Liu. The test case also serves for
the previous patch.
* bin/genltl.cc, spot/gen/formulas.cc, spot/gen/formulas.hh: Add it.
* NEWS: Mention it.
* tests/core/genltl.test: Test it.
This is motivated by an example sent by Edmond Irani Liu,
that will be tested in next patch.
* spot/twaalgos/dbranch.cc, spot/twaalgos/dbranch.hh: New files.
* python/spot/impl.i, spot/twaalgos/Makefile.am: Add them.
* spot/twaalgos/translate.cc: Call delay_branching_here
unconditionally.
* spot/twa/twagraph.cc (defrag_states): Do not assume
that games are alternating.
* tests/core/genltl.test: Adjust expected numbers.
* tests/python/dbranch.py: New file.
* tests/Makefile.am: Add it.
Typically intead of doing
minato_isop isop(rel & letter);
while (bdd cube = isop.next()) {
bdd res = bdd_exists(cube, ap)
...
}
do
minato_isop isop(bdd_relprod(rel, letter, ap);
while (bdd res = isop.next()) {
...
}
this way the existential quantification is done once at the same time
of the conjunction, and isop has fewer variable to work with.
* spot/twaalgos/alternation.cc, spot/twaalgos/dualize.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/toweak.cc: Here.
* bin/ltlsynt.cc: Implement these options.
* bin/common_aoutput.hh, bin/common_aoutput.cc (automaton_format_opt):
Make extern.
* NEWS: Mention the new options.
* doc/org/ltlsynt.org: Use dot output in documentation.
* tests/core/ltlsynt.test: Quick test of the new options.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Introduce a
merge-states-min option.
* bin/spot-x.cc: Document it.
* spot/gen/automata.cc, spot/gen/automata.hh, bin/genaut.cc: Add
option to generate cyclist test cases.
* NEWS: Document the above.
* tests/core/included.test: Add test cases that used to be too slow.
* spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Adjust
degeneralize() and degeneralize_tba() to work on generalized-co-Büchi.
* NEWS: Mention this.
* spot/twaalgos/cobuchi.hh, spot/twaalgos/cobuchi.cc (to_nca): Use
degeneralization on generalized-co-Büchi.
* spot/twaalgos/postproc.cc: Use degeneralization for generalized
co-Büchi as well.
* bin/autfilt.cc: Improve chain products of co-Büchi automata by using
generalization if too many colors are needed.
* tests/core/prodchain.test, tests/python/pdegen.py: Add test cases.
Improve the construction of the above constructions, saving colors.
* spot/twaalgos/product.cc: Here.
* spot/twaalgos/product.hh, NEWS: Mention it.
* tests/core/prodchain.test, tests/core/prodor.test,
tests/python/_product_weak.ipynb: Adjust.
* NEWS: Mention those change.
* spot/twaalgos/game.hh (print_pg): New function.
(pg_print): Mark as deprecated.
* spot/twaalgos/game.cc (pg_print): Redirect to print_pg().
(print_pg): Update to output state names.
* python/spot/__init__.py: Teach to_str() about print_pg().
* bin/ltlsynt.cc: Adjust to call print_pg().
* tests/python/games.ipynb: Add an example.
* tests/core/ltlsynt.test: Adjust to remove the "INIT" note.
* spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll: Add rules for
PGSolver's format.
* spot/parseaut/public.hh: PGAME is a new type of output.
* tests/core/pgsolver.test: New file.
* tests/Makefile.am: Add it.
* tests/python/games.ipynb: More exemples.
* NEWS: Mention the new feature.
* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: add detection
of edges that are in at least one accepting cycle.
* spot/twaalgos/toparity.cc,
spot/twaalgos/toparity.hh: add parity_type_to_parity and
buchi_type_to_buchi.
