1. 07 Mar, 2018 18 commits
    • Etienne Renault's avatar
      convert: simplify interfaces · 5b9c35d0
      Etienne Renault authored
      * spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
      tests/core/twacube.cc: here.
      5b9c35d0
    • Etienne Renault's avatar
      twacube: atomic propositions are now passed by copy · dc925288
      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.
      dc925288
    • Etienne Renault's avatar
      bricks: ATOMIC_FLAG_INIT initialization · 978c19f1
      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.
      978c19f1
    • Etienne Renault's avatar
      sanity: replace tabulars by spaces · 07483cd4
      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.
      07483cd4
    • Etienne Renault's avatar
      ltsmin: use FastConcurrent map · 02488217
      Etienne Renault authored
      * spot/ltsmin/ltsmin.cc: here.
      02488217
    • Etienne Renault's avatar
      bricks: fix clang warnings · 154486e0
      Etienne Renault authored
      * bricks/brick-hash.h, bricks/brick-shmem.h: here.
      154486e0
    • Etienne Renault's avatar
      bricks: add bricks for concurrent hashmap · 4eff22ae
      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.
      4eff22ae
    • Etienne Renault's avatar
      modelcheck: rewrite and use argp · 22106212
      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.
      22106212
    • Etienne Renault's avatar
      ltsmin: prodcuce kripkecube · f1315de1
      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.
      f1315de1
    • Etienne Renault's avatar
      convert: kripke and product towards twa · abb4984b
      Etienne Renault authored
      * spot/mc/Makefile.am, spot/mc/utils.hh: here.
      abb4984b
    • Etienne Renault's avatar
      ec: Renault et al LPAR'13 emptiness check · 53e9acf8
      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.
      53e9acf8
    • Etienne Renault's avatar
      intersection: for kripke and twacube · eb3cf788
      Etienne Renault authored
      * spot/mc/Makefile.am, spot/mc/intersect.hh: here.
      eb3cf788
    • Etienne Renault's avatar
      reachability: sequential reachability for kripkecube · a4113d31
      Etienne Renault authored
      * README, configure.ac, spot/mc/Makefile.am,
      spot/mc/reachability.hh: here.
      a4113d31
    • Etienne Renault's avatar
      kripke: define kripkecube structure · 2e7e29eb
      Etienne Renault authored
      * spot/kripke/kripke.hh: here.
      2e7e29eb
    • Etienne Renault's avatar
      convert: twacube to twa translation · cb1af8dd
      Etienne Renault authored
      * spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
      tests/core/twacube.cc, tests/core/twacube.test: here.
      cb1af8dd
    • Etienne Renault's avatar
      convert: twa to twacube translation · be711d61
      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.
      be711d61
    • Etienne Renault's avatar
      convert: BDD to cube conversions · f567bb86
      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.
      f567bb86
    • Etienne Renault's avatar
      Introduce cube data structure · 80bb711f
      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.
      80bb711f
  2. 02 Mar, 2018 1 commit
  3. 01 Mar, 2018 4 commits
  4. 23 Feb, 2018 3 commits
  5. 22 Feb, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      More config for GitLab-CI · f8575b42
      Alexandre Duret-Lutz authored
      * .gitlab-ci.yml: Add a build with gcc-snapshot, and disable Debian
      packages on all branches except master/next/stable and branches ending
      in "-deb".
      f8575b42
  6. 21 Feb, 2018 4 commits
    • Maximilien Colange's avatar
      Slight improvement of the determinization · 41d5e449
      Maximilien Colange authored
      * spot/twaalgos/determinize.cc: the acceptance condition
        of the determinized automaton should be simpler
      * tests/core/safra.test, tests/python/simstate.py: update tests
      41d5e449
    • Maximilien Colange's avatar
      Improve cleanup_parity · e945beb6
      Maximilien Colange authored
      * spot/twaalgos/parity.cc: cleanup_parity and cleanup_parity_here are
        now better at finding useless parity colors
      * tests/python/parity.py: test it
      * NEWS: document the change
      e945beb6
    • Alexandre Duret-Lutz's avatar
      include config.h in all *.cc files · ac6b0c94
      Alexandre Duret-Lutz authored
      This helps working around missing C functions like strcasecmp that do
      not exist everywhere (e.g. on Cygwin), and for which lib/ supplies a
      replacement.  Unfortunately we do not have such build in our current
      continuous integration suite, so we cannot easily detect files where
      such config.h inclusion would be useful.  Therefore this patch simply
      makes it mandatory to include config.h in *.cc files.  Including this
      in public *.hh file is currently forbidden.
      
      * spot/gen/automata.cc, spot/gen/formulas.cc,
      spot/kripke/fairkripke.cc, spot/kripke/kripke.cc,
      spot/ltsmin/ltsmin.cc, spot/misc/game.cc, spot/parseaut/fmterror.cc,
      spot/parsetl/fmterror.cc, spot/parsetl/parsetl.yy,
      spot/priv/bddalloc.cc, spot/priv/freelist.cc, spot/priv/satcommon.cc,
      spot/priv/trim.cc, spot/priv/weight.cc, spot/ta/ta.cc,
      spot/ta/taexplicit.cc, spot/ta/taproduct.cc, spot/ta/tgtaexplicit.cc,
      spot/ta/tgtaproduct.cc, spot/taalgos/dot.cc,
      spot/taalgos/emptinessta.cc, spot/taalgos/minimize.cc,
      spot/taalgos/reachiter.cc, spot/taalgos/statessetbuilder.cc,
      spot/taalgos/stats.cc, spot/taalgos/tgba2ta.cc, spot/tl/apcollect.cc,
      spot/tl/contain.cc, spot/tl/declenv.cc, spot/tl/defaultenv.cc,
      spot/tl/dot.cc, spot/tl/exclusive.cc, spot/tl/hierarchy.cc,
      spot/tl/length.cc, spot/tl/ltlf.cc, spot/tl/mark.cc,
      spot/tl/mutation.cc, spot/tl/nenoform.cc, spot/tl/print.cc,
      spot/tl/randomltl.cc, spot/tl/relabel.cc, spot/tl/remove_x.cc,
      spot/tl/simplify.cc, spot/tl/snf.cc, spot/tl/unabbrev.cc,
      spot/twa/acc.cc, spot/twa/bdddict.cc, spot/twa/bddprint.cc,
      spot/twa/formula2bdd.cc, spot/twa/taatgba.cc, spot/twa/twa.cc,
      spot/twa/twagraph.cc, spot/twa/twaproduct.cc, spot/twaalgos/aiger.cc,
      spot/twaalgos/alternation.cc, spot/twaalgos/are_isomorphic.cc,
      spot/twaalgos/bfssteps.cc, spot/twaalgos/canonicalize.cc,
      spot/twaalgos/cleanacc.cc, spot/twaalgos/cobuchi.cc,
      spot/twaalgos/complement.cc, spot/twaalgos/complete.cc,
      spot/twaalgos/compsusp.cc, spot/twaalgos/couvreurnew.cc,
      spot/twaalgos/cycles.cc, spot/twaalgos/degen.cc,
      spot/twaalgos/determinize.cc, spot/twaalgos/dot.cc,
      spot/twaalgos/dtbasat.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/gtec/status.cc,
      spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc,
      spot/twaalgos/iscolored.cc, spot/twaalgos/isdet.cc,
      spot/twaalgos/isunamb.cc, spot/twaalgos/isweakscc.cc,
      spot/twaalgos/langmap.cc, spot/twaalgos/lbtt.cc,
      spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc,
      spot/twaalgos/magic.cc, spot/twaalgos/mask.cc,
      spot/twaalgos/minimize.cc, spot/twaalgos/neverclaim.cc,
      spot/twaalgos/parity.cc, spot/twaalgos/postproc.cc,
      spot/twaalgos/powerset.cc, spot/twaalgos/product.cc,
      spot/twaalgos/rabin2parity.cc, spot/twaalgos/randomgraph.cc,
      spot/twaalgos/randomize.cc, spot/twaalgos/reachiter.cc,
      spot/twaalgos/relabel.cc, spot/twaalgos/remfin.cc,
      spot/twaalgos/remprop.cc, spot/twaalgos/sbacc.cc,
      spot/twaalgos/sccfilter.cc, spot/twaalgos/sccinfo.cc,
      spot/twaalgos/se05.cc, spot/twaalgos/sepsets.cc,
      spot/twaalgos/simulation.cc, spot/twaalgos/split.cc,
      spot/twaalgos/stats.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, spot/twaalgos/translate.cc,
      spot/twaalgos/word.cc, tests/core/acc.cc, tests/core/bitvect.cc,
      tests/core/checkpsl.cc, tests/core/checkta.cc, tests/core/consterm.cc,
      tests/core/emptchk.cc, tests/core/equalsf.cc, tests/core/graph.cc,
      tests/core/ikwiad.cc, tests/core/intvcmp2.cc, tests/core/intvcomp.cc,
      tests/core/kind.cc, tests/core/kripkecat.cc, tests/core/length.cc,
      tests/core/ltlrel.cc, tests/core/ngraph.cc, tests/core/parity.cc,
      tests/core/randtgba.cc, tests/core/readltl.cc, tests/core/reduc.cc,
      tests/core/safra.cc, tests/core/sccif.cc, tests/core/syntimpl.cc,
      tests/core/taatgba.cc, tests/core/tostring.cc, tests/core/trival.cc,
      tests/core/twagraph.cc, tests/ltsmin/modelcheck.cc,
      spot/parseaut/scanaut.ll, spot/parsetl/scantl.ll: Include config.h.
      * spot/gen/Makefile.am, spot/graph/Makefile.am,
      spot/kripke/Makefile.am, spot/ltsmin/Makefile.am,
      spot/parseaut/Makefile.am, spot/parsetl/Makefile.am,
      spot/priv/Makefile.am, spot/ta/Makefile.am, spot/taalgos/Makefile.am,
      spot/tl/Makefile.am, spot/twa/Makefile.am, spot/twaalgos/Makefile.am,
      spot/twaalgos/gtec/Makefile.am, tests/Makefile.am: Add the -I lib/
      flags.
      * tests/sanity/includes.test: Catch missing config.h in *.cc, and
      diagnose config.h in *.hh.
      * tests/sanity/style.test: Better diagnostics.
      ac6b0c94
    • Alexandre Duret-Lutz's avatar
      cdec6b28
  7. 20 Feb, 2018 4 commits
  8. 19 Feb, 2018 3 commits
  9. 18 Feb, 2018 1 commit
  10. 17 Feb, 2018 1 commit