GitLab

The goal is to improve coverage stats, but I discovered two issues
while doing so.

* tests/python/twagraph.py: New test case.
* tests/Makefile.am: Add it.
* spot/twa/twagraph.hh: Add fix typos in error messages.
* python/spot/impl.i: Fix broken wrappers for state_from_number and
state_acc_sets.

Fixes #235, reported by Henrich Lauko.

* python/spot/ltsmin.i: Catch CalledProcessError.
* NEWS: Mention the bug.
* THANKS: Add Henrich.

Related to #172, where we discussed that scc_info bindings were
missing.

* spot/twaalgos/sccinfo.hh (spot::scc_info::scc_node): Move...
(spot::scc_info_node): ... here to help Swig.
* python/spot/impl.i: Add bindings for scc_info.
* tests/python/sccinfo.py: New file.
* tests/Makefile.am: Add it.

* python/spot/__init__.py (show_mp_hierarchy, mp_hierarchy_svg): New
functions.
* tests/python/formulas.ipynb: Illustrate show_mp_hierarchy.
* python/ajax/spotcgi.in: Use mp_hierarchy_svg.
* python/ajax/css/trans.css: Adjust for possible overflows.
* NEWS: Mention this new feature.

* bin/common_output.cc: Move some of the printing code...
* spot/tl/hierarchy.cc, spot/tl/hierarchy.hh: ... here, as new
  variants of mp_class...
* python/spot/impl.i: ... that we can now call from Python.
* python/ajax/spotcgi.in: Use those to simplify and extend
the code printing class membership.

* spot/twaalgos/minimize.cc (minimize_wdba): Diminish the color of
terminal SCCs that are incomplete, as if they had a non-accepting
sink as successor.
* spot/twaalgos/strength.hh, spot/twaalgos/strength.cc
(is_terminal_automaton): Add an option to ignore trivial SCC as we did
before, since it matters for deciding membership to the guarantee
class.
(is_safety_mwdba): Rewrite as ...
(is_safety_automaton): ... generalizating to any acceptance, and
ignoring trivial SCCs.
* bin/ltlfilt.cc, python/ajax/spotcgi.in, spot/tl/hierarchy.cc,
tests/core/ikwiad.cc: Adjust usage of is_terminal_automaton and
is_safety_automaton().
* tests/core/hierarchy.test: Add a problematic formula as test-case.
* NEWS: Mention the bug.

* python/spot/__init__.py: Handle options.
* spot/twaalgos/dtwasat.cc: Handle options.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Handle options.
* tests/core/satmin.test: Update tests.
Now use 'sat-minimize=4' to use the naive algo.
* tests/core/satmin2.test: Update tests.
Now use --sat-minimize='naive' to use the naive algo.
* tests/python/satmin.py: Update tests.
Now use 'naive=True' to use the naive algo.

* python/spot/__init__.py: Handle 'dicho' option in 'sat_minimize'.
* spot/priv/satcommon.cc: Implement get_number_of_distinct_vals.
* spot/priv/satcommon.hh: Declare get_number_of_distinct_vals.
* spot/twaalgos/dtbasat.cc: Use get_number_of_distinct_vals.
* spot/twaalgos/dtbasat.hh: Change dichotomy function's prototype.
* spot/twaalgos/dtwasat.cc: Use get_number_of_distinct_vals.
* spot/twaalgos/dtwasat.hh: Change dichotomy function's prototype.
Handle options.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Add dicho_langmap_ var for options.
* tests/core/satmin2.test: Add tests for dichotomy.
* tests/core/satmin.test: Add tests for dichotomy.
* tests/python/satmin.py: Replace 'dichotomy' with 'dicho' option.

* python/spot/impl.i: Add python bindings.
* spot/twaalgos/langmap.cc: Implement algo.
* spot/twaalgos/langmap.hh: Declare algo.
* spot/twaalgos/Makefile.am: Add new files.
* tests/python/langmap.py: Add tests.
* NEWS: Update.

* python/spot/__init__.py: Add 'assume' option.
* spot/misc/satsolver.cc: Add function to handle assumptions.
* spot/misc/satsolver.hh: Declare assumption function.
* spot/twaalgos/dtbasat.cc: Implement dtba_sat_minimize_assume.
* spot/twaalgos/dtbasat.hh: Declare it.
* spot/twaalgos/dtwasat.cc: Implement dtwa_sat_minimize_assume and
handle options.
* spot/twaalgos/dtwasat.hh: Declare it.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Use param_ var for incr and assume.
* tests/core/satmin.test: Add tests for the new function.
* tests/core/satmin2.test: Add tests for the new function.
* tests/python/satmin.py: Add tests for the new function.

* python/spot/__init__.py: Add 'incr' boolean argument.
* spot/twaalgos/dtbasat.cc: Implement dtba_sat_minimize_incr(...).
* spot/twaalgos/dtbasat.hh: Declare it.
* spot/twaalgos/dtwasat.cc: Implement dtwa_sat_minimize_incr(...) and
deal with options.
* spot/twaalgos/dtwasat.hh: Declare it.
* spot/twaalgos/postproc.cc: Add option --sat-minimize=incr.
* spot/twaalgos/postproc.hh: Add incr parameter.
* tests/core/satmin.test: Add tests for incremental version.
Update expected result.
* tests/core/satmin2.test: Add tests for incremental version.
* tests/python/satmin.py: Add tests for incremental version.

This should will come handy to implement the convertion from LTL to
alternating automata, and to handle automata with multiple initial
states.

