Commit graph

6434 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
bb95705d52 mention the bug fixed in BuDDy
* NEWS: Explain the bug fixed in previous patch and reported in
issue #535.
* THANKS: Add Guillermo.
2023-08-01 11:12:49 +02:00
Alexandre Duret-Lutz
e37bc9e1ae [buddy] fix cache index of bdd_forall
Fix a 20 year old typo that caused a bug reported by Guillermo Perez.

* src/bddop.c (bdd_forall, bdd_forallcomp): Fix the cache index.
2023-08-01 11:12:49 +02:00
Alexandre Duret-Lutz
de7d5a956f * .gitlab-ci.yml: temporary disable raspbian. 2023-08-01 11:12:49 +02:00
Alexandre Duret-Lutz
44d9e34e32 improve coverage of LaTeX/utf8 printers for SERE
* bin/common_output.cc, bin/common_output.hh,
bin/randltl.cc: Adjust so that running "randltl -S" use
the SERE flavor of the spot/latex/utf8 formula printers.
* tests/core/latex.test, tests/core/utf8.test,
tests/python/ltlparse.py: Add more test cases.
2023-08-01 11:12:49 +02:00
Alexandre Duret-Lutz
15857385a5 bin: cover more tmpfile failure when running as root
* tests/core/ltlcross5.test: reorganize to test missing directory
before permission issues, as the latter cannot be run as root.
2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
3d412fbb78 tests: add some test to cover autcross' univ-edges removal
* tests/core/ltl3ba.test: Here.
2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
531252119c aiger: order the inputs of binary AND gates
* spot/twaalgos/aiger.cc: Here.
* tests/core/ltlsynt.test: Adjust, and add test case for aiger=optim.
2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
e548bf0a8e acc: remove some dead functions
* spot/twa/acc.hh, spot/twa/acc.cc (has_parity_prefix,
is_parity_max_equiv): Remove.
* spot/twa/acc.hh, spot/twa/twagraph.cc,
spot/twa/twagraph.hh (apply_permutation): Remove.
2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
69b9ffef9a bin: fix handling for --output & --format with LTL outputs
* bin/common_output.cc: Set the output stream for LTL formats.
2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
8065759fbd * HACKING: Mention the svgo version we use. 2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
090dcf17eb work around spurious GCC 13 warnings
* spot/graph/graph.hh (new_univ_dests): Add an overload taking
a temporary vector.
* spot/twa/twagraph.cc (defrag_states): Use it.
* tests/core/parity.cc: Remove some temporary variables.
2023-08-01 10:51:33 +02:00
Alexandre Duret-Lutz
bd1809f758 bin: handle thousands of output files
Fixes #534.  Test case is only on next branch.

* bin/common_file.hh, bin/common_file.cc: Make it possible
to reopen a closed file.
* bin/common_output.cc, bin/common_aoutput.cc: Add a heuristic
to decide when to close files.
* NEWS: Mention the issue.
2023-08-01 10:51:33 +02:00
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