1. 27 Mar, 2018 16 commits
    • Etienne Renault's avatar
      bricks: ATOMIC_FLAG_INIT initialization · c658d540
      Etienne Renault authored
      From the working draft: "The macro ATOMIC_FLAG_INIT shall be defined
      in such a way that it can be used to initialize an object of type
      atomic_flag to the clear state. The macro can be used in the form:
      atomic_flag guard = ATOMIC_FLAG_INIT; It is unspecified whether the
      macro can be used in other initialization contexts."
      
      * bricks/brick-shmem.h: here.
      c658d540
    • 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
      ltsmin: use FastConcurrent map · 71da5b75
      Etienne Renault authored
      * spot/ltsmin/ltsmin.cc: here.
      71da5b75
    • Etienne Renault's avatar
      bricks: fix clang warnings · 0ba44759
      Etienne Renault authored
      * bricks/brick-hash.h, bricks/brick-shmem.h: here.
      0ba44759
    • Etienne Renault's avatar
      bricks: add bricks for concurrent hashmap · cef5120a
      Etienne Renault authored
      * Makefile.am, README, bricks/brick-assert.h,
      bricks/brick-bitlevel.h, bricks/brick-hash.h,
      bricks/brick-hashset.h, bricks/brick-shmem.h,
      bricks/brick-types.h, configure.ac,
      debian/copyright, debian/libspot-dev.install,
      m4/bricks.m4, tests/Makefile.am,
      tests/core/.gitignore, tests/core/bricks.cc: here.
      cef5120a
    • Etienne Renault's avatar
      modelcheck: rewrite and use argp · d7e0366d
      Etienne Renault authored
      * tests/Makefile.am, tests/ltsmin/check.test,
      tests/ltsmin/finite.test, tests/ltsmin/finite2.test,
      tests/ltsmin/kripke.test, tests/ltsmin/modelcheck.cc: here.
      d7e0366d
    • Etienne Renault's avatar
      ltsmin: prodcuce kripkecube · 6a4d2237
      Etienne Renault authored
      Warning! this patch introduces redundancy (or difference)
      between wether you ask for a kripkecube or a kripke.
      
      * spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh: here.
      6a4d2237
    • Etienne Renault's avatar
      convert: kripke and product towards twa · 709a79b5
      Etienne Renault authored
      * spot/mc/Makefile.am, spot/mc/utils.hh: here.
      709a79b5
    • 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
    • Etienne Renault's avatar
      intersection: for kripke and twacube · 1403bbb5
      Etienne Renault authored
      * spot/mc/Makefile.am, spot/mc/intersect.hh: here.
      1403bbb5
    • Etienne Renault's avatar
      reachability: sequential reachability for kripkecube · 8a09388d
      Etienne Renault authored
      * README, configure.ac, spot/mc/Makefile.am,
      spot/mc/reachability.hh: here.
      8a09388d
    • Etienne Renault's avatar
      kripke: define kripkecube structure · 6c642df0
      Etienne Renault authored
      * spot/kripke/kripke.hh: here.
      6c642df0
    • Etienne Renault's avatar
      convert: twacube to twa translation · 09c155f8
      Etienne Renault authored
      * spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
      tests/core/twacube.cc, tests/core/twacube.test: here.
      09c155f8
    • Etienne Renault's avatar
      convert: twa to twacube translation · 93acf313
      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.
      93acf313
    • Etienne Renault's avatar
      convert: BDD to cube conversions · ed6e414d
      Etienne Renault authored
      * README, configure.ac, spot/Makefile.am,
      spot/twacube_algos/Makefile.am, spot/twacube_algos/convert.cc
      spot/twacube_algos/convert.hh, tests/core/cube.cc,
      tests/core/cube.test: here.
      ed6e414d
    • Etienne Renault's avatar
      Introduce cube data structure · ea4a4b1e
      Etienne Renault authored
      * README, configure.ac, spot/Makefile.am,
      spot/twacube/Makefile.am, spot/twacube/cube.cc,
      spot/twacube/cube.hh, tests/Makefile.am,
      tests/core/.gitignore, tests/core/cube.cc,
      tests/core/cube.test: here.
      ea4a4b1e
  2. 25 Mar, 2018 3 commits
  3. 24 Mar, 2018 2 commits
  4. 23 Mar, 2018 2 commits
  5. 21 Mar, 2018 1 commit
  6. 19 Mar, 2018 3 commits
  7. 18 Mar, 2018 4 commits
  8. 16 Mar, 2018 4 commits
  9. 15 Mar, 2018 2 commits
    • Maximilien Colange's avatar
      Clean the usage of spot::acc_cond::mark_t · b09c293f
      Maximilien Colange authored
      spot::acc_cond::mark_t is implemented as a bit vector using a single
      unsigned, and implicit conversions between mark_t and unsigned may be
      confusing. We try to use the proper interface.
      
      * bin/autfilt.cc, bin/ltlsynt.cc, spot/kripke/kripke.cc,
        spot/misc/game.hh, spot/parseaut/parseaut.yy, spot/priv/accmap.hh,
        spot/ta/ta.cc, spot/ta/taexplicit.cc, spot/ta/taproduct.cc,
        spot/taalgos/emptinessta.cc, spot/taalgos/tgba2ta.cc, spot/twa/acc.cc,
        spot/twa/acc.hh, spot/twa/taatgba.cc, spot/twa/taatgba.hh,
        spot/twa/twagraph.hh, spot/twaalgos/alternation.cc,
        spot/twaalgos/cleanacc.cc, spot/twaalgos/cobuchi.cc,
        spot/twaalgos/complete.cc, spot/twaalgos/couvreurnew.cc,
        spot/twaalgos/degen.cc, spot/twaalgos/dot.cc,
        spot/twaalgos/dtwasat.cc, spot/twaalgos/dualize.cc,
        spot/twaalgos/emptiness.cc, spot/twaalgos/gtec/ce.cc,
        spot/twaalgos/gtec/gtec.cc, spot/twaalgos/gtec/sccstack.cc,
        spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc, spot/twaalgos/lbtt.cc,
        spot/twaalgos/ltl2tgba_fm.cc, spot/twaalgos/magic.cc,
        spot/twaalgos/ndfs_result.hxx, spot/twaalgos/rabin2parity.cc,
        spot/twaalgos/randomgraph.cc, spot/twaalgos/remfin.cc,
        spot/twaalgos/sbacc.cc, spot/twaalgos/sccfilter.cc,
        spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh,
        spot/twaalgos/se05.cc, spot/twaalgos/sepsets.cc,
        spot/twaalgos/simulation.cc, spot/twaalgos/strength.cc,
        spot/twaalgos/stripacc.cc, spot/twaalgos/stutter.cc,
        spot/twaalgos/sum.cc, spot/twaalgos/tau03.cc,
        spot/twaalgos/tau03opt.cc, spot/twaalgos/totgba.cc,
        spot/twaalgos/toweak.cc, python/spot/impl.i, tests/core/acc.cc,
        tests/core/twagraph.cc: do not confuse mark_t and unsigned
      * tests/python/acc_cond.ipynb: warn about possible change of the API
      b09c293f
    • Alexandre Duret-Lutz's avatar
      simplify: reduce {r;1} to {r} or {1} · cfcc18e6
      Alexandre Duret-Lutz authored
      Fixes #3.
      
      * spot/tl/simplify.cc: Implement this new rule.
      * doc/tl/tl.tex, NEWS: Document it.
      * tests/core/reduccmp.test: Test it.
      cfcc18e6
  10. 14 Mar, 2018 3 commits