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

5317 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
32e9bd4dbf Release Spot 2.8.7 
* NEWS, configure.ac, doc/org/setup.org: Update.
 2020-03-13 07:53:38 +01:00
Alexandre Duret-Lutz
c368903398 ltlcross: detect write errors for --save-bogus and --grind 
* bin/ltlcross.cc: Explicitly close those files to check for
error conditions.
* NEWS: Mention it.
 2020-03-13 07:52:34 +01:00
Alexandre Duret-Lutz
0940c9a25a stutter: fix sl, sl2 to never accept on added self-loop 
Fixes #401, reported by Victor Khomenko.

* spot/twaalgos/stutter.cc (sl, sl2): If {} is accepting, upgrade the
acceptance condition.
* tests/python/stutter.py: Add test cases.
 2020-03-12 22:51:13 +01:00
Alexandre Duret-Lutz
7aec23f019 sccinfo: fix generation of self-loop accepting runs 
Reported by Juraj Major.

* spot/twaalgos/sccinfo.cc (scc_info::get_accepting_run): Do not
assume TRACK_STATES is enabled.
* tests/core/autcross5.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
 2020-03-12 22:49:56 +01:00
Alexandre Duret-Lutz
e2ec711c40 autfilt: fix -u 
Fixes #399.

* bin/autfilt.cc: Fix it.
* tests/core/isomorph.test: Add test case.
* NEWS: Mention the issue.
 2020-03-12 22:49:38 +01:00
Alexandre Duret-Lutz
5b8dbc6549 product: fix handling of operand with false acceptance 
* NEWS: Mention the issue.
* spot/twaalgos/product.cc: Fix it.
* tests/python/prodexpt.py: Test it.
 2020-03-12 22:49:26 +01:00
Alexandre Duret-Lutz
fa90a97d54 org: fix some typos 
* doc/org/tut12.org: Here.
 2020-03-12 22:49:14 +01:00
Alexandre Duret-Lutz
3820f369b0 genem: fix suboptimal selection of Fin to remove 
* spot/twaalgos/genem.cc: If a disjunct has no unit-Fin to remove the
code should select any Fin occuring in the disjunct, but it was
selecting any Fin occuring in the acceptance condition (made of
disjuncts) instead.  This could potentially double the number of
recursive calls.
 2020-03-12 22:47:03 +01:00
Alexandre Duret-Lutz
c98f82dc36 * NEWS, configure.ac: Bump version to 2.8.6.dev. 2020-02-19 14:47:34 +01:00
Alexandre Duret-Lutz
39fa829340 Release Spot 2.8.6 
* NEWS, configure.ac, doc/org/setup.org: Update version.
 2020-02-19 14:45:07 +01:00
Alexandre Duret-Lutz
00cd9b7719 doc: add DOIs to most citations 
* doc/spot.bib: Here.
* doc/tl/tl.tex: Fix a citation.
 2020-02-19 10:52:15 +01:00
Alexandre Duret-Lutz
05cf6683ce * tests/run.in: reset some envvars to avoid spurious failures. 2020-02-19 10:52:15 +01:00
Alexandre Duret-Lutz
de5704049d tgba_determinize: improve citations in doc 
* doc/spot.bib (klein.07.ciaa, redziejowski.12.fi): Add two entries.
* spot/twaalgos/determinize.hh: Use them.
 2020-02-19 10:52:15 +01:00
Alexandre Duret-Lutz
80b04e10b5 update citations of generic emptiness-check 
* doc/org/citing.org, doc/spot.bib: Here.
 2020-02-19 10:52:15 +01:00
Alexandre Duret-Lutz
aad5b135ef fix is_generalized_rabin() and is_generalized_streett() 
* spot/twa/acc.cc: Fix detection of single-pairs gen-Rabin and
gen-Streett.
* tests/core/randaut.test: Add test case.
* NEWS: Mention this issue.
 2020-02-19 10:52:15 +01:00
Alexandre Duret-Lutz
9365f8de1b relabel: do not create automata with false labels 
* spot/twaalgos/relabel.cc: Remove false transitions if
some of the propositions are equivalent to true or false.
* NEWS: Mention the bug.
* tests/core/ltl2tgba2.test: Test it.
 2020-02-19 10:52:15 +01:00
