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.
* 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::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.
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
* 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.
* NEWS, doc/tl/tl.tex, doc/tl/tl.bib: Document these new operators.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse those.
* spot/tl/formula.cc, spot/tl/formula.hh: Add constructors.
* spot/gen/formulas.cc: Use it.
* tests/core/sugar.test: New file.
* tests/Makefile.am: Add it.
