1. 18 May, 2020 9 commits
    • Etienne Renault's avatar
      twacube: use default/deleted · 18a075db
      Etienne Renault authored
      * spot/twacube/cube.cc,
      spot/twacube/cube.hh,
      spot/twacube/twacube.cc,
      spot/twacube/twacube.hh: Here.
      18a075db
    • Etienne Renault's avatar
      twacube: please gcc null-dereference · 3772f53b
      Etienne Renault authored
      * spot/twacube/twacube.hh: here.
      3772f53b
    • Etienne Renault's avatar
      twacube: move useless unsigned int to unsigned · 05b43496
      Etienne Renault authored
      * spot/twacube/twacube.cc,
      spot/twacube/twacube.hh: here.
      05b43496
    • Etienne Renault's avatar
      twacube: more documentation · cce284a4
      Etienne Renault authored
      * spot/twacube/twacube.hh: here.
      cce284a4
    • Etienne Renault's avatar
      swarming: add support everywhere · 3f2c08bf
      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.
      3f2c08bf
    • Etienne Renault's avatar
      Promote use of shared_ptr · a804c2a8
      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.
      a804c2a8
    • Etienne Renault's avatar
      twacube: atomic propositions are now passed by copy · 32e52318
      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.
      32e52318
    • Etienne Renault's avatar
      sanity: replace tabulars by spaces · 64c34989
      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.
      64c34989
    • Etienne Renault's avatar
      convert: twa to twacube translation · 5497f23a
      Etienne Renault authored
      * spot/twacube/Makefile.am, spot/twacube/twacube.cc,
      spot/twacube/twacube.hh, spot/twacube_algos/convert.cc,
      spot/twacube_algos/convert.hh, tests/Makefile.am,
      tests/core/.gitignore, tests/core/twacube.cc,
      tests/core/twacube.test: here.
      5497f23a