No point in having options such as --spin, --lbtt, --check, etc.
Also --dot was documented twice...
* bin/ltlsynt.cc (children): Remove aoutput_argp.
(options): Add explicit support for -d, -H, -q.
* bin/common_aoutput.cc, bin/common_aoutput.hh: Share the HOA help
text.
This is a patch that was sent by Simon Reinhardt to gnulib and has
never been applied. It fixes a several formatting issues in --help.
https://lists.gnu.org/archive/html/bug-gnulib/2016-02/msg00013.html
* lib/argp-fmtstream.c (__argp_fmtstream_update): Flush output as soon
as possible.
* lib/argp-fmtstream.h (struct argp_fmtstream): Member point_offs is
no longer needed.
* lib/argp-help.c (indent_to): Flush output to avoid a spurious
newline before an overlong word.
* spot/twaalgos/aiger.cc (mealy_machine_to_aig): Remove the code that
attempted to convert state names to integer, throwing exceptions on
failure. That code was not exercised anywhere, but it caused failure
in the implementation of an LTLf->AIG pipeline in which LTLf formulas
that label states are preserved.
The negation of global equivalences for outputs
contained a slight error when the output corresponded
to a negated gate.
* spot/twaalgos/aiger.cc: Fix
* tests/core/ltlsynt.test: Test
Some colleagues complained that the highlighting of edges and nodes
in the ACD display where not very readable, especially when sharing
screen during some video call. This should improve it.
* python/spot/__init__.py (acd): Fill the contents of the nodes when
they are highlighted. Add some glowing effect the the highlighted
edges.
* tests/python/zlktree.ipynb: Adjust.
* python/spot/__init__.py: Unindent the docstring for
formula.__format__. Because Python 3.13 strips the indentation but
previous version didn't, the following test case failed with Python
3.13.
* tests/python/formulas.ipynb: Adjust to unindented docstring.
Fix#597.
* spot/tl/print.cc: Fix rendering of X[!].
* doc/tl/spotltl.sty: Add a \StrongX definition.
* tests/core/latex.test: Add a test case.
* NEWS: Mention the issue.
This fixes issue #596.
* spot/twaalgos/remprop.cc: Rewrite main loop.
* tests/core/ltlf.test: Add test case.
* tests/python/game.py: Remove a test that appears
to make incorrect assumptions about to_finite.
* NEWS: Mention the bug.
The negation of global equivalences for outputs
contained a slight error when the output corresponded
to a negated gate.
* spot/twaalgos/aiger.cc: Fix
* tests/core/ltlsynt.test: Test
* python/spot/__init__.py: Unindent the docstring for
formula.__format__. Because Python 3.13 strips the indentation but
previous version didn't, the following test case failed with Python
3.13.
* tests/python/formulas.ipynb: Adjust to unindented docstring.
Fix#597.
* spot/tl/print.cc: Fix rendering of X[!].
* doc/tl/spotltl.sty: Add a \StrongX definition.
* tests/core/latex.test: Add a test case.
* NEWS: Mention the issue.
This fixes issue #596.
* spot/twaalgos/remprop.cc: Rewrite main loop.
* tests/core/ltlf.test: Add test case.
* tests/python/game.py: Remove a test that appears
to make incorrect assumptions about to_finite.
* NEWS: Mention the bug.
* spot/twaalgos/game.cc, spot/twaalgos/game.hh (get_state_winners):
Declare a non-const version as well to avoid a "possibly dangling
reference" error in code show by tut40.org.
I could not run "make check" in a copy of seminator 2.0 regenerated
with swig 4.0, because of changes in the way Swig imports its shared
libraries.
* python/spot/__init__.py: If sys.path contains "/spot-extra"
directory, add it to spot.__path__ as well. This helps situations
where a plugin use libtool and the development tree has the shared
libraries in .../spot-extra/.libs/
* spot/twaalgos/game.cc: If the original acceptance is "parity min",
use min_set(), not max_set(), to read edge priorities.
* tests/python/game.py: Add a test case.
* NEWS: Mention the bug.
* spot/tl/randomltl.hh (has_unary_ops): New method.
* spot/tl/randomltl.cc: Avoid creating subformulas of even size
when we do not have unary operators.
* tests/core/randpsl.test: Test it.
* NEWS: Mention it.
The error message, inherited from ltl2tgba, used to say "No formula to
translate", but "translate" isn't appropriate here.
* bin/common_finput.cc, bin/common_finput.hh (check_no_formula): Allow
"translate" to be changed.
* bin/ltlgrind.cc: Change it.
* tests/core/ltlgrind.test: Test it.
* spot/misc/permute.hh: New file.
* spot/misc/Makefile.am: Add it.
* spot/graph/graph.hh, spot/twa/twagraph.cc,
spot/twaalgos/randomize.cc: Use the new permute_vector() function.
* spot/twa/twagraph.hh: Update documentation.
* NEWS: Update.
* tests/core/syntimpl.cc: Rewrite to test multiple formulas at once,
and test them with three different implication checks.
* tests/core/syntimpl.test: Adjust the test to execute syntimpl only
once.
* spot/twaalgos/synthesis.cc: Remove a debuging print
from the semisym code, and add an additional case
in the fullysym code.
* tests/core/ltlsynt.test: Add a some test case,
and remove some bashism.
Previous output was not very usable in presence of decomposed
specifications. We now keep track of the number of parts, and also
prefix the columns names with "max_" or "sum_" to indicate how their
statistics are updated in presence of multiple part. Other missing
statistics, like the size of the translated automaton, or maximal
number of colors seen in a game, have been added.
* spot/twaalgos/synthesis.hh (bench_var): Rename, augment, and
document each statistsic.
* spot/twaalgos/mealy_machine.cc, spot/twaalgos/synthesis.cc,
bin/ltlsynt.cc: Adjust to the new naming scheme.
* doc/org/ltlsynt.org: Show a CSV file, and document its columns.
* tests/core/ltlsynt-pgame.test, tests/core/ltlsynt2.test,
tests/core/ltlsynt.test: Adjust test cases.
* NEWS: Mention the backward incompatible change.
Some columns were superfluous, other had inconsistent names, and some
times where not tracked.
* spot/twaalgos/synthesis.cc: Improve tracking of times and verbose
messages.
* bin/ltlsynt.cc (print_csv): Adjust CSV columns.
* tests/core/ltlsynt.test, tests/core/ltlsynt2.test,
tests/core/ltlsynt-pgame.test: Adjust expected CSV and verbose
messages.
* doc/org/ltlsynt.org: Give some example.
