1. 18 May, 2020 9 commits
    • Etienne Renault's avatar
      cube: rename get_ap into ap · bcb55017
      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.
      bcb55017
    • Etienne Renault's avatar
      kripkecube: modernize is_a_kripkecube_ptr · 84fef0ed
      Etienne Renault authored
      * spot/kripke/kripke.hh,
      spot/ltsmin/spins_kripke.hh,
      spot/mc/bloemen.hh,
      spot/mc/bloemen_ec.hh,
      spot/mc/cndfs.hh,
      spot/mc/deadlock.hh,
      spot/mc/intersect.hh,
      spot/mc/reachability.hh,
      tests/ltsmin/modelcheck.cc: Here.
      84fef0ed
    • Etienne Renault's avatar
      spins_kripke: rewrite, clean and document · 273cce37
      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.
      273cce37
    • Etienne Renault's avatar
      ltsmin: remove useless code · a947de25
      Etienne Renault authored
      * spot/ltsmin/spins_kripke.hh: here.
      a947de25
    • Etienne Renault's avatar
      swarming: bug fix · 384e5756
      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.
      384e5756
    • Etienne Renault's avatar
      bricks: move into spot directory · 8d35bf89
      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.
      8d35bf89
    • Etienne Renault's avatar
      fixpool: propose alternative policy · c06b35b9
      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.
      c06b35b9
    • Etienne Renault's avatar
      ltsmin: remove shared table at model level · 694b8399
      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.
      694b8399
    • Etienne Renault's avatar
      ltsmin: extract kripkecube to ease manipulation · d933f939
      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.
      d933f939