Commit graph

6414 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
b6c076ce19 release Spot 2.11.5
* NEWS, configure.ac, doc/org/setup.org: Update version.
2023-04-20 09:45:41 +02:00
Alexandre Duret-Lutz
184aa9931e org: replace version references with org-babel blocks
This way we have fewer lines to edit multiple when making releases.

* doc/org/index.org, doc/org/init.el.in, doc/org/install.org,
doc/org/setup.org, doc/org/tools.org: Use org-babel instead of macros
for release version and links.
2023-04-19 09:07:02 +02:00
Alexandre Duret-Lutz
eb80f5d5af powerset: fix segfault when the initial state is a sink
Reported by Raven Beutner.

* spot/twaalgos/minimize.cc: Improve comment.
* spot/twaalgos/powerset.cc: Fix handling of an initial state that
is also a sink.
* tests/core/wdba2.test: Add test case.
* NEWS: Mention the bug.
2023-04-19 09:06:58 +02:00
Alexandre Duret-Lutz
eb0f40b9d6 twa_run: let as_twa work on the result of intersecting_run
Reported by Philipp Schlehuber-Caissier.

* spot/twaalgos/emptiness.cc (as_twa): Simplify considerably.  Don't
try to replay the run, and don't merge identical states.
* spot/twaalgos/word.hh, spot/twaalgos/emptiness.hh: Improve
documentation.
* tests/python/intrun.py: Add a test case.
* NEWS: Mention the bug.
2023-04-19 09:06:55 +02:00
Philipp Schlehuber-Caissier
993695a2c4 Fix parity solver if edgevector is not contiguous
Validity of strategies was tested relying on
num_edges() which might be smaller than the edge_number

* spot/twaalgos/game.cc: Fix here
* tests/python/game.py: Test here
2023-04-19 09:06:25 +02:00
Alexandre Duret-Lutz
0c8093eded correctly fails if emacs needed and missing
Fixes #528.

* configure.ac: Define EMACS using tools/missing.
* NEWS: Mention the bug.
2023-04-19 09:06:01 +02:00
Alexandre Duret-Lutz
646b6e546f fix spurious test-case failure when Python is not installed
Fixes #530.

* tests/core/ltlsynt2.test: Skip when PYTHON is empty.
* NEWS: Mention the fix.
2023-04-19 09:05:42 +02:00
Alexandre Duret-Lutz
1a0b1f235d * doc/tl/tl.tex: Typo in firstmatch semantics. 2023-04-19 09:04:16 +02:00
Philipp Schlehuber
5714ecce32 Ignore ltargz.m4
* .gitignore: Ignore it
* m4/ltargz.m4: Remove it
2023-04-19 09:04:11 +02:00
Alexandre Duret-Lutz
dcd4759896 org: fix rendering of R examples for recent ESS/Org
* doc/org/.dir-locals.el.in, doc/org/init.el.in: Newer ESS version
need to be taught to use default-directory instead of the project
directory.
* doc/org/ltlcross.org: Use "result file" to render the output.
2023-04-19 09:04:07 +02:00
Alexandre Duret-Lutz
a146457ea1 * doc/org/tut03.org: Typos. 2023-04-19 09:04:02 +02:00
Alexandre Duret-Lutz
d3013b072d org: do not require org-install
org-install has been obsolete for a long time, and has been removed
from Org 9.6.

* doc/org/init.el.in: Remove org-install.
2023-04-19 09:03:53 +02:00
Alexandre Duret-Lutz
e44cb5152a Bump version to 2.11.4.dev
* NEWS, configure.ac: Here.
2023-02-10 08:51:29 +01:00
Alexandre Duret-Lutz
50a58254a7 Release spot 2.11.4
* NEWS, configure.ac, doc/org/setup.org: Update version.
2023-02-10 08:49:26 +01:00
Alexandre Duret-Lutz
6fd0eebad4 to_finit: fix issue #526
* spot/twaalgos/remprop.cc: Use bdd_restrict instead of bdd_exists.
* tests/core/ltlf.test: Add test case.
* NEWS: Mention the bug.
2023-02-07 23:13:25 +01:00
Alexandre Duret-Lutz
058975c167 dbranch: fix handling of state-based acceptance
Fixes issue #525.

* spot/twaalgos/dbranch.hh, NEWS: Document.
* spot/twaalgos/dbranch.cc: Detect cases where the acceptance should
be changed from state-based to transition-based.
* tests/python/dbranch.py: Add a test case.
2023-02-05 14:59:50 +01:00
Alexandre Duret-Lutz
5969aa4925 work around gcc-snapshot warnings about dangling references
* spot/twaalgos/game.hh, spot/twaalgos/game.cc (get_state_players,
get_strategy, get_state_winners): Take argument by reference, not
copy.
* spot/twaalgos/synthesis.cc, spot/twaalgos/mealy_machine.cc: Replace
auto by actual type for readability.
2023-01-31 17:55:51 +01:00
Alexandre Duret-Lutz
2666072867 * .gitlab-ci.yml: Use pipeline id to name volumes. 2023-01-31 17:55:51 +01:00
Alexandre Duret-Lutz
126d9bc103 bin: fix number conversion routines on 32bit
On 32bit archetectures, long int = int the current check for detecting
values that overflow int will fail.  Conversion routings should check
errno.

