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

5701 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
eb4e3f8be9 modelcheck: fix erroneous report in deadlock 
* tests/ltsmin/modelcheck.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
Etienne Renault
b9ac017382 spins_kripke: rewrite, clean and document 
Some parts of the kripke were confusing, lacked
of documentation or could be factorized. This patch
cleans all of this.

* spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx: here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
7aa2d292cf ltsmin: remove useless code 
* spot/ltsmin/spins_kripke.hh: here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
d1200cb579 swarming: bug fix 
This is an important bug fix. When swarming
is activated, some multiplication is performed
to find a successor. This multiplication could,
eventually, overflow... Using larger types solves
the problem.

* spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx: here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
69457e957b misc: add clz wrapper for builtin 
* spot/bricks/brick-bitlevel, spot/misc/Makefile.am,
spot/misc/bitset.hh, spot/misc/clz.cc,
spot/misc/clz.hh, spot/misc/fixpool.hh: 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
b115d2f9b1 fixpool: remove useless clz encapsulation 
* spot/misc/fixpool.hh: Here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
4871635159 bloemen: fix memory leaks 
* spot/mc/bloemen.hh, spot/mc/mc.hh: here.
 2020-06-03 12:22:40 +02:00
Etienne Renault
2dd2d44907 deadlock: fix memory leak 
Do not forget to recycle iterator, otherwise the todo
stack will be trashed without cleaning iterators.

* spot/mc/deadlock.hh: 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
73ccf2216d bloemen: avoid tail-recursive calls 
* spot/mc/bloemen.hh: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
ae101a509f bloemen: PPOPP'16 is buggy 
In PPOPP'16, the algorithm does not unlock
roots. This could lead to deadlock between
threads.

* spot/mc/bloemen.hh: 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
2bd08d956a mc: please Werror=noexcept 
* spot/mc/intersect.hh: 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
fe694e2ba2 debian: fix corrupted profile info 
* debian/rules: 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
f777e96890 mc: recycle iterators in bloemen 
* spot/mc/bloemen.hh: 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
Etienne Renault
80746e4332 modelcheck: update tests 
* tests/ltsmin/check.test,
tests/ltsmin/check2.test,
tests/ltsmin/check3.test,
tests/ltsmin/finite2.test,
tests/ltsmin/finite3.test: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
0b917af762 mc: please sanity.test 
* spot/mc/bloemen.hh, spot/mc/mc.hh: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
e6e3b568ca mc: parallel version of bloemen 
* spot/mc/bloemen.hh,
tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
01093f992e mc: sequential version of Bloemen 
* spot/mc/Makefile.am, spot/mc/bloemen.hh,
spot/mc/mc.hh, tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
15e72e90cc mc: add swarmed deadlock-detection 
* spot/mc/Makefile.am, spot/mc/deadlock.hh,
spot/mc/mc.hh, tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
f486dab241 ltsmin: move modelchek in mc directory 
* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh,
spot/mc/Makefile.am, tests/ltsmin/modelcheck.cc,
spot/mc/mc.hh: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
1d4cb26235 ltsmin: remove shared table at model level 
Experiments shows  that this table slows down algorithms
since the management is also tracked at higher lever by
algorithms

* spot/ltsmin/spins_kripke.hh,
spot/ltsmin/spins_kripke.hxx: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
d2549334f9 modelcheck: please gcc catch-value errors 
* tests/ltsmin/modelcheck.cc: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
a147fd65dc tests: add pthread library 
* tests/Makefile.am: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
f9b0044623 ltsmin: please private.test 
* spot/ltsmin/Makefile.am, spot/ltsmin/spins_interface.hh: here.
* spot/ltsmin/spins_interface.cc: delete.
 2020-06-03 10:33:54 +02:00
Etienne Renault
32b79818dc kripke: avoir internal compiler error 
gcc snapshot yield internal compiler error: tree check: accessed elt 2
of tree_vec with 1 elts in tsubst, at cp/pt.c:13693

* spot/kripke/kripke.hh: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
7bac705e83 twacube: please gcc null-dereference 
* spot/twacube/twacube.hh: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
b8258ac638 twacube: move useless unsigned int to unsigned 
* spot/twacube/twacube.cc,
spot/twacube/twacube.hh: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
cb343ff02d twacube: more documentation 
* spot/twacube/twacube.hh: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
fbf9d98e15 Fix typo 
* spot/mc/ec.hh: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
d95428d245 ltsmin: remove ltdl from public headers 
* spot/ltsmin/Makefile.am,
spot/ltsmin/spins_interface.cc,
spot/ltsmin/spins_interface.hh: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
d3b143574b bricks: please gcc error=noexcept option 
* bricks/brick-shmem: here.
 2020-06-03 10:33:54 +02:00
Etienne Renault
1fc3d7f935 bricks: gcc-7 doesn't align variables up to a maximum of 16 bytes 
* bricks/brick-shmem: here.
 2020-06-03 10:33:54 +02:00