* bin/autcross.cc: Let complement() decide how to complement automata.
Do not apply remove_fin(), because we have a generic emptiness check
now. Use intersecting_word() instead of product()+accepting_word() so
that the former can maybe be optimized in the future.
* tests/core/autcross2.test: Adjust test case to use TGBA instead
of monitors, as calling complement() had a side-effect of setting
the "weak" property on the input.
* 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.
* configure.ac: Test for <spawn.h>.
* bin/common_trans.cc: Use posix_spawn when available.
* NEWS: Mention the change.
* tests/core/ltldo.test: Adjust expected error message.
* spot/twaalgos/dot.cc: Implement support for hidding labels.
* tests/core/readsave.test: Test it.
* bin/common_aoutput.cc: Add --help text.
* NEWS: Mention it.
spot::contains(a, b) should test a⊇b. It was testing a⊆b instead.
* NEWS: Mention the bug.
* spot/twaalgos/contains.cc, spot/twaalgos/contains.hh: Fix the
code and documentation.
* tests/python/contains.ipynb: Adjust description and expected
results.
* python/spot/__init__.py: Also swap the argument of
language_containment_checker.contains()
* bin/autfilt.cc: Adjust usage.
ltlsynt now offers two algorithms: one where splitting occurs before
determinization (the historical one) and one where determinization
occurs before splitting.
* bin/ltlsynt.cc: here
* tests/core/ltlsynt.test: test it and refactor test file
* NEWS: document it
* spot/misc/game.hh, spot/misc/game.cc: remove Calude's algorithm
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.
* doc/org/tools.org: Adjust the link to ltl2tgba.org.
* doc/org/ltl2tgba.org: Also point out that --generic and --parity can
be used without --deterministic.
* bin/ltl2tgba.cc, bin/spot.cc: Adjust help text.
* 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.
Together with the previous patch, this Fixes#353.
Implementing this required to extend our interface two support
two-parameter patterns.
* spot/gen/formulas.cc, spot/gen/formulas.hh: Implement it.
* bin/genltl.cc: Add --sejk-f.
* bin/common_output.cc, bin/common_output.hh: Adjust to handle
"line numbers" that are not integers (e.g., "3,2"), since those
are used to display pattern parameters.
* bin/ltlfilt.cc: Adjust.
* python/spot/gen.i: Add support for two-parameters patterns.
* tests/core/genltl.test, tests/python/gen.ipynb: Augment.
* NEWS: Mention it.
These correspond to the first three blocks of table 1 in S. Sickert,
J. Esparza, S. Jaax, and J. Křetínský: Limit-Deterministic Büchi
Automata for Linear Temporal Logic. CAV'16. LNCS 9780.
For #353.
* spot/gen/formulas.cc, spot/gen/formulas.hh, bin/genltl.cc: Implement
the new families.
* tests/core/genltl.test: Test it.
* bin/man/genltl.x, NEWS: Document it.
The exception raised by << and >> when shifting mark_t by too many
bits are only enabled in SPOT_DEBUG, as those operations are quite
low-level. However we were always testing them, and although we
wanted them to be active in Python, it was not always the case.
* spot/twa/acc.hh: introduce max_accsets() as
a static constexpr method, so we can see it in Python.
* spot/misc/bitset.hh: Fix preprocessing directive
so the check is actually enabled when compiling the Python
bindings.
* bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc: Use max_accsets().
* tests/core/acc.cc: Comment out the shifting exception when
SPOT_DEBUG is unset.
* tests/python/except.py: Make sure the exception is always raised in
Python.
Fixes#348, reported by Jeroen Meijer.
* bin/autfilt.cc: If -B is used with many --product,
degeneralize intermediate products as needed.
* NEWS: Mention the change.
* tests/core/prodchain.test: New file.
* tests/Makefile.am: Add it.
* spot/twa/acc.cc, spot/twa/acc.hh: Fix reporting of
overflow.
* tests/core/acc.cc: Adjust.
This allows to represent more than 32 acceptance marks.
* configure.ac: add an option to specify the number of marks
* spot/twa/acc.hh: implement it
* tests/python/acc_cond.ipynb, tests/core/acc.cc,
tests/core/ltlcross3.test: update tests
* NEWS: document it
* bin/randltl.cc: fix an include
* bin/common_conv.cc, bin/common_conv.hh: Here.
* bin/autfilt.cc, bin/common_trans.cc, bin/ltlcross.cc, bin/ltldo.cc,
bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randaut.cc, bin/randltl.cc: Pass
the name of the argumennt to the conversion function.
* tests/core/ltlcross3.test, tests/core/ltldo.test,
tests/core/randaut.test: Add test cases.
* bin/common_hoaread.hh (hoa_processor): Add a abort_on_error
option.
* bin/autcross.cc: Use it.
* tests/core/autcross4.test: Add many more error cases to improve
coverage.
This also improve the coverage of the is_colored() function, because
it was not used in negative cases so far.
* bin/autfilt.cc: Implement it.
* tests/core/satmin2.test: Test it.
* NEWS: Mention it.
* bin/common_setup.cc, bin/common_setup.hh: Define a protected_main()
function that deal with exceptions.
* bin/autcross.cc, bin/autfilt.cc, bin/dstar2tgba.cc, bin/genaut.cc,
bin/genltl.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc,
bin/ltldo.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/ltlsynt.cc,
bin/randaut.cc, bin/randltl.cc: Use it for all tools.