* bin/common_conv.cc, bin/common_range.cc: Here.
2023-01-31 17:55:51 +01:00
Alexandre Duret-Lutz
a1c02856ac autfilt: allow --highlight-word to work on Fin acceptance
Fixes #523.

* bin/autfilt.cc: Remove the restriction.
* tests/core/acc_word.test: Add test case.
* NEWS: Mention the fix.
2023-01-31 17:55:51 +01:00
Florian Renkin
315872a54b ltlsynt: typo in doc
* bin/ltlsynt.cc: here
2023-01-31 17:55:51 +01:00
Alexandre Duret-Lutz
9ca2927291 bin: update copyright year and laboratory name
* bin/common_setup.cc: Here.
2023-01-31 17:55:51 +01:00
Alexandre Duret-Lutz
eae91e97cd robin_hood: update to version version 3.11.5
* spot/priv/robin_hood.hh: Update.
* spot/priv/Makefile.am: Patch ROBIN_HOOD_IS_TRIVIALLY_COPYABLE to
work around an issue with clang on Arch linux.
2023-01-31 17:55:51 +01:00
Alexandre Duret-Lutz
7e1d684797 dbranch: fix handling of states without successors
Fixes #524, reported by Rüdiger Ehlers.

* spot/twaalgos/dbranch.cc: When merging an edge going to state
without successors simply delete it.
* bin/spot-x.cc: Typo in documentation.
* tests/core/ltlcross.test: Add a test case.
* NEWS: Mention the bug.
2023-01-31 17:55:51 +01:00
Alexandre Duret-Lutz
39212bbcd2 more code smells
* bin/common_file.cc, bin/common_file.hh, bin/common_finput.cc,
bin/common_finput.hh, bin/common_output.cc, bin/common_setup.cc,
bin/common_setup.hh, bin/common_trans.cc, bin/common_trans.hh,
bin/dstar2tgba.cc, bin/genaut.cc, bin/genltl.cc, bin/ltl2tgba.cc,
bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc, bin/ltlfilt.cc,
bin/ltlsynt.cc, bin/randltl.cc: Fix minor code issues reported by
sonarcloud.
2023-01-31 17:51:18 +01:00
Alexandre Duret-Lutz
7b0507a950 bin: detect overflows in conversion functions
* bin/common_conv.cc (to_int, to_unsigned): Here.
* bin/common_range.cc (parse_range): And there.
* tests/core/ltlgrind.test, tests/core/genaut.test,
tests/core/randaut.test: Add test cases.
2023-01-31 17:51:18 +01:00
Alexandre Duret-Lutz
4a78d1bff4 fix some code smells reported by sonarcloud
* bench/dtgbasat/gen.py, bin/autcross.cc, bin/autfilt.cc,
bin/common_aoutput.cc, bin/common_aoutput.hh: Various cleanups.
2023-01-31 17:51:18 +01:00
Alexandre Duret-Lutz
36e79ecca6 * spot/twaalgos/game.cc: Fix incorrect std::forward. 2023-01-31 17:51:18 +01:00
Alexandre Duret-Lutz
344d82f2b4 simplify several comparison operators
* spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc,
spot/twaalgos/simulation.cc: Simplify, as reported by sonarcloud.
2023-01-31 17:51:18 +01:00
Alexandre Duret-Lutz
403e55d555 * doc/org/spot.css: Do not define background twice. 2023-01-31 17:51:18 +01:00
Alexandre Duret-Lutz
104e98aca6 fix merging of initial states in state-based automata
Fixes #522 reported by Raven Beutner.

* spot/parseaut/parseaut.yy: Make sure all edges leaving
the initial state have the same color.
* THANKS: Add Raven.
* NEWS: Mention the bug.
* tests/core/522.test: New file.
* tests/Makefile.am: Add it.
2023-01-31 17:51:18 +01:00
Alexandre Duret-Lutz
cab3ea7faf acd: rewrite Python wrapper without jQuery
* python/spot/__init__.py (acd): Rewrite javascript so that it does
not use jQuery, to make it easier to use in jupyterlab, or with
nbconvert.
* tests/python/zlktree.ipynb: Adjust.
* NEWS: Mention this.
2023-01-31 17:51:18 +01:00
Alexandre Duret-Lutz
09e147ee4b * NEWS, configure.ac: Bump version to 2.11.3.dev. 2022-12-09 09:43:18 +01:00
Alexandre Duret-Lutz
d7feeca13e Release Spot 2.11.3
* NEWS, configure.ac, doc/org/setup.org: Bump version to 2.11.3.
2022-12-09 09:40:27 +01:00
Alexandre Duret-Lutz
4629d074ab Fix semantics of [*i..j] and [:*i..j]
* doc/tl/tl.tex: After a discussion with Antoin, it appears that the
semantics previously given for f[*0..j] was not considering that f[*0]
should accept any sequence of one letter.
2022-12-07 11:26:51 +01:00
Alexandre Duret-Lutz
5dbf601afb * NEWS: Typos. 2022-12-06 16:07:21 +01:00
Philipp Schlehuber-Caissier
37d4e513d9 game: fix appending strategies bug
When calling solve_parity_game() multiple times on the same
automaton the strategies are appended one after the other.
Reported by Dávid Smolka.

