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

956 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
64aee87d76 postproc: option to wdba-minimize only when sure 
Fixes #15.

* spot/twaalgos/minimize.hh, spot/twaalgos/minimize.cc
(minimize_obligation_garanteed_to_work): New function.
* spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use it if
wdba-minimize=1.  Handle new default for wdba-minimize.
* NEWS, bin/spot-x.cc: Document those changes.
* tests/core/ltl2tgba2.test: Add some test cases.
* tests/core/genltl.test: Improve expected results.
 2020-07-13 16:30:29 +02:00
Alexandre Duret-Lutz
d25fcb23eb stats: speed up the computation of transitions 
Juraj Major reported a case with 32 APs where ltlcross would take
forever to gather statistics.  It turns out that for each edge,
twa_sub_statistics was enumerating all compatible assignments of 32
APs.  This uses bdd_satcountset() instead, and also store the result
in a long long to avoid overflows.

* spot/twaalgos/stats.cc (twa_sub_statistics): Improve the code for
counting transitions.
* bin/common_aoutput.hh, bin/ltlcross.cc, spot/twaalgos/stats.hh:
Store transition counts are long long.
* tests/core/readsave.test: Add test case.
* NEWS: Mention the bug.
 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
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
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
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
d3eb269078 modelcheck: fix incorrect return value without --csv 
* tests/ltsmin/modelcheck.cc: Here.
 2020-06-09 16:21:11 +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
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
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
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
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
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
Etienne Renault
17579ad9ad mc: rework and test conversion into twa 
* spot/mc/Makefile.am,
spot/mc/reachability.hh,
spot/mc/utils.hh,
tests/Makefile.am,
tests/ltsmin/.gitignore,
tests/ltsmin/testconvert.cc,
tests/ltsmin/testconvert.test: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
369a8b8b14 mc: merge deadlock and reachabilty algorithms 
* spot/mc/deadlock.hh,
spot/mc/mc.hh,
spot/mc/mc_instanciator.hh,
tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
1736a7364c modelcheck: formula can be nullptr 
* tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
c19163cced cube: rename get_ap into ap 
* spot/kripke/kripke.hh,
spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx,
spot/mc/mc_instanciator.hh,
spot/mc/utils.hh,
spot/twacube/twacube.cc,
spot/twacube/twacube.hh,
spot/twacube_algos/convert.cc,
tests/core/twacube.cc,
tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
ee01fdf209 mc: rename ec_renault13lpar into lpar13 
* spot/mc/ec.hh: Rename to ...
* spot/mc/lpar13.hh: ... this.
* spot/mc/Makefile.am,
spot/mc/mc_instanciator.hh,
tests/ltsmin/modelcheck.cc: Here
 2020-06-03 12:22:41 +02:00
Etienne Renault
5bb29d646b mc: refactor parallel algorithms 
* spot/mc/Makefile.am,
spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/cndfs.hh,
spot/mc/deadlock.hh,
spot/mc/ec.hh,
spot/mc/intersect.hh,
spot/mc/mc.hh,
spot/mc/mc_instanciator.hh,
spot/mc/utils.hh,
tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
f8448fad89 kripkecube: modernize is_a_kripkecube_ptr 
* spot/kripke/kripke.hh,
spot/ltsmin/spins_kripke.hh,
spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/cndfs.hh,
spot/mc/deadlock.hh,
spot/mc/intersect.hh,
spot/mc/reachability.hh,
tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
b52e941b04 ltsmin: prefer '\n' for std::cerr 
* tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:40 +02:00
Antoine Martin
276892229c mc: implement CNDFS 
* spot/mc/Makefile.am: add cndfs.hh
* spot/mc/cndfs.hh, spot/mc/mc.hh: implementation here
* tests/ltsmin/check.test: test CNDFS
* tests/ltsmin/modelcheck.cc: add CNDFS option
 2020-06-03 12:22:40 +02:00
Antoine Martin
298e6f2b47 mc: bloemen emptiness check 
* spot/mc/bloemen_ec.hh,
spot/mc/mc.hh,
tests/ltsmin/check.test,
tests/ltsmin/modelcheck.cc: here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
35f1423e20 prefer -pthread to -lpthread 
* configure.ac,
spot/ltsmin/Makefile.am,
tests/Makefile.am: Here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
2b9471b9a7 please gcc snapshot 
* spot/bricks/brick-assert,
spot/bricks/brick-bitlevel,
spot/bricks/brick-shmem,
spot/bricks/brick-types,
spot/mc/bloemen.hh,
spot/mc/ec.hh,
spot/mc/intersect.hh,
tests/core/bricks.cc: Here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
eb4e3f8be9 modelcheck: fix erroneous report in deadlock 
* tests/ltsmin/modelcheck.cc: Here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
01cceef29a bricks: move into spot directory 
* bricks/brick-assert, bricks/brick-bitlevel,
bricks/brick-hash, bricks/brick-hashset,
bricks/brick-shmem, bricks/brick-types: Rename as .. .
* spot/bricks/brick-assert, spot/bricks/brick-bitlevel,
spot/bricks/brick-hash, spot/bricks/brick-hashset,
spot/bricks/brick-shmem, spot/bricks/brick-types: ... this
* Makefile.am, README, debian/copyright,
debian/libspot-dev.install, m4/bricks.m4,
spot/Makefile.am, spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx, spot/mc/bloemen.hh
spot/mc/deadlock.hh, tests/Makefile.am,
tests/core/bricks.cc: here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
23edf52dd5 fixpool: propose alternative policy 
In 3fe74f1c, fixed_size_pool was changed in order to
help memcheck to detect "potential" memory leaks. In a
multithreaded context, this could raise false alarm. To
solve this, we proprose 2 policies for the pool, one with
the check and one without.

* spot/misc/fixpool.cc: deleted ...
* spot/ltsmin/ltsmin.cc, spot/ltsmin/spins_kripke.hh,
spot/mc/deadlock.hh, spot/misc/Makefile.am,
spot/misc/fixpool.cc, spot/misc/fixpool.hh,
spot/priv/allocator.hh, spot/ta/tgtaproduct.cc,
spot/ta/tgtaproduct.hh, spot/twa/twaproduct.cc,
spot/twa/twaproduct.hh, tests/core/mempool.cc: Here.
 2020-06-03 12:22:26 +02:00
Etienne Renault
fe1be20f09 twacube: fix dot output in tests 
* tests/core/twacube.test: Here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
5062d1c2fa modelcheck: conversions now report about the options 
* tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
5d30286dd6 twacube: 'mark_t' is deprecated 
* spot/mc/ec.hh, spot/mc/intersect.hh,
tests/core/twacube.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
9827b1d096 modelcheck: capture exceptions by const reference 
* tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
88dc500aa7 tests: fix call to print_dot according to default arguments 
* tests/core/twacube.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
a9178fbe64 modelcheck: update output and documentation 
Fixes #330.

* tests/ltsmin/README,
tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
011115cb1d tests: include missing config.h 
* spot/mc/unionfind.cc,
spot/twacube/cube.cc,
spot/twacube/twacube.cc,
spot/twacube_algos/convert.cc,
tests/core/bricks.cc,
tests/core/cube.cc,
tests/core/twacube.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
34b9e89f5d tests: please modelcheck interface 
* tests/ltsmin/finite3.test: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
f397def03e tests: add tests for parallel algorithms 
* tests/ltsmin/check.test: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
63a4b4085a mc: bloemen count unique states 
* spot/mc/bloemen.hh, tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00