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

5520 commits

This branch
This branch
All branches
Author SHA1 Message Date
Florian Renkin
6489d6c091 ltlsynt: Correct segfault with ds algorithm and verbose 
* bin/ltlsynt.cc: Use initialized DPA when printing when
 we use DET_SPLIT and verbose.
 2020-03-22 16:04:44 +01:00
Alexandre Duret-Lutz
e827d3a634 Merge branch 'master' into next 2020-03-13 08:07:16 +01:00
Alexandre Duret-Lutz
f53338e8ad * NEWS, configure.ac: Bump version to 2.8.7.dev. 2020-03-13 08:04:48 +01:00
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
b5d688dc97 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/core/stutter-tgba.test, tests/python/stutter.py: Add test cases.
 2020-03-12 21:54:13 +01:00
Alexandre Duret-Lutz
150f815c87 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 17:06:03 +01:00
Alexandre Duret-Lutz
ceb5210569 * NEWS: Typos. 2020-03-11 23:14:29 +01:00
Alexandre Duret-Lutz
f9f4fd1c89 ltlcross --save-inclusion-products: name the saved automata 
* bin/ltlcross.cc: Name saved automata for easier tracking.
 2020-03-11 23:06:19 +01:00
Alexandre Duret-Lutz
124de77925 autfilt: fix -u 
Fixes #399.

* bin/autfilt.cc: Fix it.
* tests/core/isomorph.test: Add test case.
* NEWS: Mention the issue.
 2020-03-11 23:05:15 +01:00
Alexandre Duret-Lutz
c3d7e942d3 ltlfilt, autfilt: add support for --nth 
* bin/autfilt.cc, bin/ltlfilt.cc: Implement it.
* NEWS: Mention it.
* tests/core/genaut.test, tests/core/genltl.test: Add test cases.
 2020-03-11 11:42:31 +01:00
Alexandre Duret-Lutz
4e99518da7 ltlcross: do not use remove_fin anymore 
* bin/ltlcross.cc: Since is_empty() now works with arbitrary
acceptance conditions, calling remove_fin() is not necessary anymore.
* tests/core/ltlcrossce.test: Adjust.
* NEWS: Mention the change.
 2020-03-09 17:51:44 +01:00
Alexandre Duret-Lutz
addaf7f5b0 ltlcross: detect write errors for --save-bogus, --grind, etc 
* bin/ltlcross.cc: Explicitly close those file to check for
error conditions.
* tests/core/full.test: Add one test.
 2020-03-08 09:15:06 +01:00
Alexandre Duret-Lutz
3805b63e24 ltlcross: add option --save-inclusion-products 
* NEWS: Mention it.
* bin/ltlcross.cc: Implement it.
* tests/core/ltlcross3.test: Test it.
 2020-03-08 09:15:06 +01:00
Alexandre Duret-Lutz
d8a0f307eb 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-08 09:15:06 +01:00
Alexandre Duret-Lutz
7f0ef7ad59 genem: improve the worst case 
* spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Improve the worst
case by not recurring twice into each disjunct individually.  Keep
the previous two implementation available and add a function
generic_emptiness_check_select_version() so we can benchmark the
difference.
* tests/python/genem.py: Test the three versions.
 2020-03-06 12:38:20 +01:00
Alexandre Duret-Lutz
73277bed96 org: fix some typos 
* doc/org/tut12.org: Here.
 2020-03-04 23:22:21 +01:00
Alexandre Duret-Lutz
d4b8ecdf90 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-04 16:41:23 +01:00
Alexandre Duret-Lutz
332f830d58 * HACKING: Update various bits. 2020-03-02 23:17:38 +01:00
Florian Renkin
6f3208a783 CAR: Correct the value of the max color of the acceptance condition 
* spot/twaalgos/car.cc: Update the max_color in apply_to_Buchi.
* tests/python/car.py: Add some tests that showed this issue.
 2020-02-26 15:40:52 +01:00
Florian Renkin
4b9704a072 Check that every color appears once in is_parity_max_equiv 
* spot/twa/acc.cc: Now suppose that a condition cannot contain
the same mark twice to be parity equivalent.
 2020-02-26 15:40:52 +01:00
Florian Renkin
f4c201c980 Correct CAR when we use apply_to_Buchi 
* spot/twaalgos/car.cc: Correct the colors producted in apply_to_Buchi.
 2020-02-26 15:40:52 +01:00
Florian Renkin
a62241376f Add mores cases in car.py 
* tests/python/car.py: Add more combinaisons of options
when testing CAR.
 2020-02-26 15:40:52 +01:00
Florian Renkin
9ec0f6bd09 fixup! IAR: Correct parity prefix 
* spot/twaalgos/car.cc: Reduce the number of colors used by parity
prefix and check that it uses parity colors in apply_to_Buchi.
 2020-02-26 15:40:52 +01:00
Florian Renkin
1b9acf32cf IAR: Use less colors with parity prefix and check that use parity colors 
* spot/twaalgos/car.cc: Don't reserve colors when parity prefix is used
but the condition has no parity prefix and use colors of prefix in
apply_to_Buchi.
 2020-02-26 15:40:16 +01:00
Florian Renkin
de8cd91e94 * AUTHORS: Add myself. 2020-02-24 15:05:40 +01:00
Florian Renkin
96531f29f2 CAR: new algorithm for paritizing 
* NEWS: Mention it.
* spot/twaalgos/car.cc, spot/twaalgos/car.hh, tests/python/car.py:
New files.
* spot/twaalgos/Makefile.am, tests/Makefile.am: Add them.
* python/spot/impl.i: Include CAR.
* spot/twa/acc.cc, spot/twa/acc.hh, spot/twa/twagraph.cc,
spot/twa/twagraph.hh: Add supporting methods.
 2020-02-24 15:05:40 +01:00
Florian Renkin
5d021a18d6 IAR: Add pretty print option and better lookup of existing states 
* spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh: here.
 2020-02-24 15:05:39 +01:00
Alexandre Duret-Lutz
8a4a4b9fff simplify_acceptance: fix erroneous simplification 
Reported by Florian Renkin.

* spot/twaalgos/cleanacc.cc: Do not rewrite
...Fin(0)&(Fin(1)|(Fin(3)&Inf(4)))... as Fin(0)&f when it appears that
{1,3} cannot receive {0}, because {1} is used elsewhere in the
acceptance.
* tests/python/simplacc.py: Add test case.
 2020-02-24 12:17:07 +01:00
Alexandre Duret-Lutz
b44daef42a Merge branch 'master' into next 2020-02-19 15:09:25 +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
e0d8188701 doc: add DOIs to most citations 
* doc/spot.bib: Here.
* doc/tl/tl.tex: Fix a citation.
 2020-02-19 10:40:40 +01:00
Alexandre Duret-Lutz
5afa528df0 pdegen: fix another original-states related issue 
* spot/twaalgos/degen.cc (keep_bottommost_copies): Fix intialisation
of bottommost_occurence.
* tests/python/pdegen.py: Add test case sent by Florian Renkin.
 2020-02-16 20:02:48 +01:00