* spot/twaalgos/alternation.hh, spot/twaalgos/alternation.cc: New files.
* spot/twaalgos/Makefile.am: Add them.
* python/spot/impl.i: Add bindings.
* tests/python/alternating.py: Test states_and.

The only missing point is that the HOA parser cannot deal with multiple
universal initial states, as seen in parseaut.test.

* spot/graph/graph.hh (new_univ_dests): New function, extracted from...
(new_univ_edge): ... this one.
* spot/twa/twagraph.hh (set_univ_init_state): Implement using
new_univ_dests.
* spot/twaalgos/dot.cc, spot/twaalgos/hoa.cc, python/spot/impl.i:
Add support for universal initial states.
* spot/parseaut/parseaut.yy: Add preliminary support for
universal initial states.  Multiple universal initial states
are still not supported.
* tests/core/alternating.test, tests/core/parseaut.test,
tests/python/alternating.py: Adjust tests and exercise this new feature.

This only allows creating universal edges, and reading the associated
destinations.

* spot/twa/twagraph.hh (new_univ_edges, univ_dests, is_alternating): New
function.
* python/spot/impl.i: Add Python bindings.
* tests/python/alternating.py: New file.
* tests/Makefile.am: Add it.

* python/spot/__init__.py (automata): Do not create a session for
every command, this is only needed if automata() is run with a timeout
parameter.
* python/ajax/spotcgi.in: Adjust exclude the main process from
the process group, so that only children are killed on SIGALRM.
* NEWS: Mention the bug.

* python/spot/__init__.py (automata): Do not create a session for
every command, this is only needed if automata() is run with a timeout
parameter.
* python/ajax/spotcgi.in: Adjust exclude the main process from
the process group, so that only children are killed on SIGALRM.
* NEWS: Mention the bug.

Fixes #187.

* spot/tl/ltlf.cc, spot/tl/ltlf.hh: New files.
* spot/tl/Makefile.am: Add them.
* bin/ltlfilt.cc: Add a new option.
* bin/man/ltlfilt.x: Add bibliographic reference.
* tests/core/ltlfilt.test: Add more tests.
* tests/python/ltlf.py: New file.
* tests/Makefile.am: Add it.
* python/spot/impl.i: Python bindings.
* NEWS: Mention it.

* NEWS, python/spot/ltsmin.i: here.

Reported by Laurent Xu.

* python/spot/impl.i: Fix the iterator to return pointers instead of
references.  Because references are ultimately copied.
* tests/python/automata.ipynb: Add test cases.
* NEWS: Mention it.

* python/spot/aux.py (tmpdir): New context manager.
* python/spot/ltsmin.i: Use it for the two magics.
* NEWS: Mention this.

* python/spot/impl.i: Here.
* NEWS: Mention it.
* tests/python/highlighting.ipynb: Add test case.

* python/ajax/spotcgi.in: Here.
* NEWS: Mention it.

* python/ajax/spotcgi.in: Here.
* NEWS: Mention it.

* python/ajax/logos/lip6sys64.png, python/ajax/logos/lrde64.png: Delete.
* python/ajax/css/trans.css, python/ajax/trans.html,
python/ajax/Makefile.am: Adjust.

Fixes #162.

* python/spot/ltsmin.i: Implement the magic.
* NEWS: Mention it.
* tests/python/ltsmin-pml.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* tests/python/ipnbdoctest.py: Adjust.

* spot/tl/contain.cc, spot/tl/contain.hh: Simplify the
use of language_containment_checker by adding default argument.
* python/spot/__init__.py, python/spot/impl.i: Bind it in Python.
* doc/org/tut04.org: New file to illustrate it.
* doc/org/tut.org, doc/Makefile.am: Add it.
* NEWS: Mention those changes.

Final part of #176.

* python/ajax/trans.html: Here.

Final part of #176.

* python/ajax/trans.html: Here.

Fixes #168.

* python/spot/__init__.py: Implement it.
* tests/python/formulas.ipynb: Test it.
* NEWS: Mention it.

* python/spot/impl.i: Here.
* tests/python/automata.ipynb: Use it.
* NEWS: Mention it.

* python/spot/impl.i: Here.
* tests/python/automata.ipynb: Use it.
* NEWS: Mention it.

* doc/org/concepts.org, doc/org/ltlcross.org, doc/org/ltldo.org,
python/ajax/trans.html, tools/man2html.pl: Update URLs.

Fixes #159.

* python/spot/ltsmin.i: Here.
* python/spot/impl.i: Disable duplicate instantiation.
* tests/python/ltsmin.ipynb: Test it.

* spot/twa/twagraph.hh (edges): Do not hide from SWIG.
* spot/graph/graph.hh: Hide stuff that SWIG do not understand.
* python/spot/impl.i: Add some typemaps and fragment to
iterate over the result of twa_graph::edges().

* spot/twaalgos/word.hh: add parse_word method and a new constructor
* spot/twaalgos/word.cc: implement word parsing
* python/spot/__init__.py: add parse_word method binding
* tests/python/word.ipynb: add word parsing tests

* spot/twaalgos/emptiness.hh (emptiness_check_instantiator): rename
min_acceptance_conditions and max_acceptance_conditions to
min_sets and max_sets.
* spot/twaalgos/emptiness.cc, python/ajax/spotcgi.in,
tests/core/ikwiad.cc, tests/core/emptchk.cc, tests/core/randtgba.cc:
Adjust.
* doc/org/upgrade2.org, NEWS: Mention the change.