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

5722 commits

This branch
This branch
All branches
Author SHA1 Message Date
Alexandre Duret-Lutz
4608d9a5b1 [buddy] avoid cache errors in bdd_satcount() and friends 
* src/bddop.c (bdd_satcount, bdd_satcountln): If the number of
declared variables changed since we last used it, reset misccache.
Otherwise, bdd_satcount() and friends might return incorrect results
after the number of variable is changed.  These is needed for the next
patch in Spot to pass all tests.
(misccache_varnum): New global variable to track that.
(bdd_satcountset): Make sure that bdd_satcountset(bddtrue, bddtrue)
return 1.0 and not 0.0.
 2020-07-13 16:30:29 +02:00
Alexandre Duret-Lutz
fc1c17b91c ltlsynt: make sure the previous Xor optimization actually works 
* spot/tl/simplify.hh, spot/tl/simplify.cc,
spot/twaalgos/translate.cc: Update the tl_simplification
options after all preferences have been given.
* bin/ltlsynt.cc: Display the size of the translation output.
* tests/core/ltlsynt.test: Add test case.
 2020-07-13 16:30:29 +02:00
Alexandre Duret-Lutz
6ec6150462 translate: improve handling of Xor and Equiv at top-level for -G -D 
* spot/tl/formula.hh: Add variant of formula::is that support 4
arguments.
* spot/tl/simplify.hh, spot/tl/simplify.cc: Add option keep_top_xor
to preserve Xor and Equiv at the top-level.
* spot/twaalgos/translate.cc: Adjust ltl-split to deal with Xor and
Equiv for the -D -G case.
* NEWS: Mention that.
* tests/core/ltl2tgba2.test: Add test case.
* tests/python/simstate.py: Adjust expected result.
 2020-07-13 16:30:29 +02:00
Alexandre Duret-Lutz
822b749166 product: add product_xor() and product_xnor() 
* spot/twaalgos/product.cc, spot/twaalgos/product.hh: Add those
functions.
* tests/python/_product_weak.ipynb, tests/python/except.py: Test them.
* NEWS: Mention them.
 2020-07-13 16:30:29 +02:00
Alexandre Duret-Lutz
918548a03d run: fix reduce on automata with Fin 
Reported by Florian Renkin.

* spot/twaalgos/emptiness.cc (reduce): If the automaton uses Fin
acceptance, check the reduced cycle and revert to the original cycle
if necessary.
* tests/python/intrun.py: New file.
* tests/Makefile.am: Add it.
* spot/twaalgos/emptiness.hh: Improve documentation.
 2020-07-10 18:05:18 +02:00
Alexandre Duret-Lutz
6dbdd89fc1 genem: replace one recursive call by a loop 
* spot/twaalgos/genem.cc: In the spot29 implementation for the generic
case, when Fin(fo)=true and Fin(fo)=false have to be tested
separately, the second test can be done by a loop instead of a
recursion, to avoid unnecessary processing of the acceptance
condition.  Suggested by Jan Strejček.
 2020-06-18 15:32:54 +02:00
Etienne Renault
b3c7994a1d bricks: rework tests 
On some architectures this test fails due to several
reasons:
    - missing headers
    - use of valueAt instead of count in ConCS. Indeed,
    valueAt acts similarly to count but avoids some validity
    check that are required when the hashmap is growing.

This patch also:
     - removes inaccurate comments from bricks.test.
     - test more features for hashset.

* spot/bricks/brick-hashset,
tests/core/bricks.cc,
tests/core/bricks.test: Here.
 2020-06-11 08:56:56 +02:00
Etienne Renault
f748281719 HACKING: precisions for debugging under MacOS 
* HACKING: Here.
 2020-06-10 11:49:47 +02:00
Etienne Renault
68014e46fc HACKING: rename src to spot 
* HACKING: Here.
 2020-06-10 10:07:14 +02:00
Etienne Renault
9b4d51e3db cube: prefer value_initialization 
* spot/twacube/cube.cc: Here.
 2020-06-10 10:07:14 +02:00
Etienne Renault
9411dab738 lpar13: avoid leak when counterexample detected 
* spot/mc/lpar13.hh: Here.
 2020-06-10 10:07:14 +02:00
Etienne Renault
13402a63c4 bloemen_ec: avoid leak when counterexample detected 
* spot/mc/bloemen_ec.hh: Here.
 2020-06-10 10:07:14 +02:00
Etienne Renault
6a12b77360 sanity: fixes #417 
* tests/sanity/style.test: Here.
 2020-06-10 10:07:14 +02:00
Etienne Renault
47b31bd9eb bricks: include tests in test-suite 
* tests/Makefile.am,
tests/core/bricks.cc,
tests/core/bricks.test: Here.
 2020-06-10 10:07:06 +02:00
Etienne Renault
2098d41c05 bricks: details version and modifications 
* README, spot/bricks/README: Here.
 2020-06-10 09:02:11 +02:00
Etienne Renault
7d69708f73 modelchek: add more tests 
* tests/ltsmin/check.test,
tests/ltsmin/finite.test: Here.
 2020-06-10 09:02:02 +02:00
