* bin/man/spot-x.x, bin/spot-x.cc: Improve documentation of SAT-based
minimization. It was still referring to TGBA although it works for
TwA.
* spot/twaalgos/postproc.cc: Typo.
Also have simul-max default to 4096 instead of 512, because it's
really simul-trans-pruning that is very slow and need to be limited.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/simulation.cc, spot/twaalgos/simulation.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh:
Implement the above options.
* bin/spot-x.cc, NEWS: Document them.
* tests/core/ltlsynt.test, tests/core/minusx.test,
tests/core/sim3.test: Add some test cases.
* bin/man/spot-x.x, bin/spot-x.cc: Improve documentation of SAT-based
minimization. It was still referring to TGBA although it works for
TwA.
* spot/twaalgos/postproc.cc: Typo.
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Add the new simulation
in do_simul().
* bin/man/spot-x.x, bin/spot-x.cc: Add documentation for
SPOT_SIMULATION_REDUCTION environnement variable and the simul-method
fine tunning option.
* NEWS: Mention the changes.
This helped confirming a behavior observed in #298.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add support
for -x exprop.
* bin/spot-x.cc, NEWS: Document it.
* tests/core/ltl2tgba2.test: Test it.
This restricts the time spent in translating sub-formulas for
implication tests by limiting the associated automata to 64 states by
default. Doing so this does worsen any test case, and actually remove
all calls the BuDDy's GC in bdd.test.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh,
spot/tl/simplify.cc, spot/tl/simplify.hh, spot/tl/contain.hh,
spot/tl/contain.cc, spot/twaalgos/ltl2tgba_fm.cc,
spot/twaalgos/ltl2tgba_fm.hh: Add support for the option or
its constraint via an output_aborter.
* bin/spot-x.cc, NEWS: Document it.
* tests/core/bdd.test: Adjust and augment test case.
Fixes#15.
* spot/twaalgos/minimize.hh, spot/twaalgos/minimize.cc
(minimize_obligation_garanteed_to_work): New function.
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use it if
wdba-minimize=1. Handle new default for wdba-minimize.
* NEWS, bin/spot-x.cc: Document those changes.
* tests/core/ltl2tgba2.test: Add some test cases.
* tests/core/genltl.test: Improve expected results.
Fixes#15.
* spot/twaalgos/minimize.hh, spot/twaalgos/minimize.cc
(minimize_obligation_garanteed_to_work): New function.
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use it if
wdba-minimize=1. Handle new default for wdba-minimize.
* NEWS, bin/spot-x.cc: Document those changes.
* tests/core/ltl2tgba2.test: Add some test cases.
* tests/core/genltl.test: Improve expected results.
* 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.
* spot/twaalgos/alternation.cc, spot/twaalgos/alternation.hh,
spot/twaalgos/complement.cc, spot/twaalgos/complement.hh,
spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh,
spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh,
spot/twaalgos/product.cc, spot/twaalgos/product.hh: Use an
output_aborter argument to abort if the output is too large.
* bin/ltlcross.cc: Use complement() with an output_aborter
so that ltlcross will not attempt to build complement larger
than 500 states or 5000 edges. Add --determinize-max-states
and --determinize-max-edges options.
* tests/core/ltlcross3.test, tests/core/ltlcrossce2.test,
tests/core/sccsimpl.test, tests/core/wdba2.test,
tests/python/stutter-inv.ipynb: Adjust test cases.
* NEWS: Document this.
* bin/spot-x.cc: Add documentation for postprocessor's
det-max-states and det-max-edges arguments.
* doc/org/ltlcross.org: Update description.
Fixes#267
* spot/twaalgos/gfguarantee.cc: Fix a typo when comparing automata
sizes.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Use
ltl-split even for BA/TGBA, but only of conjunctions with GF(..)
in those cases.
* tests/core/ltl2tgba2.test: Adjust and add the example of #267.
* tests/core/degenid.test, tests/core/parity2.test,
tests/core/stutter-tgba.test, tests/python/automata.ipynb,
tests/python/highlighting.ipynb, tests/python/stutter-inv.ipynb,
bin/spot-x.cc: Adjust.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Build
automata with generic acceptance by doing product of automata for
smaller subformulas.
* bin/spot-x.cc: Mention ltl-split.
* NEWS: Mention the change, and show some results.
* tests/core/genltl.test, tests/python/_product_susp.ipynb,
tests/python/highlighting.ipynb: Adjust test cases.
* doc/org/ltl2tgba.org: Update.
* tests/core/gragsa.test: Add another formula to cover more
code.
This is adapted from a proposition in a paper by J. Esparza,
J. Křentínský, and S. Sickert, submitted to LICS'18. We should add
proper references to the code and documentation once that paper is
accepted.
* spot/twaalgos/gfguarantee.cc, spot/twaalgos/gfguarantee.hh:
New files.
* spot/twaalgos/Makefile.am, python/spot/impl.i: Add them.
* spot/twa/fwd.hh: Add a forward declaration of bdd_dict_ptr.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Make it
possible to call finalize() from the translator subclass. Constify
all the do_* functions while we are there.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add
a "gf-guarantee" option to decide whether to use the new translation.
* bin/spot-x.cc: Document it.
* tests/core/dca2.test, tests/core/genltl.test,
tests/core/ltl2tgba2.test, tests/core/parity2.test,
tests/core/satmin.test, tests/python/automata.ipynb,
tests/python/sbacc.py: Adjust test cases.
* tests/python/except.py: Add a couple more tests.
This is long overdue, and we probably want to use tls-impl=1 in
ltlsynt.
* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh:
Add support for tls-impl=N.
* tests/core/ltl2tgba.test: Test it.
* bin/spot-x.cc, NEWS: Document it.
Suggested by Maximilien Colange.
* spot/twaalgos/degen.cc: If the output has more SCC than the input,
detect useless SCCs and remove them.
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
spot/twaalgos/degen.hh: Add support for a degen-remscc option.
* bin/spot-x.cc, NEWS: Document it.
* tests/core/degenscc.test: New file.
* tests/Makefile.am: Add it.
* tests/core/det.test: Lower some expected size (yay!).
* spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh:
Add options det-scc, det-simul, det-stutter.
* bin/spot-x.cc: Document them.
* doc/org/ltl2tgba.org: Illustrate one of them and link
to the spot-x man page.
