* NEWS: Mention the change.
* python/spot/__init__.py: Add _repr_latex_ for twa_word, and
remove __repr__ and __str__ for atomic_prop_set.
* python/spot/impl.i: Implement __repr__ and __str__ for
atomic_prop_set. Fix __repr__ for trival, acc_code, acc_cond,
mark_t. Remove __repr__ for twa_run and twa_word.
* tests/python/acc_cond.ipynb, tests/python/accparse.ipynb,
tests/python/atva16-fig2a.ipynb, tests/python/automata.ipynb,
tests/python/bdditer.py, tests/python/contains.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltlsimple.py, tests/python/ltsmin-dve.ipynb,
tests/python/product.ipynb, tests/python/relabel.py,
tests/python/satmin.ipynb tests/python/stutter-inv.ipynb,
tests/python/word.ipynb: Adjust test cases.
* tests/python/formulas.ipynb: Add test for atomic_prop_set.
* spot/twa/acc.hh: Hide default constructors, so that we can have
keyword arguments on the main constructor.
* python/spot/impl.i: Add __repr__.
* tests/python/setacc.py: Test it.
Fixes#366, reported by Simon Jantsch.
* spot/twaalgos/translate.cc: type_&Generic will also match if
type_==BA... use type_==Generic instead.
* tests/core/unambig.test: Add a test corresponding to Simon's report.
* NEWS: Describe the bug.
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.
Based on a report from Andreas Tollkötter.
* spot/twaalgos/dot.cc (highlight_states_show_num_): New option,
turned on implicitly when more than 8 colors are used.
* tests/core/highlightstate.test: Test it.
* NEWS: Mention it.
* THANKS: Add Andreas.
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.
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#357.
* spot/twaalgos/gfguarantee.cc: Decide that a moved init state is to
close from the terminal state *before* actually modifying the
automaton.
* tests/core/ltl2tgba2.test: Add a test.
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: Here.
* NEWS: Mention the change.
* tests/core/genltl.test: Add parity automata sizes for a set of
formulas.
* tests/core/parity2.test: Add another formula to the tests.
* 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/gfguarantee.cc: Rework the history computation to keep
an overapproximation of the history, and a longer one. Also replay
the history even if there is no initial trivial SCC. This helps with
translating FG(!a|XXXb) where we need to keep the history of a, but we
were previously unable to do so because some state had both "a" and
"ab" as input.
* spot/twaalgos/translate.cc: Optimize the product of suspendable
automata by removing useless trivial SCCs.
* tests/core/genltl.test, tests/core/satmin.test, NEWS: Adjust
expected results.
* spot/priv/allocator.hh, spot/priv/Makefile.am: add a STL-compliant
allocator based on spot::fixed_size_pool
* spot/misc/fixpool.hh, spot/misc/fixpool.cc, spot/misc/Makefile.am:
refactor the existing spot::fixed_size_pool
* spot/ltsmin/ltsmin.cc, spot/twa/twaproduct.cc: reflect changes in the
interface of spot::fixed_size_pool
* tests/core/mempool.cc: test the new allocator
Annotate pools with valgrind macros so that it detects errors in pool
usage. Typically, we wish valgrind to detect a leak when the user fails
to call proper deallocation function.
* spot/misc/fixpool.hh, spot/misc/mspool.hh: here
* configure.ac: ensure that valgrind header exists
* tests/Makefile.am, tests/core/mempool.cc, tests/core/mempool.test,
tests/core/.gitignore: add tests to ensure valgrind accurately detects
leaks
* 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.
This improves gf_guarantee_to_ba() on formulas GF(φ) where the
automaton for F(φ) as several leading transiant SCCs. E.g.,
GF(a <-> XXXa) where we know get results that are as good as
those of delag without loosing on the cases where delag's technique
would actually produce two big automata.
* spot/twaalgos/gfguarantee.cc: Implement this.
* spot/twaalgos/gfguarantee.hh, NEWS: Document it.
* tests/core/ltl2tgba2.test, tests/core/ltl3ba.test: Add test cases.
