Commit graph

5939 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
e5b90a8e00 * NEWS, configure.ac: Bump version to 2.9.6.dev. 2021-01-18 11:09:49 +01:00
Alexandre Duret-Lutz
93ea0e34b0 Release Spot 2.9.6
* NEWS, configure.ac, doc/org/setup.org: Bump version to 2.9.6.
2021-01-18 11:07:12 +01:00
Alexandre Duret-Lutz
507c4a509c * NEWS: Update for recent changes. 2021-01-18 09:30:33 +01:00
Alexandre Duret-Lutz
f0e1ea1931 * .gitlab-ci.yml (alpine-gcc): Do not run both check and distcheck. 2021-01-18 09:23:52 +01:00
Alexandre Duret-Lutz
171c67c091 gfguarantee: fix automaton modification during iteration
Fixes #449.

* spot/twaalgos/gfguarantee.cc (do_g_f_terminal_inplace): Save
edge additions to perform them after the loop.  Otherwise,
reallocating the edge buffer might break the iteration.
2021-01-18 09:23:50 +01:00
Alexandre Duret-Lutz
91fc622d00 python: fix incorrect assertions on temporary objects
* tests/python/stutter.py: Do not call acc() on a temporary
object, and fix the last two asserts.
2021-01-18 09:23:47 +01:00
Alexandre Duret-Lutz
b7accdcf0d * tests/python/ipnbdoctest.py: Work around failures on Fedora. 2021-01-18 09:23:42 +01:00
Alexandre Duret-Lutz
a820c58e74 patch gnulib to accomodate autoconf 2.70
Upgrading gnulib turned to be too difficult, so this only includes
updates to m4 files necessary to please Autoconf 2.70.

For issue #447.

* m4/extensions.m4, m4/malloc.m4, m4/std-gnu11.m4: Cherry-pick
from today's gnulib version.
2021-01-18 09:23:25 +01:00
Alexandre Duret-Lutz
d779395db6 update obsolete autoconf constructs
Part of #447.

* configure.ac, m4/debug.m4, m4/devel.m4, m4/gccoptim.m4,
m4/ndebug.m4: Replace AC_ERROR and AC_HELP_STRING by
by AC_MSG_ERROR and AS_HELP_STRING.
2021-01-18 09:23:14 +01:00
Alexandre Duret-Lutz
7efdd497a8 require Autoconf 2.69 for building from git
Part of issue #447.

Autoconf 2.69 was released in 2012, so it now widely available.  The
recent release of 2.70 is obsoleting some constructs, so it will be
easier on us if we do not have too many versions to support.

* HACKING, configure.ac: Require Autoconf 2.69.
2021-01-18 09:21:51 +01:00
Alexandre Duret-Lutz
4522891f13 * doc/org/oaut.org: Fix two broken displays of results. 2021-01-18 09:21:22 +01:00
Alexandre Duret-Lutz
0df98b33b0 bump copyright year
* bin/common_setup.cc, debian/copyright: Here.
2021-01-18 09:21:18 +01:00
Alexandre Duret-Lutz
319204e868 * lib/.gitignore: More files to ignore. 2021-01-18 09:21:14 +01:00
Alexandre Duret-Lutz
26c232759e * doc/org/install.org: apt-key is deprecated in Bullseye. 2021-01-18 09:21:01 +01:00
Florian Renkin
b16192ae19 translate: Correct the choice of the automaton with the fewest colors
* spot/twaalgos/translate.cc: here
2021-01-18 09:20:51 +01:00
Alexandre Duret-Lutz
3dfe0dad24 determinize: do not copy the "incomplete" property
Mentioned in issue #298.

* spot/twaalgos/determinize.cc: Do not copy prop_complete of
the input if it is false.
* NEWS: Mention the bug.
2021-01-18 09:20:23 +01:00
Alexandre Duret-Lutz
b073e70880 propagate: fix constness of scc_info argument
* spot/twaalgos/degen.cc,
spot/twaalgos/degen.hh (propagate_marks_vector, propagate_marks_here):
Take the scc_info* argument as const.
2021-01-18 09:17:30 +01:00
Alexandre Duret-Lutz
20e52cf7a5 * NEWS: Typo. 2021-01-18 09:16:22 +01:00
Alexandre Duret-Lutz
a7d5d00f71 debian: do not install README in both spot and spot-doc
* debian/spot-doc.docs: Delete this file.
* Makefile.am: Adjust.
2021-01-18 09:16:19 +01:00
Alexandre Duret-Lutz
05d2f5fe37 * .gitlab-ci.yml: Remove reference to registry.lrde.epita.fr. 2021-01-18 09:16:13 +01:00
Alexandre Duret-Lutz
791daed851 debian: use -flto=jobserver.
* debian/rules: Adjust to use the jobserver, don't pass 'u' to ar.
2021-01-18 09:15:14 +01:00
Alexandre Duret-Lutz
75b95fd0f4 debian: upgrade dh-compat and standards versions
* debian/compat, debian/control: Upgrade dh compat from 9 to 12.
* debian/rules: Upgrade standards from 3.9.6 to to 4.5.1.
2021-01-18 09:13:26 +01:00
Jerome Dubois
adce0d2bfd * spot/twa/twagraph: Fix undefined behavior. 2021-01-18 09:12:58 +01:00
Alexandre Duret-Lutz
6fd9717fbb simulation: remove unnecessary iteration
This fixes #442.

