- 18 May, 2020 40 commits
-
-
Etienne Renault authored
* spot/mc/ec.hh, spot/mc/intersect.hh, tests/core/twacube.cc: here.
-
Etienne Renault authored
* spot/mc/bloemen.hh: here.
-
Etienne Renault authored
In PPOPP'16, the algorithm does not unlock roots. This could lead to deadlock between threads. * spot/mc/bloemen.hh: here.
-
Etienne Renault authored
* tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* tests/core/twacube.cc: here.
-
Etienne Renault authored
Fixes #330. * tests/ltsmin/README, tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* spot/mc/intersect.hh: here.
-
Etienne Renault authored
* 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.
-
Etienne Renault authored
* debian/rules: here.
-
Etienne Renault authored
* tests/ltsmin/finite3.test: here.
-
Etienne Renault authored
* spot/mc/bloemen.hh: here.
-
Etienne Renault authored
* tests/ltsmin/check.test: here.
-
Etienne Renault authored
* spot/mc/bloemen.hh, tests/ltsmin/modelcheck.cc: here.
-
Etienne Renault authored
* tests/ltsmin/check.test, tests/ltsmin/check2.test, tests/ltsmin/check3.test, tests/ltsmin/finite2.test, tests/ltsmin/finite3.test: here.
-
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.
-