* spot/kripke/kripke.hh: Here.

* 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.

* spot/twacube_algos/convert.cc: Here.

* spot/mc/Makefile.am: here.

Antoine Martin authored Apr 18, 2020 and Etienne Renault committed May 18, 2020

* spot/twacube/twacube.hh,spot/twacube/twacube.cc: Here.

Antoine Martin authored Mar 22, 2020 and Etienne Renault committed May 18, 2020

* spot/twacube/twacube.hh: Here.

Antoine Martin authored Feb 19, 2020 and Etienne Renault committed May 18, 2020

* spot/twacube/twacube.hh: Here.

Antoine Martin authored Mar 10, 2020 and Etienne Renault committed May 18, 2020

* spot/twacube/twacube.hh,spot/twacube/twacube.cc: Here.

* 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.

* tests/ltsmin/modelcheck.cc: Here.

This bug is similar to the one described in  commit
d956fdc3.

* spot/twacube/twacube.hh: Here.

Antoine Martin authored Jul 09, 2018 and Etienne Renault committed May 18, 2020

* 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

Antoine Martin authored Aug 08, 2018 and Etienne Renault committed May 18, 2020

* spot/mc/bloemen_ec.hh,
spot/mc/mc.hh,
tests/ltsmin/check.test,
tests/ltsmin/modelcheck.cc: here.

* spot/ltsmin/ltsmin.cc,
spot/ltsmin/spins_interface.cc,
spot/ltsmin/spins_interface.hh: here.

* spot/ltsmin/Makefile.am,
spot/ltsmin/spins_interface.hh,
spot/ltsmin/spins_interface.cc: here.

* configure.ac,
spot/ltsmin/Makefile.am,
tests/Makefile.am: Here.

* 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.

* tests/ltsmin/modelcheck.cc: Here.

* spot/mc/deadlock.hh: Here.

* spot/bricks/brick-assert,
spot/bricks/brick-bitlevel,
spot/bricks/brick-hashset,
spot/bricks/brick-shmem: Here.

* spot/twacube/cube.cc,
spot/twacube/cube.hh,
spot/twacube/twacube.cc,
spot/twacube/twacube.hh: Here.

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.

* spot/ltsmin/spins_kripke.hh: here.

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.

* 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.

* 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.

* spot/misc/fixpool.hh: Here.

* spot/mc/bloemen.hh, spot/mc/mc.hh: here.

Do not forget to recycle iterator, otherwise the todo
stack will be trashed without cleaning iterators.

* spot/mc/deadlock.hh: Here.

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.

* tests/core/twacube.test: Here.

* tests/ltsmin/modelcheck.cc: here.

* spot/mc/ec.hh, spot/mc/intersect.hh,
tests/core/twacube.cc: here.

* spot/mc/bloemen.hh: here.

In PPOPP'16, the algorithm does not unlock
roots. This could lead to deadlock between
threads.

* spot/mc/bloemen.hh: here.

* tests/ltsmin/modelcheck.cc: here.

* tests/core/twacube.cc: here.

Fixes #330.

* tests/ltsmin/README,
tests/ltsmin/modelcheck.cc: here.

* spot/mc/intersect.hh: here.

* 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.