- 18 May, 2020 40 commits
-
-
Etienne Renault authored
* spot/mc/bloemen.hh, spot/mc/mc.hh: here.
-
Etienne Renault authored
* spot/mc/bloemen.hh, tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* spot/mc/Makefile.am, spot/mc/bloemen.hh, spot/mc/mc.hh, tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* spot/mc/Makefile.am, spot/mc/deadlock.hh, spot/mc/mc.hh, tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh, spot/mc/Makefile.am, tests/ltsmin/modelcheck.cc, spot/mc/mc.hh: here.
-
Etienne Renault authored
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.
-
Etienne Renault authored
* tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* tests/Makefile.am: here.
-
Etienne Renault authored
* spot/ltsmin/Makefile.am, spot/ltsmin/spins_interface.hh: here. * spot/ltsmin/spins_interface.cc: delete.
-
Etienne Renault authored
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.
-
Etienne Renault authored
* spot/twacube/twacube.hh: here.
-
Etienne Renault authored
* spot/twacube/twacube.cc, spot/twacube/twacube.hh: here.
-
Etienne Renault authored
* spot/twacube/twacube.hh: here.
-
Etienne Renault authored
* spot/mc/ec.hh: here.
-
Etienne Renault authored
* spot/ltsmin/Makefile.am, spot/ltsmin/spins_interface.cc, spot/ltsmin/spins_interface.hh: here.
-
Etienne Renault authored
* bricks/brick-shmem: here.
-
Etienne Renault authored
* bricks/brick-shmem: here.
-
Etienne Renault authored
* bricks/brick-hashset: here.
-
Etienne Renault authored
* spot/ltsmin/spins_kripke.hxx: here
-
Etienne Renault authored
* spot/ltsmin/spins_kripke.hxx: here.
-
Etienne Renault authored
This commit fixes a bug that (randomly) occurs when calling destructor of kripkecube. * spot/ltsmin/spins_kripke.hxx: here.
-
Etienne Renault authored
* bricks/brick-shmem: here.
-
Etienne Renault authored
* bricks/brick-assert: here.
-
Etienne Renault authored
* tests/sanity/includes.test: here.
-
Etienne Renault authored
* spot/ltsmin/Makefile.am, spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh spot/ltsmin/spins_kripke.hh, spot/ltsmin/spins_kripke.hxx: here.
-
Etienne Renault authored
* spot/ltsmin/Makefile.am, spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh, spot/ltsmin/spins_interface.hh: here.
-
Etienne Renault authored
* spot/ltsmin/ltsmin.cc: here.
-
Etienne Renault authored
* bricks/brick-assert: here.
-
Etienne Renault authored
Follows up cf5d2c2b. * spot/mc/ec.hh: here.
-
Etienne Renault authored
From a discussion with Petr Rockai: "the possibly non-intuitive bit that you probably didn't notice is that the hashset is supposed to be passed to each thread by value. The copy semantics of the entire hashset are that of a shared pointer: multiple copies share the same underlying data. Each thread *must* have its own private copy of the hashset object (there are bits of state that each thread needs for bookkeeping and those must not be shared)." * spot/ltsmin/ltsmin.cc: here.
-
Etienne Renault authored
* bricks/brick-hashset: here.
-
Etienne Renault authored
* bricks/brick-bitlevel: here.
-
Etienne Renault authored
* spot/kripke/kripke.hh: here.
-
Etienne Renault authored
* bricks/brick-bitlevel, bricks/brick-hashset, bricks/brick-shmem, bricks/brick-types: here.
-
Etienne Renault authored
* bricks/brick-hash, tests/core/bricks.cc: here.
-
Etienne Renault authored
* Makefile.am, bricks/brick-assert, bricks/brick-assert.h, spot/ltsmin/ltsmin.cc, spot/mc/ec.hh: here. * bricks/brick-bitlevel.h, bricks/brick-hash.h, bricks/brick-hashset.h, bricks/brick-shmem.h, bricks/brick-types.h: Rename as ... * bricks/brick-bitlevel, bricks/brick-hash, bricks/brick-hashset, bricks/brick-shmem, bricks/brick-types: ... these
-
Etienne Renault authored
* spot/mc/reachability.hh: here.
-
Etienne Renault authored
Swarming implies that a single instance of the kripke structure (or product) will be explored by diffrent threads with their own exploration order. Most of the modification aims to have a thread safe kripke structure. * spot/kripke/kripke.hh, spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh, spot/mc/ec.hh, spot/mc/intersect.hh, spot/mc/reachability.hh, spot/misc/hash.hh, spot/twacube/twacube.hh, tests/core/twacube.test, tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* bricks/brick-hash.h, bricks/brick-hashset.h: here.
-
Etienne Renault authored
* spot/mc/ec.hh, spot/mc/intersect.hh, spot/mc/reachability.hh, spot/mc/utils.hh: here.
-