Alexandre Duret-Lutz
cf2cfcd2fb _postproc_translate_options: fix syntax error 
* python/spot/__init__.py: Here.
* tests/python/except.py: Add test.
* NEWS: Mention the issue.
 2020-02-19 10:52:15 +01:00
Alexandre Duret-Lutz
e7ae3d3ae0 fix degeneralize_tba after accepting transition 
* spot/twaalgos/degen.cc (degeneralize_tba): Here.
* tests/python/simstate.py: Adjust expected values.
* NEWS: Mention the bug.
 2020-02-19 10:52:15 +01:00
Alexandre Duret-Lutz
abab62dd3e * doc/org/concepts.org: Typo. 2020-02-19 10:42:11 +01:00
Alexandre Duret-Lutz
fd92d20fd3 ipnbdoctest: attempt to restart when the kernel dies 
* tests/python/ipnbdoctest.py: Catch kernel deaths, wait a random
number of seconds, and try again up to three times.
 2020-02-19 10:42:04 +01:00
Alexandre Duret-Lutz
d8ed0fb8ab * NEWS, configure.ac: Bump version to 2.8.5.dev. 2020-01-04 14:24:49 +01:00
Alexandre Duret-Lutz
68435915e7 Release Spot 2.8.5 
* NEWS, configure.ac, doc/org/setup.org: Bump version number.
 2020-01-04 14:19:33 +01:00
Alexandre Duret-Lutz
49bfefb46e ipnbdoctest: attempt to deal with buildfarm timeouts 
* tests/python/ipnbdoctest.py: Use shorter timeouts, and flush the
shell messages without expecting them.
 2020-01-03 20:32:58 +01:00
Alexandre Duret-Lutz
a65ddf5b53 bump copyright year 
* bin/common_setup.cc, debian/copyright: Here.
 2020-01-01 16:21:56 +01:00
Alexandre Duret-Lutz
265332dedf twagraph: merge_edge() can determinize automata 
Reported by František Blahoudek.

* spot/twa/twagraph.cc: Reset prop_universal() if edges are merged in
a non-deterministic automaton.
* tests/core/det.test: Add test case.
* NEWS: Mention the issue.
 2020-01-01 16:18:44 +01:00
Alexandre Duret-Lutz
383d1c003c ltl2tgba, ltldo: fix location of --negate in --help output 
* bin/common_finput.cc, bin/ltl2tgba.cc, bin/ltldo.cc: Make sure
--negate is listed along with input options.
 2020-01-01 16:18:44 +01:00
Alexandre Duret-Lutz
1f90e1cff9 fix ltl2tgba -B not always returning Inf(0) 
Reported by František Blahoudek.

* spot/twaalgos/postproc.cc: Turn "t" into "Inf(0)" for BA.
* tests/core/ltl2tgba.test: Add test case.
* NEWS: Mention the bug.
 2020-01-01 16:18:44 +01:00
Alexandre Duret-Lutz
67b9bfda08 tmpfile: improve error message 
* spot/misc/tmpfile.cc: Display strerror(errno) plus some suggestions
that depend on the error.  Based on a report from Shengping Shaw.
* THANKS: Add reporter.
* tests/core/ltlcross5.test: New file.
* tests/Makefile.am: Add it.
 2019-12-31 22:42:45 +01:00
Alexandre Duret-Lutz
b9cac2cedb * spot/twaalgos/emptiness.cc: Fix another gcc-snapshot warning. 2019-12-31 22:42:42 +01:00
Alexandre Duret-Lutz
9b9c2b3c94 * spot/twaalgos/compsusp.cc: Fix a warning from gcc-snapshot. 2019-12-31 22:42:39 +01:00
Alexandre Duret-Lutz
44d9a629b1 * NEWS, configure.ac: Bump version to 2.8.4.dev. 2019-12-08 13:37:00 +01:00
Alexandre Duret-Lutz
625a2e2836 Release Spot 2.8.4 
* NEWS, configure.ac, doc/org/setup.org: Set version to 2.8.4.
 2019-12-08 13:35:01 +01:00
Alexandre Duret-Lutz
e374b95689 bin: fix documentation of --trust-hoa 
* bin/common_hoaread.cc: Here.  Reported by Juraj Major.
 2019-12-08 13:32:58 +01:00
Alexandre Duret-Lutz
adc7c93448 remfin: fix tra_to_tba 
This fixes a complementation bug reported by Juraj Major and Tereza
Šťastná.

