* spot/twaalgos/dot.cc (print_dot): Add some detection of Mealy
machines, and some code to render its I/O in a <table>.
* tests/python/synthesis.ipynb: Adjust expected output.
* tests/python/_mealy.ipynb: New file.
* tests/Makefile.am: Add python/_mealy.ipynb.
* NEWS: Mention the new feature.
Aiger circuits noew have their own class.
Monitors can be translated to and obtained
from aiger circuits.
Moreover a step by step evaluation method
is provided.
* spot/twaalgos/aiger.hh,
spot/twaalgos/aiger.cc: Here
* bin/ltlsynt.cc: Adopt new modes
* tests/core/ltlsynt.test: Adapt tests
* python/spot/impl.i: Add python support
* tests/Makefile.am,
tests/python/aiger.py: New test cases
Reported by Florian.
* spot/twaalgos/zlktree.cc: Handle the case where the condition does
not cover all colors.
* tests/python/zlktree.py: New file.
* tests/Makefile.am: Add it.
Fixes#471, reported by Cambridge Yang.
* spot/twa/twa.cc (intersecting_run): Disable the product
optimization for weak automata.
* tests/python/471.py: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
We have enough outputs checked verbatim everywhere so that testing
that three execution of a single command return the same output is now
a waste of time.
* tests/core/simdet.test: Remove.
* tests/Makefile.am: Adjust.
Related to issue #298.
* spot/twaalgos/determinize.cc: Recognize braces that are temporary
to avoid emitting colors when they become empty.
* tests/python/298.py: New file, showing a reduction of colors.
* tests/Makefile.am: Add it.
* tests/core/ltlsynt.test: Adjust expected output (now smaller).
* tests/core/genltl.test: Adjust one expected output (now larger).
* NEWS: Mention the issue.
* spot/twaalgos/game.hh, spot/twaalgos/game.cc: Rename
solve_reachability_game() as solve_safety_game(), rewrite it (the old
implementation incorrectly marked dead states as winning for their
owner).
* tests/python/paritygame.ipynb: Rename as...
* tests/python/games.ipynb: ... this, and illustrate
solve_safety_game().
* tests/Makefile.am, NEWS, doc/org/tut.org: Adjust.
* tests/python/except.py: Add more tests.
This fixes#441, reported by Jérôme Dubois.
* tests/python/mergedge.py: New file.
* tests/Makefile.am: Add it.
* spot/twa/twagraph.cc (merge_edges): Fix initialization of second
loop.
* NEWS: Mention the bug.
spot/twaalgos/postproc.hh: Introduce options Buchi and
GeneralizedBuchi. The latter is similar to TGBA but the former differs
from BA in that it does not imply state-based acceptance, since that
can be specified separately. Also all other acceptance types are not
abbreviated, so those new names make more sense.
* NEWS: Mention that.
* spot/twaalgos/postproc.cc, spot/twaalgos/translate.cc: Adjust
to support Buchi and GeneralizedBuchi without breaking BA and TGBA.
* bin/autfilt.cc, bin/common_aoutput.cc, bin/common_post.cc,
bin/ltl2tgta.cc, doc/org/tut10.org, doc/org/tut12.org,
doc/org/tut30.org, python/spot/__init__.py,
tests/python/automata.ipynb, tests/python/langmap.py,
tests/python/misc-ec.py, tests/python/satmin.ipynb,
tests/python/satmin.py, tests/python/toweak.py: Use the new names.
* tests/Makefile.am: Add missing langmap.py.
This is a bug I introduced while merging Philipp's patch.
* spot/misc/game.cc (parity_game::solve): Set the strategy for player
0 in useless SCCs.
(parity_game::fix_scc): Do not use sub_game_ to detect edges exiting
the SCC.
* tests/python/game.py: New file.
* tests/Makefile.am: Add it.
* 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.
