Commit graph

10 commits

Author SHA1 Message Date
Etienne Renault
9208726d97 reachability: improve support for callbacks
* spot/mc/reachability.hh: here.
2020-06-03 10:33:53 +02:00
Etienne Renault
72948661e9 swarming: add support everywhere
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.
2020-06-03 10:33:53 +02:00
Etienne Renault
fb4ef40d11 Use SPOT_ASSERT() instead of assert() in public headers
* spot/mc/ec.hh, spot/mc/intersect.hh,
spot/mc/reachability.hh, spot/mc/utils.hh: here.
2020-06-03 10:33:53 +02:00
Etienne Renault
765bb8a7c4 Promote use of shared_ptr
* 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.
2020-06-03 10:33:53 +02:00
Etienne Renault
94f7c58f44 intersect: statistic provided using an object
* spot/mc/ec.hh, spot/mc/intersect.hh: here.
2020-06-03 10:33:53 +02:00
Etienne Renault
f04074bd6d sanity: replace tabulars by spaces
* 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.
2020-06-03 10:33:53 +02:00
Etienne Renault
8e593611f6 convert: kripke and product towards twa
* spot/mc/Makefile.am, spot/mc/utils.hh: here.
2020-06-03 10:33:53 +02:00
Etienne Renault
3bafe693ef ec: Renault et al LPAR'13 emptiness check
In order to reuse the computation of the
intersection between kripke and twa efficiently,
we use template inheritance through the
"mixin templates" technique.

* spot/Makefile.am, spot/mc/Makefile.am,
spot/mc/ec.hh, spot/mc/unionfind.cc,
spot/mc/unionfind.hh: here.
2020-06-03 10:33:53 +02:00
Etienne Renault
87de88c80c intersection: for kripke and twacube
* spot/mc/Makefile.am, spot/mc/intersect.hh: here.
2020-06-03 10:33:53 +02:00
Etienne Renault
94492ffa14 reachability: sequential reachability for kripkecube
* README, configure.ac, spot/mc/Makefile.am,
spot/mc/reachability.hh: here.
2020-06-03 10:33:53 +02:00