* spot/twaalgos/remfin.cc (is_scc_tba_type): Fix the condition for
handling Fin-alone pairs.
* tests/core/complement.test: Add Juraj & Tereza's test case.
* NEWS: Mention it.
 2019-12-08 13:32:58 +01:00
Alexandre Duret-Lutz
71fef458e1 python: define our own SVG DisplayObject 
This is to workaround differences in minidom's pretty-printing that
occurred between Python 3.7 and 3.8.

* python/spot/jupyter.py (SVG): New class.
* python/spot/__init__.py: Use it.
* tests/python/_altscc.ipynb, tests/python/alternation.ipynb,
tests/python/automata.ipynb, tests/python/formulas.ipynb,
tests/python/gen.ipynb, tests/python/highlighting.ipynb,
tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
tests/python/product.ipynb, tests/python/randaut.ipynb,
tests/python/testingaut.ipynb, tests/python/twagraph-internals.ipynb,
tests/python/word.ipynb: Adjust.
 2019-12-08 13:29:26 +01:00
Alexandre Duret-Lutz
317520efe8 org: improve architecture diagram 
* doc/org/arch.tex: Improve diagram, add links and online services.
* doc/org/concepts.org: Update text.
 2019-12-08 13:29:14 +01:00
Alexandre Duret-Lutz
56e08af896 * NEWS, configure.ac: Bump version to 2.8.3.dev. 2019-11-06 09:56:25 +01:00
Alexandre Duret-Lutz
7ece494794 release Spot 2.8.3 
* NEWS, configure.ac, doc/org/setup.org: Set version to 2.8.3.
 2019-11-06 09:54:52 +01:00
Alexandre Duret-Lutz
44a79b1b89 work around recent GraphViz bug in SVG scaling 
See https://gitlab.com/graphviz/graphviz/issues/1605.

* python/spot/aux.py (str_to_svg): Invert the scale parameters
if they are both greater than one.
 2019-10-28 14:53:32 +01:00
Alexandre Duret-Lutz
0e681ed060 acc: improve diagnostics for algorithms that use too many colors 
* spot/twa/acc.hh (acc_cond::mark_t): Diagnose mark_t with set numbers
that are too larges.
* tests/python/except.py: Adjust.
* tests/core/acc.cc: Remove most of asserts, as those can be disabled,
and adjust expected exception.
 2019-10-28 14:53:32 +01:00
Etienne Renault
f31864488b core: random_shuffle is deprecated and not portable 
* tests/core/parity.cc: Here.
 2019-10-28 14:53:32 +01:00
Alexandre Duret-Lutz
9e38273172 trim: avoid the soon-to-be-deprecated std::ptr_fun 
Reported by Etienne Renault.

* spot/priv/trim.cc: Simplify with a lambda.
 2019-10-28 14:53:32 +01:00
Alexandre Duret-Lutz
e864baf6e7 * bin/ltlsynt.cc: Typo. 2019-10-28 14:53:32 +01:00
Alexandre Duret-Lutz
2960b8138c "import spot.foo" may now load "spot-extra/foo.py" 
This is needed for tcltl.

* python/spot/__init__.py: Alter __path__ to add any spot-extra/
directory we find.
* NEWS: Mention this.
 2019-10-28 14:53:32 +01:00
Alexandre Duret-Lutz
865427c73b python: remove workaround for swig 2.0.2 
* python/spot/gen.i, python/spot/impl.i, python/spot/ltsmin.i: Here.
 2019-10-28 14:53:32 +01:00
Alexandre Duret-Lutz
d15ce1a773 * NEWS: Fix many typos. 2019-10-28 14:53:30 +01:00
Alexandre Duret-Lutz
b28c8a5973 * debian/control (libspotgen0): Fix leading spaces in description. 2019-10-28 14:52:22 +01:00
Alexandre Duret-Lutz
750fcca7b7 debian: use local version of require.js 
* debian/control (spot-doc): Depends on libjs-requirejs.
* debian/rules (fix-js): Replace uses.
 2019-10-28 14:52:22 +01:00
Alexandre Duret-Lutz
24a48c9f1e debian: remove -flo workaround 
* debian/rules: Here.
 2019-10-28 14:52:22 +01:00
Alexandre Duret-Lutz
cbfcee9449 Bump version to 2.8.2.dev 
* NEWS, configure.ac: Here.
 2019-09-27 20:45:34 +02:00