* NEWS: Mention the bug.
* spot/twaalgos/game.cc: Fix it.
* tests/python/game.py: Test it.
* THANKS: Add Dávid.
2022-12-06 16:06:04 +01:00
Philipp Schlehuber-Caissier
86c433cf80 mealy: fix incorrect assertion
* spot/twaalgos/mealy_machine.cc (minimize_mealy): Do not compare
result to the original unsplit machine without splitting it first.
* tests/python/mealy.py: Add a test case.
2022-12-06 16:04:40 +01:00
Alexandre Duret-Lutz
6b70edabf0 getopt: do not include sys/cdefs.h to please Alpine Linux
* m4/getopt.m4: Pretend sys/cdefs.h is missing, so that Alpine linux
does not output a warning which we would turn into an error.
2022-12-02 17:30:29 +01:00
Alexandre Duret-Lutz
29037c1f55 autfilt: print match count even on parse errors
* bin/autfilt.cc: If -c is used, print the match_count even
in present of parse errors.
* tests/core/readsave.test: Adjust.
* NEWS: Mention the bug.
2022-12-02 15:24:31 +01:00
Alexandre Duret-Lutz
a032abf0c5 parseaut: diagnose states that are unused and undefined
Reported by Pierre Ganty.

* spot/parseaut/parseaut.yy: Add diagnostics.
* tests/core/parseaut.test: Adjust expected output, and add a test
case.
* NEWS: Mention the bug.
2022-12-02 15:24:25 +01:00
Alexandre Duret-Lutz
cfe1b0b70d configure: --with-pythondir should also override pyexecdir
Fixes #512.

* configure.ac: Here.
* NEWS: Mention the bug.
2022-11-17 11:14:32 +01:00
Alexandre Duret-Lutz
c2a3f2941d ltl_to_tgba_fm: fix a memory leak on abort
This issue surfaced in twacube.test after the previous patches.

* spot/twaalgos/ltl2tgba_fm.cc: Release the formula namer on abort.
* NEWS: Mention the bug.
2022-11-15 17:50:45 +01:00
Alexandre Duret-Lutz
843c4cdb91 translate, simplify: limit containment checks of n-ary operators
Fixes #521.

* spot/tl/simplify.cc, spot/tl/simplify.hh,
spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add an option
to limit automata-based implication checks of n-ary operators when too
many operands are used.  Defaults to 16.
* bin/spot-x.cc, NEWS, doc/tl/tl.tex: Document it.
* tests/core/bdd.test: Disable the limit for this test.
2022-11-15 17:49:21 +01:00
Alexandre Duret-Lutz
f2c65ea557 simplify: set exprop=false during containment checks
For issue #521, reported by Jacopo Binchi.

* spot/tl/simplify.cc: Here.
* tests/core/521.test: New test case.
* tests/Makefile.am: Add it.
* NEWS: Mention it.
* THANKS: Add Jacopo Binchi.
2022-11-15 17:22:13 +01:00
Alexandre Duret-Lutz
a6c65dff8d misc Doxygen fixes
* spot/misc/satsolver.hh, spot/tl/formula.hh, spot/twaalgos/hoa.hh,
spot/twaalgos/synthesis.hh, spot/twaalgos/zlktree.hh,
spot/twacube_algos/convert.hh: Typos in Doxygen comments.
2022-11-10 17:08:30 +01:00
Alexandre Duret-Lutz
0f4f7ec287 * debian/copyright: Fix download URL. 2022-11-10 17:08:30 +01:00
Alexandre Duret-Lutz
b36cee06a1 adjust to Swig 4.1.0
* python/spot/__init__.py: Add flatnested versions of some static
methods.
* spot/twa/acc.hh: Hide && version of & and |, causing trouble
to swig.
* tests/python/_synthesis.ipynb, tests/python/synthesis.ipynb:
Upgrade expected type names.
* tests/python/ipnbdoctest.py: Adjust for difference between 4.0 and
4.1.
2022-11-10 17:08:30 +01:00
Alexandre Duret-Lutz
6dc740184c * tests/sanity/style.test: Fix recent grep warnings. 2022-11-07 09:37:40 +01:00
Alexandre Duret-Lutz
5c5133348e mealy: improve error reporting
* spot/twaalgos/mealy_machine.cc: Add more exceptions.
* tests/python/except.py: Test them.
2022-11-07 09:07:31 +01:00