* python/spot/impl.i: Process game.hh.
* spot/misc/game.cc, spot/misc/game.hh: Make the output of
parity_game_solve() a solved_game object for easier manipulation in
Python.
* bin/ltlsynt.cc: Adjust usage.
* tests/python/paritygame.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* NEWS: Mention these bindings.
* spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll,
spot/twaalgos/hoa.cc: Add input and output support.
* doc/org/hoa.org: Document the HOA extension.
* bin/ltlsynt.cc: Add a --print-game-hoa option to
produce such format.
* tests/core/gamehoa.test: New file to test this.
* tests/Makefile.am: Add it.
* NEWS: Mention this new feature.
Fixes#411 reported by Frantiček Blahoudek.
* bin/ltlcross.cc: Catch the issue.
* tests/core/ltlcross6.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention it.
Reported by Florian Renkin.
* spot/twaalgos/emptiness.cc (reduce): If the automaton uses Fin
acceptance, check the reduced cycle and revert to the original cycle
if necessary.
* tests/python/intrun.py: New file.
* tests/Makefile.am: Add it.
* spot/twaalgos/emptiness.hh: Improve documentation.
Reported by Florian Renkin.
* spot/twaalgos/emptiness.cc (reduce): If the automaton uses Fin
acceptance, check the reduced cycle and revert to the original cycle
if necessary.
* tests/python/intrun.py: New file.
* tests/Makefile.am: Add it.
* spot/twaalgos/emptiness.hh: Improve documentation.
* python/spot/__init__.py: Use keyword arguments in to_parity()
* python/spot/impl.i: remove useless includes.
* spot/twaalgos/car.cc, spot/twaalgos/car.hh,
spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh,
tests/Makefile.am, spot/twaalgos/Makefile.am:
content moved to toparity.
* spot/twaalgos/postproc.cc: Use the new version of to_parity in
postprocessor::run.
* spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: Add the
content of rabin2parity and car.
* tests/python/car.py, tests/python/toparity.py: Moved all tests
from car.py to toparity.py.
* tests/python/except.py: Change iar() to iar_old().
Reported by Juraj Major.
* spot/twaalgos/sccinfo.cc (scc_info::get_accepting_run): Do not
assume TRACK_STATES is enabled.
* tests/core/autcross5.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
* bin/autfilt.cc: Add a --partial-degeneralize option.
* NEWS: Mention it.
* spot/twaalgos/degen.cc: Do not restrict partial_degeneralize() to
deterministic automata.
* spot/twaalgos/degen.hh: Adjust documentation.
* tests/core/pdegen.test: New test case.
* tests/Makefile.am: Add it.
* tests/python/pdegen.py: Adjust.
* spot/misc/tmpfile.cc: Display strerror(errno) plus some suggestions
that depend on the error. Based on a report from Shengping Shaw.
* THANKS: Add reporter.
* tests/core/ltlcross5.test: New file.
* tests/Makefile.am: Add it.
* spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Implement it.
* tests/python/pdegen.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the new function.
* tests/Makefile.am (ltsmin_modelcheck_LDADD): Add -lpthread as it
seems Debian's libtool does not carries this dependency over from
libspotltsmin.la. Also using $(LTLIBMULTITHREAD) does not work,
because that would add -pthread which is currently ignored when
linking shared libraries (because libtool adds -nostdlib for some
reason).
These rules come from Delag's paper, and help some cases
in issue #385.
* spot/tl/simplify.cc: Implement the simplification.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/385.test: New file.
* tests/Makefile.am: Add it.
* tests/core/reduccmp.test: More tests.
* tests/core/ltl2tgba2.test: Adjust one improved case.
* tests/python/automata.ipynb, tests/python/twagraph-internals.ipynb:
Adjust expected output, as the cnf/dnf reorder some subformulas.
This allows fixing issue #388 reported by Victor Khomenko.
* spot/twaalgos/word.cc, spot/twaalgos/word.hh (use_all_aps): New
method.
* tests/python/stutter-inv.ipynb: Use it.
* tests/python/stutter.py: New file, with Victor's test case.
* tests/Makefile.am: Add python/stutter.py.
Related to issue #376.
* spot/kripke/kripkegraph.hh: Avoid indirect type definitions for the
benefit of Swig.
* python/spot/impl.i: Add bindings for iterators over kripke_graph
states and edges.
* tests/python/kripke.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Update.
Reported by Simon Jantsch.
* spot/twaalgos/product.cc: Here.
* tests/core/unambig2.test: New file, testing this plus
the previous patch.
* tests/Makefile.am: Add unambig2.test.
* NEWS: Mention the bug.
Fixes#372.
* python/spot/impl.i: Refactor the handling of exceptions using a
Lippincott function. Map out_of_range to IndexError. Add
PyObject* version for bdd_dict's register and unregister functions
so we can use Python objects as well.
* tests/python/bdddict.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the changes.
* 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.
* 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.
* 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
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/product.cc, spot/twaalgos/product.hh: Implement it.
* tests/python/_product_susp.ipynb: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention it.
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.
* 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.
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#341.
* python/spot/__init__.py (automata): Rewrite and simplify using
the subprocess context manager.
* tests/python/341.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the issue.
* spot/priv/satcommon.cc, spot/priv/satcommon.hh: Make it possible to
set the log file without setting the environment variable. Adjust
print_log to take the input state and print it as a new column.
* spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc: Adjust all
calls to print_log. Fix log output for incremental approaches.
Prefer purge_unreachable_states() over stats_reachable(). Do
not call scc_filter() on colored automata.
* spot/twaalgos/dtwasat.hh: Document the new "log" option.
* NEWS: Mention the changes.
* tests/python/satmin.ipynb: New file.
* tests/Makefile.am: Add it.
* doc/org/satmin.org, doc/org/tut.org: Link to it.
* doc/org/satmin.org, bin/man/spot-x.x: Adjust description
of CSV files.
* bench/dtgbasat/gen.py, bench/dtgbasat/tabl.pl,
bench/dtgbasat/tabl1.pl, bench/dtgbasat/tabl2.pl,
bench/dtgbasat/tabl3.pl, bench/dtgbasat/tabl4.pl: Adjust for
the new column.
* spot/misc/satsolver.cc, spot/misc/satsolver.hh (stats): Make it
const.
* python/spot/__init__.py (sat_minimize): Add display_log and
return_log options.
* tests/python/ipnbdoctest.py: Adjust to not compare SAT-minimization
logs as they contain timings.
* python/spot/impl.i: Add missing bindings from remprop.hh
* tests/python/except.py: New file to test several error cases.
* tests/Makefile.am: Add it.
* spot/twaalgos/rabin2parity.cc (iar): Fix error message.
