- 18 May, 2020 40 commits
-
-
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.
-
Etienne Renault authored
* bricks/brick-assert.h, bricks/brick-hashset.h, bricks/brick-shmem.h: here.
-
Etienne Renault authored
* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh, tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* spot/misc/timer.hh: here.
-
Etienne Renault authored
* spot/kripke/kripke.hh, spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh, spot/mc/ec.hh, spot/mc/intersect.hh, spot/mc/utils.hh, spot/twacube/Makefile.am, spot/twacube/fwd.hh, spot/twacube/twacube.hh, spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh, tests/core/twacube.cc, tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
According to swig3.0. the 'using' keyword in type aliasing is not fully supported yet. * spot/ltsmin/ltsmin.hh: here.
-
Etienne Renault authored
* spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh, tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* spot/mc/ec.hh, spot/mc/intersect.hh: here.
-
Etienne Renault authored
* spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh, tests/core/twacube.cc: here.
-
Etienne Renault authored
Passing atomic propositions by reference allows to save very little memory so it doesn't worth complexifying memory management. * spot/twacube/twacube.cc, spot/twacube/twacube.hh: here.
-
Etienne Renault authored
From the working draft: "The macro ATOMIC_FLAG_INIT shall be defined in such a way that it can be used to initialize an object of type atomic_flag to the clear state. The macro can be used in the form: atomic_flag guard = ATOMIC_FLAG_INIT; It is unspecified whether the macro can be used in other initialization contexts." * bricks/brick-shmem.h: here.
-
Etienne Renault authored
* spot/ltsmin/ltsmin.cc, spot/mc/ec.hh, spot/mc/intersect.hh, spot/mc/reachability.hh, spot/mc/unionfind.cc, spot/mc/utils.hh, spot/twacube/cube.cc, spot/twacube/twacube.cc, spot/twacube/twacube.hh, spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh, tests/core/bricks.cc, tests/core/cube.cc, tests/core/twacube.cc, tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* spot/ltsmin/ltsmin.cc: here.
-