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

954 commits

Author SHA1 Message Date
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
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
2098d41c05 bricks: details version and modifications 
* README, spot/bricks/README: Here.
 2020-06-10 09:02: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
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
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
Etienne Renault
1a8920d9b6 rpm: fixes commit 3acf2ca6 
* spot.spec.in, spot/Makefile.am: Here.
 2020-06-08 08:15:52 +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
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
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
a3df930a60 mc: please include.test 
* spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/deadlock.hh,
spot/mc/lpar13.hh,
spot/mc/mc.hh: 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
568fcdfc9a mc: rework product_to_twa 
* spot/mc/utils.hh: 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
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
2d59a5c752 mc: clarify method name 
* spot/mc/bloemen.hh,
spot/mc/bloemen_ec.hh,
spot/mc/cndfs.hh,
spot/mc/deadlock.hh,
spot/mc/lpar13.hh,
spot/mc/mc_instanciator.hh: 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
b32e451292 kripke: please style.test 
* spot/kripke/kripke.hh: 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
907a3cfbbf twacube: check nullptr during conversion 
* spot/twacube_algos/convert.cc: Here.
 2020-06-03 12:22:41 +02:00
Etienne Renault
53ea1131e6 Fixup: missing dependency bloemen 
* spot/mc/Makefile.am: here.
 2020-06-03 12:22:41 +02:00
Antoine Martin
fcf6bb3d3d twacube: mark get_initial method as const 
* spot/twacube/twacube.hh,spot/twacube/twacube.cc: Here.
 2020-06-03 12:22:40 +02:00
Antoine Martin
0ad380ef12 twacube: mark succ() as const 
* spot/twacube/twacube.hh: Here.
 2020-06-03 12:22:40 +02:00
Antoine Martin
a14f63dd25 twacube: add num_states and num_edges 
* spot/twacube/twacube.hh: Here.
 2020-06-03 12:22:40 +02:00
Antoine Martin
49a3cf1148 twacube: mark get_ap method as const 
* spot/twacube/twacube.hh,spot/twacube/twacube.cc: Here.
 2020-06-03 12:22:40 +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
87afcd2f87 twacube: fix bug in swarming for large formulae 
This bug is similar to the one described in  commit
d956fdc385b4dd9a5c5b3a63a0de80a09eb8e40d.

* spot/twacube/twacube.hh: 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
949881935a ltsmin: rework spins_interface 
* spot/ltsmin/ltsmin.cc,
spot/ltsmin/spins_interface.cc,
spot/ltsmin/spins_interface.hh: here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
7a8a4f4d77 ltdl: should not appear in public headers 
* spot/ltsmin/Makefile.am,
spot/ltsmin/spins_interface.hh,
spot/ltsmin/spins_interface.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
ec5e42a8ef mc: fix deadlock according to new bricks 
* spot/mc/deadlock.hh: Here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
fd28cb5e49 bricks: update excluding C++17 features 
* spot/bricks/brick-assert,
spot/bricks/brick-bitlevel,
spot/bricks/brick-hashset,
spot/bricks/brick-shmem: Here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
9f372d78de twacube: use default/deleted 
* spot/twacube/cube.cc,
spot/twacube/cube.hh,
spot/twacube/twacube.cc,
spot/twacube/twacube.hh: Here.
 2020-06-03 12:22:40 +02:00