alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
5600 commits 6 branches 0 tags 36 MiB
Commit graph

5600 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
773939bebe typos: coma -> comma 
* ChangeLog.1, tests/core/autcross3.test, tests/core/ltl3ba.test,
tests/core/ltl3dra.test, tests/core/ltlcross3.test,
tests/core/ltlsynt.test, tests/sanity/style.test: Here.
 2021-08-10 13:26:12 +02:00
Alexandre Duret-Lutz
2e14eb0c02 [buddy] typo coma -> comma 
* ChangeLog.1: Here.
 2021-08-10 13:25:28 +02:00
Alexandre Duret-Lutz
eeccd5804d * spot/graph/graph.hh (chain_edges_): Typo in doc. 2021-08-10 13:24:55 +02:00
Alexandre Duret-Lutz
30e82e7b1f Bump version to 2.9.7.dev 
* NEWS, configure.ac: Here.
 2021-05-12 15:56:02 +02:00
Alexandre Duret-Lutz
bc768a7157 Release Spot 2.9.7 
* NEWS, configure.ac, doc/org/setup.org: Update for 2.9.7.
 2021-05-12 15:54:55 +02:00
Alexandre Duret-Lutz
d3df766e56 org: add missing :exports results :results silent 
* doc/org/ltlfilt.org, doc/org/tut30.org, doc/org/tut31.org: Hide rm
invocations used for cleanup.
 2021-05-12 10:27:46 +02:00
Alexandre Duret-Lutz
6253885af7 improve documentation for -x sat-minimize 
* bin/man/spot-x.x, bin/spot-x.cc: Improve documentation of SAT-based
minimization.  It was still referring to TGBA although it works for
TwA.
* spot/twaalgos/postproc.cc: Typo.
 2021-05-12 10:26:54 +02:00
Alexandre Duret-Lutz
caca8728fe * spot/twa/twagraph.cc (remove_unused_ap): Remove unused variable. 2021-05-12 10:24:50 +02:00
Alexandre Duret-Lutz
7ef69fa15b * doc/tl/tl.tex: Typo reported by Florian. 2021-05-12 10:24:29 +02:00
Alexandre Duret-Lutz
084964a9ff autfilt: fix incorrect diagnostic 
* bin/autfilt.cc (OPT_KEEP_STATES): Mention the correct option.
* tests/core/maskkeep.test: Test for it.
* NEWS: Mention the bug.
 2021-05-12 10:24:12 +02:00
Alexandre Duret-Lutz
cad3d7706c twagraph: improve doc 
Based on report by Michaël Cadilhac.

* spot/graph/graph.hh, spot/twa/twagraph.hh (defrag_state): Clarify
that only unreachable states are meant to be removed.
* spot/twa/twagraph.hh (merge_edges): Typo in comment.  Fixes #457.
* THANKS: Add Michaël.
 2021-05-12 10:22:42 +02:00
Alexandre Duret-Lutz
4d23b7b770 work around a GraphViz 2.60.0 bug 
* spot/twa/twagraph.cc (dump_storage_as_dot): Prefer \n over a plain
new line to work around GraphViz issue 1931, which was causing
twagraph-internals.ipynb to fail in our test suite.
 2021-05-12 10:13:56 +02:00
Alexandre Duret-Lutz
244e3a9731 fix eventual/universal properties for ->/<->/xor 
* spot/tl/formula.cc: Correctly set eventual and universal properties
for ->, <->, and xor.  This wasn't really relevant before, but there
are now situation where those are not rewritten.
* tests/core/kind.test: Adjust expected output.
* tests/core/ltl2tgba2.test: New test case, reported by Florian
Renkin.
* NEWS: Mention the bug.
 2021-05-12 10:13:38 +02:00
Alexandre Duret-Lutz
b6c4145599 merge_edge: clarify documentation 
Reported by Florian Renkin.

* spot/graph/graph.hh, spot/twa/twagraph.hh (merge_edge): Document
that it is expected that state i can only be renamed as j if j≤i.
 2021-05-12 10:11:35 +02:00
Alexandre Duret-Lutz
fe007b9de3 * doc/org/setup.org: Fix last release date. 2021-05-12 10:09:40 +02:00
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
c5c8e8c516 * NEWS, configure.ac: Bump version. 2020-11-19 10:42:46 +01:00
Alexandre Duret-Lutz
a5385bb886 Release Spot 2.9.5 
* configure.ac, NEWS, doc/org/setup.org: Update version.
 2020-11-19 10:41:35 +01:00
Alexandre Duret-Lutz
aecdab7ba7 * NEWS: Update for recent fixes. 2020-11-08 14:20:17 +01:00
Alexandre Duret-Lutz
bcd88df0fe python: rename aux.py to aux_.py 
Fixes #437, reporeted by Yann Thierry-Mieg.

* python/spot/aux.py: Rename as...
* python/spot/aux_.py: ... this.
* python/spot/__init__.py, python/Makefile.am: Adjust.
* NEWS: Mention the change.
 2020-11-08 14:11:37 +01:00
Alexandre Duret-Lutz
5ea20db6b4 ltlsmin: fix incorrect check for dlsym error 
Fix #435 reported by Yann Thierry-Mieg.

* spot/ltsmin/ltsmin.cc (sym): Fix incorrect check introduced
by dc4a477172.
 2020-11-08 13:45:01 +01:00
Alexandre Duret-Lutz
7697adf645 org: work around ESS issue 1052 
This was causing all our build to fail.

* doc/org/init.el.in: Here.
 2020-11-08 13:42:09 +01:00
Alexandre Duret-Lutz
53a68f99f4 org: various improvements 
* doc/org/spot.css: Improve style and responsiveness.
* doc/org/oaut.org, doc/org/ioltl.org: Fix some ugly outputs.
 2020-11-08 13:41:57 +01:00
Alexandre Duret-Lutz
4ca2f394e4 org: fix local export 
* doc/org/.dir-locals.el.in: Remove incorrect quote.
 2020-11-08 13:41:41 +01:00
Alexandre Duret-Lutz
ef41b6af56 tests: do not override DYLD_LIBRARY_PATH 
* tests/run.in: Here.
 2020-11-08 13:41:32 +01:00
Alexandre Duret-Lutz
5401d4c8ce tests: fix import of libspotgen on Darwin 
Fixes #426, reported by Étienne Renault.

* tests/run.in: Augment modpath.
 2020-11-08 13:41:25 +01:00