1. 27 Mar, 2018 8 commits
    • Etienne Renault's avatar
      mark_t::operator bool() is now explicit · 27682c00
      Etienne Renault authored
      Follows up cf5d2c2b.
      
      * spot/mc/ec.hh: here.
      27682c00
    • Etienne Renault's avatar
      bricks: update and move to c++14 · e8cba2df
      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
      e8cba2df
    • Etienne Renault's avatar
      swarming: add support everywhere · c257d5bc
      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.
      c257d5bc
    • Etienne Renault's avatar
      Use SPOT_ASSERT() instead of assert() in public headers · 7f996d1b
      Etienne Renault authored
      * spot/mc/ec.hh, spot/mc/intersect.hh,
      spot/mc/reachability.hh, spot/mc/utils.hh: here.
      7f996d1b
    • Etienne Renault's avatar
      Promote use of shared_ptr · bfd6d57a
      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.
      bfd6d57a
    • Etienne Renault's avatar
      intersect: statistic provided using an object · 2db69268
      Etienne Renault authored
      * spot/mc/ec.hh, spot/mc/intersect.hh: here.
      2db69268
    • Etienne Renault's avatar
      sanity: replace tabulars by spaces · 08509a2c
      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.
      08509a2c
    • Etienne Renault's avatar
      ec: Renault et al LPAR'13 emptiness check · d3d833bd
      Etienne Renault authored
      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.
      d3d833bd