* spot/twaalgos/simulation.cc (iterated_simulations_): Initialize next
so that we can exit after the first iteration if no change was made.
* NEWS: Mention the bug.
2021-01-18 09:12:50 +01:00
Alexandre Duret-Lutz
30b165d821 twagraph: fix merge_edges() ignoring the first edge
This fixes #441, reported by Jérôme Dubois.

* tests/python/mergedge.py: New file.
* tests/Makefile.am: Add it.
* spot/twa/twagraph.cc (merge_edges): Fix initialization of second
loop.
* NEWS: Mention the bug.
2021-01-18 09:12:38 +01:00
Alexandre Duret-Lutz
013eef7499 * .gitlab-ci.yml (alpine-gcc): Do not run both check and distcheck. 2021-01-17 21:45:51 +01:00
Alexandre Duret-Lutz
7a9f0a3fd9 gfguarantee: fix automaton modification during iteration
Fixes #449.

* spot/twaalgos/gfguarantee.cc (do_g_f_terminal_inplace): Save
edge additions to perform them after the loop.  Otherwise,
reallocating the edge buffer might break the iteration.
2021-01-17 21:45:51 +01:00
Alexandre Duret-Lutz
44c074bbad python: fix incorrect assertions on temporary objects
* tests/python/stutter.py: Do not call acc() on a temporary
object, and fix the last two asserts.
2021-01-17 20:48:56 +01:00
Alexandre Duret-Lutz
8e8f77756d gen, bitset: use clz() to simplify
Fixes #448.

* spot/gen/automata.cc (ulog2): Here.
* spot/misc/bitset.hh: And there.
2021-01-17 18:03:09 +01:00
Alexandre Duret-Lutz
d1cc45f223 clz: inline the implementation
__builtin_clz() can be implemented with two x86 instructions, so we
don't want to hide it behind a function call.

* spot/misc/clz.cc: Delete the implementation.
* spot/misc/Makefile.am: Delete clz.cc.
* spot/misc/clz.hh: Make the implementation public.
2021-01-17 18:02:53 +01:00
Alexandre Duret-Lutz
a8ee291abe * tests/python/ipnbdoctest.py: Work around failures on Fedora. 2021-01-16 16:33:30 +01:00
Alexandre Duret-Lutz
99bc0f998f * .gitlab-ci.yml (before_script): Debug parallelization settings. 2021-01-16 16:33:30 +01:00
Alexandre Duret-Lutz
094a6fa57e patch gnulib to accomodate autoconf 2.70
Upgrading gnulib turned to be too difficult, so this only includes
updates to m4 files necessary to please Autoconf 2.70.

For issue #447.

* m4/extensions.m4, m4/malloc.m4, m4/std-gnu11.m4: Cherry-pick
from today's gnulib version.
2021-01-14 15:29:48 +01:00
Alexandre Duret-Lutz
06b5a82950 [buddy] update obsolete autoconf constructs
Part of #447.

* configure.ac, m4/bdebug.m4: Replace AC_ERROR and AC_HELP_STRING by
by AC_MSG_ERROR and AS_HELP_STRING.
2021-01-14 15:15:39 +01:00
Alexandre Duret-Lutz
e076645382 update obsolete autoconf constructs
Part of #447.

* configure.ac, m4/debug.m4, m4/devel.m4, m4/gccoptim.m4,
m4/ndebug.m4: Replace AC_ERROR and AC_HELP_STRING by
by AC_MSG_ERROR and AS_HELP_STRING.
2021-01-14 15:15:39 +01:00
Alexandre Duret-Lutz
e497ee26dd require Autoconf 2.69 for building from git
Part of issue #447.

Autoconf 2.69 was released in 2012, so it now widely available.  The
recent release of 2.70 is obsoleting some constructs, so it will be
easier on us if we do not have too many versions to support.