Etienne Renault
c94d877c98 modelcheck: adjust default value for deadlock 
* tests/ltsmin/modelcheck.cc: Here.
 2020-06-09 16:21:11 +02:00
Etienne Renault
d2bde1af19 modelcheck: do not load twice model 
* tests/ltsmin/modelcheck.cc: Here.
 2020-06-09 16:21:11 +02:00
Etienne Renault
4cd23d1fc5 lpar13: call finalize even when empty product 
* spot/mc/lpar13.hh: Here.
 2020-06-09 16:21:11 +02:00
Etienne Renault
d3eb269078 modelcheck: fix incorrect return value without --csv 
* tests/ltsmin/modelcheck.cc: Here.
 2020-06-09 16:21:11 +02:00
Etienne Renault
099387d831 mc: fixes #416 
* spot/mc/bloemen_ec.hh: Here.
 2020-06-09 16:21:11 +02:00
Etienne Renault
f5585525f0 twacube: cleanup API 
* spot/twacube/twacube.cc,
spot/twacube/twacube.hh: Here.
 2020-06-09 16:21:10 +02:00
Etienne Renault
c61b721a48 cube: more tests 
* tests/core/cube.cc, tests/core/cube.test: Here.
 2020-06-09 16:20:59 +02:00
Alexandre Duret-Lutz
6243803018 address a new g++-10 warnings 
* spot/twa/twa.hh (set_named_prop): Declare the lambda as noexcept.
* spot/twaalgos/couvreurnew.cc (acss_states): Likewise.
 2020-06-09 08:31:22 +02:00
Alexandre Duret-Lutz
da9d92eef7 swig: search for swig4.0 
* configure.ac: Use swig4.0 when available.
* HACKING: Update.
 2020-06-09 00:18:15 +02:00
Etienne Renault
1a8920d9b6 rpm: fixes commit 3acf2ca6 
* spot.spec.in, spot/Makefile.am: Here.
 2020-06-08 08:15:52 +02:00
Etienne Renault
b4412482c8 HACKING: swig-python is required for MacOS 
* HACKING: Here.
 2020-06-04 17:26:58 +02:00
Etienne Renault
3acf2ca689 rpm: add unpackaged files 
* spot.spec.in: Here.
 2020-06-04 14:09:54 +02:00
Etienne Renault
c20abb5a0f debian: remove useless directive 
* debian/libspot-dev.install: Here.
 2020-06-04 06:45:38 +02:00
Etienne Renault
330cd80fed twacube: fix typo 
* spot/twacube/twacube.hh: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
c06085a60b are_equivalent: remove redundant code 
* spot/twacube_algos/convert.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
ff48c81198 twacube_to_twa: allows use of existing BDD_dict 
* spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh: Here.
* tests/core/twacube.cc: Test it.
 2020-06-03 12:22:41 +02:00
Etienne Renault
b1b59d0eae cube: incorrect use of reverse_binder in are_equivalent 
Thanks to A. Martin for reporting this.

* spot/twacube_algos/convert.cc,
tests/core/twacube.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
e564dd1263 atomic: check if -latomic is required for std::atomic 
* configure.ac,
m4/l_atomic.m4,
python/Makefile.am,
tests/Makefile.am: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
6e0e6b923d NEWS: mention cube-based transformations 
* NEWS: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
61561ee9ac raspbian: add missing library 
* tests/Makefile.am,
python/Makefile.am: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
9a8745fcff tests: ignore thread affinity 
* tests/ltsmin/check.test,
tests/ltsmin/testconvert.test: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
7c9ae3d361 tests: add missing library 
* tests/Makefile.am: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
2a41772ff9 mc: remove old FIXME 
*  spot/mc/mc_instanciator.hh: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
1dc6ead1e0 mc: do not mix static and SPOT_API 
* spot/mc/mc_instanciator.hh: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
6d390a342d kripke: add missing SPOT_API 
* spot/kripke/kripke.hh: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
e484e0c471 mc: concept-like check for mc_algorithms 
* spot/mc/mc_instanciator.hh: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
85ff53c45e twacube: fix erroneous translation 
* spot/twacube_algos/convert.cc,
tests/core/twacube.test: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
89675a2762 twacube_algos: add support for are_equivalent 
* spot/twacube_algos/convert.cc,
spot/twacube_algos/convert.hh,
tests/core/twacube.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
92845612a1 sanity: please 80 columns 
* spot/ltsmin/spins_kripke.hh,
spot/twacube/twacube.cc,
spot/twacube_algos/convert.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
227627c739 mc: correct SPOT_API 
* spot/mc/mc.hh: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
070dc4880a modelcheck: more relevant information for --csv 
* tests/ltsmin/check.test,
tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
bdb95dcde9 mc: keep information about the finisher 
* spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/cndfs.hh,
spot/mc/deadlock.hh,
spot/mc/lpar13.hh,
spot/mc/mc.hh,
spot/mc/mc_instanciator.hh: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
cb8eb7e9b2 check: update with new modelcheck options/output 
* tests/ltsmin/check.test: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
ff57f59dba modelcheck: add missing --kripke option 
* tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:41 +02:00