1. 14 May, 2020 9 commits
  2. 13 May, 2020 6 commits
    • Etienne Renault's avatar
      modelcheck: formula can be nullptr · 42f9f6b6
      Etienne Renault authored
      * tests/ltsmin/modelcheck.cc: Here.
      42f9f6b6
    • Etienne Renault's avatar
      cube: rename get_ap into ap · 48f690eb
      Etienne Renault authored
      * spot/kripke/kripke.hh,
      spot/ltsmin/spins_kripke.hh,
      spot/ltsmin/spins_kripke.hxx,
      spot/mc/mc_instanciator.hh,
      spot/mc/utils.hh,
      spot/twacube/twacube.cc,
      spot/twacube/twacube.hh,
      spot/twacube_algos/convert.cc,
      tests/core/twacube.cc,
      tests/ltsmin/modelcheck.cc: Here.
      48f690eb
    • Etienne Renault's avatar
      mc: clarify method name · 56d92b2e
      Etienne Renault authored
      * spot/mc/bloemen.hh,
      spot/mc/bloemen_ec.hh,
      spot/mc/cndfs.hh,
      spot/mc/deadlock.hh,
      spot/mc/lpar13.hh,
      spot/mc/mc_instanciator.hh: Here.
      56d92b2e
    • Etienne Renault's avatar
      mc: rename ec_renault13lpar into lpar13 · 45bec09d
      Etienne Renault authored
      * spot/mc/ec.hh: Rename to ...
      * spot/mc/lpar13.hh: ... this.
      * spot/mc/Makefile.am,
      spot/mc/mc_instanciator.hh,
      tests/ltsmin/modelcheck.cc: Here
      45bec09d
    • Etienne Renault's avatar
      kripke: please style.test · 58a8af3f
      Etienne Renault authored
      * spot/kripke/kripke.hh: Here.
      58a8af3f
    • Etienne Renault's avatar
      mc: refactor parallel algorithms · da6949ab
      Etienne Renault authored
      * spot/mc/Makefile.am,
      spot/mc/bloemen.hh,
      spot/mc/bloemen_ec.hh,
      spot/mc/cndfs.hh,
      spot/mc/deadlock.hh,
      spot/mc/ec.hh,
      spot/mc/intersect.hh,
      spot/mc/mc.hh,
      spot/mc/mc_instanciator.hh,
      spot/mc/utils.hh,
      tests/ltsmin/modelcheck.cc: Here.
      da6949ab
  3. 12 May, 2020 1 commit
  4. 07 Nov, 2019 1 commit
  5. 06 Nov, 2019 2 commits
  6. 21 Oct, 2019 2 commits
  7. 18 Oct, 2019 19 commits
    • Antoine Martin's avatar
      mc: bloemen emptiness check · f8b4c1f2
      Antoine Martin authored
      * spot/mc/bloemen_ec.hh,
      spot/mc/mc.hh,
      tests/ltsmin/check.test,
      tests/ltsmin/modelcheck.cc: here.
      f8b4c1f2
    • Etienne Renault's avatar
      ltsmin: rework spins_interface · 870ed9ed
      Etienne Renault authored
      * spot/ltsmin/ltsmin.cc,
      spot/ltsmin/spins_interface.cc,
      spot/ltsmin/spins_interface.hh: here.
      870ed9ed
    • Etienne Renault's avatar
      ltdl: should not appear in public headers · 8c8068fd
      Etienne Renault authored
      * spot/ltsmin/Makefile.am,
      spot/ltsmin/spins_interface.hh,
      spot/ltsmin/spins_interface.cc: here.
      8c8068fd
    • Etienne Renault's avatar
      prefer -pthread to -lpthread · 8cfa6dac
      Etienne Renault authored
      * configure.ac,
      spot/ltsmin/Makefile.am,
      tests/Makefile.am: Here.
      8cfa6dac
    • Etienne Renault's avatar
      please gcc snapshot · be00cada
      Etienne Renault authored
      * spot/bricks/brick-assert,
      spot/bricks/brick-bitlevel,
      spot/bricks/brick-shmem,
      spot/bricks/brick-types,
      spot/mc/bloemen.hh,
      spot/mc/ec.hh,
      spot/mc/intersect.hh,
      tests/core/bricks.cc: Here.
      be00cada
    • Etienne Renault's avatar
      modelcheck: fix erroneous report in deadlock · 2fe6f5cc
      Etienne Renault authored
      * tests/ltsmin/modelcheck.cc: Here.
      2fe6f5cc
    • Etienne Renault's avatar
      mc: fix deadlock according to new bricks · 26d122d9
      Etienne Renault authored
      * spot/mc/deadlock.hh: Here.
      26d122d9
    • Etienne Renault's avatar
      bricks: update excluding C++17 features · ba9a4df1
      Etienne Renault authored
      * spot/bricks/brick-assert,
      spot/bricks/brick-bitlevel,
      spot/bricks/brick-hashset,
      spot/bricks/brick-shmem: Here.
      ba9a4df1
    • Etienne Renault's avatar
      twacube: use default/deleted · 33887fae
      Etienne Renault authored
      * spot/twacube/cube.cc,
      spot/twacube/cube.hh,
      spot/twacube/twacube.cc,
      spot/twacube/twacube.hh: Here.
      33887fae
    • Etienne Renault's avatar
      spins_kripke: rewrite, clean and document · 7e1a6802
      Etienne Renault authored
      Some parts of the kripke were confusing, lacked
      of documentation or could be factorized. This patch
      cleans all of this.
      
      * spot/ltsmin/spins_kripke.hh,
      spot/ltsmin/spins_kripke.hxx: here.
      7e1a6802
    • Etienne Renault's avatar
      ltsmin: remove useless code · 8d5b2ec3
      Etienne Renault authored
      * spot/ltsmin/spins_kripke.hh: here.
      8d5b2ec3
    • Etienne Renault's avatar
      swarming: bug fix · b156f441
      Etienne Renault authored
      This is an important bug fix. When swarming
      is activated, some multiplication is performed
      to find a successor. This multiplication could,
      eventually, overflow... Using larger types solves
      the problem.
      
      * spot/ltsmin/spins_kripke.hh,
      spot/ltsmin/spins_kripke.hxx: here.
      b156f441
    • Etienne Renault's avatar
      misc: add clz wrapper for builtin · c684d586
      Etienne Renault authored
      * spot/bricks/brick-bitlevel, spot/misc/Makefile.am,
      spot/misc/bitset.hh, spot/misc/clz.cc,
      spot/misc/clz.hh, spot/misc/fixpool.hh: here.
      c684d586
    • Etienne Renault's avatar
      bricks: move into spot directory · 9c01cc6c
      Etienne Renault authored
      * bricks/brick-assert, bricks/brick-bitlevel,
      bricks/brick-hash, bricks/brick-hashset,
      bricks/brick-shmem, bricks/brick-types: Rename as .. .
      * spot/bricks/brick-assert, spot/bricks/brick-bitlevel,
      spot/bricks/brick-hash, spot/bricks/brick-hashset,
      spot/bricks/brick-shmem, spot/bricks/brick-types: ... this
      * Makefile.am, README, debian/copyright,
      debian/libspot-dev.install, m4/bricks.m4,
      spot/Makefile.am, spot/ltsmin/spins_kripke.hh,
      spot/ltsmin/spins_kripke.hxx, spot/mc/bloemen.hh
      spot/mc/deadlock.hh, tests/Makefile.am,
      tests/core/bricks.cc: here.
      9c01cc6c
    • Etienne Renault's avatar
      fixpool: remove useless clz encapsulation · 5f5b9715
      Etienne Renault authored
      * spot/misc/fixpool.hh: Here.
      5f5b9715
    • Etienne Renault's avatar
      bloemen: fix memory leaks · c4fe8e16
      Etienne Renault authored
      * spot/mc/bloemen.hh, spot/mc/mc.hh: here.
      c4fe8e16
    • Etienne Renault's avatar
      deadlock: fix memory leak · aac48366
      Etienne Renault authored
      Do not forget to recycle iterator, otherwise the todo
      stack will be trashed without cleaning iterators.
      
      * spot/mc/deadlock.hh: Here.
      aac48366
    • Etienne Renault's avatar
      fixpool: propose alternative policy · d998f613
      Etienne Renault authored
      In 3fe74f1c, fixed_size_pool was changed in order to
      help memcheck to detect "potential" memory leaks. In a
      multithreaded context, this could raise false alarm. To
      solve this, we proprose 2 policies for the pool, one with
      the check and one without.
      
      * spot/misc/fixpool.cc: deleted ...
      * spot/ltsmin/ltsmin.cc, spot/ltsmin/spins_kripke.hh,
      spot/mc/deadlock.hh, spot/misc/Makefile.am,
      spot/misc/fixpool.cc, spot/misc/fixpool.hh,
      spot/priv/allocator.hh, spot/ta/tgtaproduct.cc,
      spot/ta/tgtaproduct.hh, spot/twa/twaproduct.cc,
      spot/twa/twaproduct.hh, tests/core/mempool.cc: Here.
      d998f613
    • Etienne Renault's avatar
      twacube: fix dot output in tests · 45de5258
      Etienne Renault authored
      * tests/core/twacube.test: Here.
      45de5258