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.
GCC 12/13/14 can emit spurious warnings for something
as innocent as vec.insert(vec.begin(), 12)...
Reported by Antoine Martin and Quentin Rataud.
* m4/gccwarn.m4: Test the above code and disable GCC's
-Wnull-dereference warning if necessary.
* debian/control: Remove the ipython3-notebook alternate
build-depends, as this package was removed from Debian in 2016. Add
gdb ad build-depends, in attempt to fix some OSB builds.
* spot/twaalgos/degen.hh (is_partially_degeneralizable): Pass the
forbid vector by reference, and document it. I hope that not passing
forbid by copy will get rid of a spurious "potential nullptr" warning
by gcc on Arch Linux.
* spot/twaalgos/degen.cc: Adjust, and refactor the code a bit.
* spot/twaalgos/toparity.cc: Likewise.
Python 3.12 introduced some subtle changes in the way doc strings are
displayed by help(). This was causing spurious errors in the
following test.
* tests/python/formulas.ipynb: Use print(x.__doc__) instead of
help(x).
We had some incorrectly escaped strings that are now causing
SyntaxWarnings with Python 3.12
* bin/options.py, python/spot/aux_.py, python/spot/ltsmin.i,
python/spot/__init__.py: Here.
* NEWS: Mention the fix.
For issue #570.
* spot/twaalgos/cleanacc.hh,
spot/twaalgos/cleanacc.cc (reduce_buchi_acceptance_set_here,
enlarge_buchi_acceptance_set_here): New functions.
* bin/autfilt.cc: Add options --reduce-acceptance-set and
--enlarge-acceptance-set.
* tests/core/basetred.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention it.
Commit bda40a5f introduced a subtle bug where nm_minato was being
increased in more cases causing some non-deterministic automata to be
incorrectly tagged as deterministic automata.
Fixes issue #575, reported by Dávid Smolka.
* spot/twaalgos/simulation.cc (create_edges): Do not increment
nm_minato when dest is bddfalse.
* tests/core/568.test: Add Dávid's first test-case.
* tests/python/forq_contains.py: Add Dávid's second test-case.
* bin/ltlsynt.cc: Also simplify subformulas using polarity and global
equivalence. Add support for --polarity=before-decompose and
--global-equiv=before-decompose to restablish the previous behavior.
* spot/tl/apcollect.hh,
spot/tl/apcollect.cc (realizability_simplifier::merge_mapping): New
method.
* tests/core/ltlsynt.test: Add new test cases.
The \f(CW macro to switch to "constant-width" does not seem to
honored when converting to html, and I've found some patch to
groff removing its use from their own man page.
https://lists.gnu.org/archive/html/groff-commit/2020-07/msg00015.html
Lets use \fC instead, as it seems to produce some <tt> in HTML.
Two manpages had URLs pointing to spot.lrde.epita.fr instead of
spot.lre.epita.fr.
Finally, spot-x.x had an incorrectly closed .EX block, that completly
broke the HTML conversion.
* bin/man/autcross.x, bin/man/ltl2tgba.x, bin/man/ltlcross.x,
bin/man/spot-x.x, bin/man/spot.x: Fix the aforementioned issues.
help2man used characters in the range 0x80,...,0x84 to mark special
sections/characters during its processing, but those bytes where also
occurring in other utf-8 characters breaking the output. For instance
the character '₁' ( a subscript 1), is encoded as "0xE2 0x82 0x81" in
utf-8.
* tools/help2man: Tell perl that input and output should be assumed to
be utf-8. Also use "private-use codepoints" for those special
characters to avoid any future conflict.
Since we now require Python 3.6, we can use f-strings instead of
format() to make the code more readable.
* doc/org/tut01.org, doc/org/tut02.org, doc/org/tut03.org,
doc/org/tut21.org, doc/org/tut24.org, doc/org/tut90.org,
python/spot/__init__.py, python/spot/jupyter.py, tests/python/acc.py,
tests/python/acc_cond.ipynb, tests/python/complement_semidet.py,
tests/python/decompose.ipynb, tests/python/formulas.ipynb,
tests/python/highlighting.ipynb, tests/python/ipnbdoctest.py,
tests/python/ltlf.py, tests/python/parity.ipynb,
tests/python/product.ipynb, tests/python/relabel.py,
tests/python/satmin.ipynb, tests/python/stutter-inv.ipynb,
tests/python/twagraph-internals.ipynb, tests/python/zlktree.ipynb: Use
f-strings.
This uses the same trick as discussed in issue #566 and issue #568.
* spot/twaalgos/determinize.cc (safra_support): Use a basis
if it is smaller than 2^|support| for the current Safra state.
* tests/core/568.test: Add some tests.
* NEWS: Mention the optimization.
Closes issue #568.
* spot/twaalgos/simulation.cc (direct_simulation::build_result):
Implement an alternate loop based on edge_separator::basis to iterate
over a signature to build results.
* tests/core/568.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the optimization.
These are meant to test the optimization implemented in issue #568.
* spot/gen/automata.hh, spot/gen/automata.cc, bin/genaut.cc: Add
support for --cycle-log-nba and --cycle-onehot-nba.
* tests/core/genaut.test: Add some tests.
* tests/python/gen.ipynb: Illustrate them.
* NEWS: Mention them.
Related to issue #563.
* spot/twaalgos/hoa.hh (create_alias_basis): New function.
* spot/twaalgos/hoa.cc (create_alias_basis): New function.
(print_hoa): Add support for option 'b' and create_alias_basis
in this case.
* bin/common_aoutput.cc, NEWS: Document -Hb.
* tests/core/readsave.test, tests/python/aliases.py: Add test cases.
Pierre Ganty wrote that he could not compile Spot with Swig 4.2.1
anymore, and when I upgraded from 4.2.0 to 4.2.1 I could not either.
It seems that declaring operator<< as friends in subclasses is
confusing Swig 4.2.1. See https://github.com/swig/swig/issues/2845
* spot/twa/acc.cc, spot/twa/acc.hh: Declare operator<< for
acc_cond::mark_t and acc_cond::acc_code outside the class, so that we
do not need friend declarations.
This script was first posted on https://github.com/adl/hoaf/issues/73
* doc/org/tut25.org: New file.
* doc/Makefile.am: Add it.
* doc/org/tut.org, doc/org/tut21.org, NEWS: Link to it.
* doc/org/init.el.in: Install *.py files.
* doc/org/.gitignore: Add toba.py.
For issue #566.
* spot/twaalgos/powerset.cc: Use the edge_separator on automata
with |AP|>5 that have few distinct labels.
* tests/core/566.test: Augment test-case.
* NEWS: Update.
* spot/twaalgos/split.cc,
spot/twaalgos/split.hh (edge_separator::add_to_basis): Add a variant
that is limited in the number of labels it adds.
* spot/twaalgos/alternation.cc: Use it. Also add
a cache of separated edges, as in the split.
This generalizes (and replaces) the two-argument split that was
introduced in c2832cabfc.
* spot/twaalgos/split.cc, spot/twaalgos/split.hh (edge_separator): New
class.
(separate_edges): New function.
(split_edges): Remove the two argument version.
* spot/twaalgos/forq_contains.cc: Adjust to use the edge_separator
class.
* tests/python/splitedge.py: Adjust test case.
* tests/python/split.ipynb: New file.
* tests/Makefile.am, doc/org/tut.org: Add it.
* NEWS: Mention it.
* spot/twaalgos/split.cc: The two split_edges() versions only differ
by the way they split a label. Let's define all the rest of the
algorithm in split_edges_aux().
Related to issue #566.
* spot/twaalgos/alternation.cc (alternation_remover::run): Here.
* tests/core/566.test: Augment test case.
* NEWS: Mention the change.
For issue #566.
* spot/twaalgos/dualize.cc (dualizer::copy_edges): Implement another
loop to be used when the number of outgoing edges of a state is
smaller than the number of AP.
* tests/core/566.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the improvement.
minterms_of was introduced in BuDDy with Spot 2.10, but
wasn't properly binded in Python.
* python/buddy.i: Add bindings.
* tests/python/bdditer.py: Test them.
