Based on a report by Simon Jantsch. Fixes#362.
* NEWS, doc/tl/tl.tex: Mention the new rules.
* spot/tl/unabbrev.cc: Implement them.
* tests/core/unabbrevwm.test: Test them.
* tests/python/randltl.ipynb: Adjust.
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.
This prevents an exception from being raised if NNF is not performed
on Boolean properties and implication-based checks are used.
* NEWS: Mention the issue.
* spot/tl/simplify.cc, doc/tl/tl.tex: Add some rules.
* tests/python/ltlsimple.py: Test them.
* spot/twaalgos/toparity.cc: here
* spot/twa/acc.hh, spot/twa/acc.cc: compute symmetries of an acceptance
condition
* tests/python/accparse2.py, tests/python/toparity.py: test it
* tests/core/ltl2tgba2.test: Add a test-case reported by Maximilien.
* spot/twaalgos/translate.cc: Translate any "safety" formula with
"rest".
* tests/python/highlighting.ipynb: Adjust.
Fixes#360.
* spot/twa/acc.cc, spot/twa/acc.hh (force_inf): New method.
* spot/twaalgos/genem.cc: Fix the emptiness check using force_inf.
* tests/python/genem.py: Add test case and adjust the python
version of the emptiness check.
* spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: implement it,
based on last-appearance record (LAR)
* spot/twaalgos/Makefile.am: build it
* NEWS: document it
* python/spot/impl.i: add to python bindings
* tests/Makefile.am, tests/python/toparity.py: test it
* spot/twa/acc.cc, spot/twa/acc.hh (fin_unit, one_fin): New function.
* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: New files.
* spot/twaalgos/Makefile.am: Add it.
* tests/python/genem.py: New file.
* tests/Makefile.am: Add it.
* python/spot/impl.i: Add bindings for genem.hh.
* NEWS: Mention the new function.
* tests/python/ipnbdoctest.py: Invert diffs inputs.
* tests/run.in: Run notebooks with
PYTHONIOENCODING=utf-8:surrogateescape to avoid exceptions when trying
to display utf-8 characters on ascii terminals.
* spot/graph/graph.hh, spot/twa/twagraph.hh, spot/twa/twagraph.cc:
Implement a dump_storage_as_dot() method.
* python/spot/__init__.py (twa_graph.show_storage): New method, above
dump_storage_as_dot().
* tests/python/twagraph-internals.ipynb: New file, with documentation
about the twa_graph internals, using show_storage() to illustrate
everything.
* tests/Makefile.am, doc/org/tut.org: Add it.
* python/spot/impl.i: Add bindings for out_iterasor, demonstrated in
the Python notebook.
* spot/twa/twa.hh: Add prop_reset(). Used in the notebook.
* NEWS: Mention the new notebook and function.
* doc/org/tut50.org: Link to the notebook.
* tests/python/ipnbdoctest.py: Adjust for twa_graph_ptr being
redefined in the spot namespace.
Hopefully fixes#359.
* spot/misc/trival.hh: Declare a global operator==(trival,trival) that
replace the specialized operator==(bool,trival), and the in class
trival::operator(trival), thanks to the implicit construction from
bool to trival. Make the repr_t/value_t constructor explicit, are
those are mostly internal to the library and may cause conflicts.
* spot/twa/twa.hh: Adjust to construct trival explicitly.
* python/spot/impl.i: Since Swig/Python does not support global
comparison operators, implement a member version, supporting
only __eq__(trival,bool) as before.
* tests/python/setacc.py: Adjust erroneous code.
* tests/python/trival.py: Add test cases.
* spot/twaalgos/isdet.cc,spot/twaalgos/isdet.hh: Two new functions to
highlight deterministic SCCs
* spot/twaalgos/complement.cc,spot/twaalgos/complement.hh:
Implementation of the NCSB complementation algorithm
* tests/Makefile.am, tests/python/complement_semidet.py: Test the
implementation
* NEWS: document function
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/postproc.cc: Here.
* spot/twaalgos/cobuchi.cc, spot/twaalgos/totgba.cc: Fix some bug
uncovered by the new simplified automata.
* tests/core/satmin2.test, tests/core/sccdot.test,
tests/core/sim3.test, tests/python/decompose.ipynb,
tests/python/satmin.ipynb: Update expected results.
* NEWS: Mention the simplification and the bug.
* 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.
* spot/twaalgos/product.cc, spot/twaalgos/product.hh: Implement it.
* tests/python/_product_susp.ipynb: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention it.
Related to issue #351.
* spot/twaalgos/sccfilter.cc: When handling weak automata, we know
they are very-weak if the SCC count is equal to the number of states.
* tests/core/dca2.test, tests/core/monitor.test,
tests/core/parity2.test, tests/core/randomize.test,
tests/core/readsave.test, tests/core/remfin.test,
tests/core/sccsimpl.test, tests/core/wdba2.test,
tests/python/dualize.py, tests/python/remfin.py: Adjust output.
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.
When dealternating the VWAA for GFa, our result had two states that
could not be fused by simulation because of unmatched acceptance mark.
With this change, the result can be simplified.
* spot/twaalgos/alternation.cc: Here.
* tests/core/alternating.test, tests/python/alternation.ipynb: Update
test case.
* NEWS: Mention it.
* spot/misc/bitset.cc, spot/misc/bitset.hh (set, clear):
Turn asserts into exceptions.
* spot/twa/acc.hh (mark_t): As a consequence, the
constructor is not noexcept anymore.
* tests/core/acc.cc, tests/python/except.py: More tests.
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.
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
As this pollutes the user's namespace.
* spot/tl/randomltl.hh: Use class-level enum and constexpr instead
of #define.
* spot/tl/randomltl.cc, python/spot/__init__.py, bin/randltl.cc,
tests/python/dualize.py, tests/python/sum.py: Adjust usage.
* spot/twaalgos/dot.cc: Here.
* NEWS, bin/common_aoutput.cc: Mention it.
* tests/python/ltsmin-pml.ipynb: Use it.
* tests/python/ipnbdoctest.py: Work around some graphviz
version differences.
* spot/twaalgos/contains.hh, spot/twaalgos/contains.cc: New files.
* spot/twaalgos/Makefile.am, python/spot/impl.i: Add them.
* python/spot/__init__.py: Also attach these functions as methods,
and support string arguments.
* tests/python/contains.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* bin/autfilt.cc, tests/python/streett_totgba.py, tests/python/sum.py,
tests/python/toweak.py: Use the new function.
* spot/twaalgos/gfguarantee.cc: Combine the last letter read
with the first one of the next pass when doing transition-based
acceptance. Also move the initial states to the source of any
accepting transition if the input is deterministic.
* tests/core/ltl2tgba2.test, tests/core/satmin.test,
tests/python/stutter-inv.ipynb: Reduce expected sizes of a few
automata.
Improve the way transitions are duplicated when preparing the turn-based
game for synthesis. The resulting arena should now be deterministic on
nodes owned by the environment. Also move the code to another file, so
that it is easier to test (e.g. in Python).
* bin/ltlsynt.cc: move the code
* spot/twaalgos/split.cc, spot/twaalgos/split.hh: move the code and
implement the improvements
* tests/Makefile.am, tests/python/split.py: test it
* tests/core/ltlsynt.test: update existing tests to reflect the changes
Fixes#327.
* spot/twaalgos/dot.cc: Emit a tooltip="..." for state names and
labels that are disabled by option "1".
* doc/org/tut51.org, tests/python/product.ipynb, NEWS: Discuss this.
* tests/core/readsave.test, tests/python/alternation.ipynb,
tests/python/automata.ipynb: Adjust test cases.
