Commit graph

6422 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
adca03a30a * tests/core/ltlcross4.test: Work around recent Pandas change. 2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
47674c0d2f fix spurious failure of ltlcross4.test
Reported by Yuri Victorovich.

* tests/core/ltlcross4.test: Drop the 'formula' column before
computing aggregates.  It causes warnings in some Pandas versions, and
errors in others.
2023-08-01 10:51:33 +02:00
Florian Renkin
330b34e84d parity_type_to_parity: Add missing cases
* spot/twaalgos/toparity.cc: Correct some cases where the solution was
not detected.
* tests/python/toparity.py: Update tests.
2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
75bd595d28 bitvect: work around incorrect warning from gcc
* spot/misc/bitvect.hh: Don't free the old ptr if realloc() returns
NULL, as this confuse GCC who warns that we are freeing something that
has already been freed.   Instead, let the ~bitvect() destructor
handle this.
2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
9c6fa4921b debian: add missing build dependencies
* debian/control: Add Build-Depends on graphviz, jupyter-nbconvert,
doxygen.
2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
2495004afd avoid a g++-12 warning about potential null pointer dereference
* spot/twaalgos/determinize.cc (sorted_nodes): Rewrite to
avoid reallocation of temporary vector.
2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
16373cfb10 Work around spurious g++-12 warnings
* spot/twaalgos/ltl2tgba_fm.cc, spot/tl/formula.hh,
spot/twaalgos/translate.cc: Add SPOT_ASSUME in various places to help
g++.
2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
d0ae0dfc38 * NEWS, configure.ac: Bump version to 2.11.5.dev. 2023-04-20 09:48:22 +02:00
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