* HACKING, configure.ac: Require Autoconf 2.69.
2021-01-12 09:28:36 +01:00
Alexandre Duret-Lutz
da869b7ddf * debian/copyright: Add missing licenses for m4/ files. 2021-01-11 20:46:36 +01:00
Alexandre Duret-Lutz
92ce384c80 fix compilation of core/bricks with clang++10
* configure.ac: Call CHECK_ATOMIC after setting the C++ options.
This is probably not necessary, but it makes more sense.
* m4/l_atomic.m4: Augment the test body with a scenario
that actually requires -latomic.
2021-01-11 20:46:36 +01:00
Alexandre Duret-Lutz
170a4ac164 * doc/org/oaut.org: Fix two broken displays of results. 2021-01-07 10:05:00 +01:00
Alexandre Duret-Lutz
449c1a582a bump copyright year
* bin/common_setup.cc, debian/copyright: Here.
2021-01-05 12:54:48 +01:00
Alexandre Duret-Lutz
1d8b00cf4c * lib/.gitignore: More files to ignore. 2021-01-05 12:54:47 +01:00
Alexandre Duret-Lutz
4a626c34e7 * doc/org/install.org: apt-key is deprecated in Bullseye. 2021-01-05 12:54:28 +01:00
Alexandre Duret-Lutz
8785f5a74b bin: add support for -b/--buchi
* bin/common_post.cc, bin/randaut.cc: Implement -b/--buchi.
Also add --sba as alias for -B, and --gba as alias for --tgba.
* NEWS: Document those changes.
* doc/org/ltl2tgba.org, doc/org/oaut.org: Adjust documentation.
* tests/core/ltl2tgba2.test, tests/core/ltlcross2.test,
tests/core/randaut.test: Add more tests.
* tests/core/sbacc.test: --sbacc cannot be abbreviated as --sba
anymore.
2020-12-18 12:24:08 +01:00
Florian Renkin
7c6b35313a translate: Correct the choice of the automaton with the fewest colors
* spot/twaalgos/translate.cc: here
2020-12-16 12:51:40 +01:00
Alexandre Duret-Lutz
7e2f091839 determinize: do not copy the "incomplete" property
Mentioned in issue #298.

* spot/twaalgos/determinize.cc: Do not copy prop_complete of
the input if it is false.
* tests/python/298.py: Test it.
* NEWS: Mention the bug.
2020-12-15 10:47:25 +01:00
Alexandre Duret-Lutz
f6be083050 determinize: don't emit colors for temporary braces
Related to issue #298.

* spot/twaalgos/determinize.cc: Recognize braces that are temporary
to avoid emitting colors when they become empty.
* tests/python/298.py: New file, showing a reduction of colors.
* tests/Makefile.am: Add it.
* tests/core/ltlsynt.test: Adjust expected output (now smaller).
* tests/core/genltl.test: Adjust one expected output (now larger).
* NEWS: Mention the issue.
2020-12-15 07:58:42 +01:00
Alexandre Duret-Lutz
142460628c translate: add support for -x exprop
This helped confirming a behavior observed in #298.

* spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add support
for -x exprop.
* bin/spot-x.cc, NEWS: Document it.
* tests/core/ltl2tgba2.test: Test it.
2020-12-14 17:46:03 +01:00
Alexandre Duret-Lutz
71f1928052 propagate: fix constness of scc_info argument
* spot/twaalgos/degen.cc,
spot/twaalgos/degen.hh (propagate_marks_vector, propagate_marks_here):
Take the scc_info* argument as const.
2020-12-14 13:11:59 +01:00
Alexandre Duret-Lutz
9a17f5676c game: rewrite, document, and rename solve_reachability_game
* spot/twaalgos/game.hh, spot/twaalgos/game.cc: Rename
solve_reachability_game() as solve_safety_game(), rewrite it (the old
implementation incorrectly marked dead states as winning for their
owner).
* tests/python/paritygame.ipynb: Rename as...
* tests/python/games.ipynb: ... this, and illustrate
solve_safety_game().
* tests/Makefile.am, NEWS, doc/org/tut.org: Adjust.
* tests/python/except.py: Add more tests.
2020-12-10 15:04:07 +01:00
Alexandre Duret-Lutz
05449a42d3 move game.cc from misc/ to twaalgos/
* spot/misc/game.cc, spot/misc/game.hh: Move...
* spot/twaalgos/game.cc, spot/twaalgos/game.hh: ... here.
* bin/ltlsynt.cc, python/spot/impl.i, spot/misc/Makefile.am,
spot/twaalgos/Makefile.am: Adjust.
2020-12-09 16:47:18 +01:00