1. 18 May, 2020 20 commits
    • Etienne Renault's avatar
      mc: sequential version of Bloemen · adccc0c1
      Etienne Renault authored
      * spot/mc/Makefile.am, spot/mc/bloemen.hh,
      spot/mc/mc.hh, tests/ltsmin/modelcheck.cc: here.
      adccc0c1
    • Etienne Renault's avatar
      mc: add swarmed deadlock-detection · 646f22ed
      Etienne Renault authored
      * spot/mc/Makefile.am, spot/mc/deadlock.hh,
      spot/mc/mc.hh, tests/ltsmin/modelcheck.cc: here.
      646f22ed
    • Etienne Renault's avatar
      ltsmin: move modelchek in mc directory · b8683488
      Etienne Renault authored
      * spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh,
      spot/mc/Makefile.am, tests/ltsmin/modelcheck.cc,
      spot/mc/mc.hh: here.
      b8683488
    • Etienne Renault's avatar
      modelcheck: please gcc catch-value errors · 59e66804
      Etienne Renault authored
      * tests/ltsmin/modelcheck.cc: here.
      59e66804
    • Etienne Renault's avatar
      tests: add pthread library · 866f75f1
      Etienne Renault authored
      * tests/Makefile.am: here.
      866f75f1
    • Etienne Renault's avatar
      includes: must not check *.hxx · f28fc664
      Etienne Renault authored
      * tests/sanity/includes.test: here.
      f28fc664
    • Etienne Renault's avatar
      bricks: adapt with the new bricks · aecdda37
      Etienne Renault authored
      * bricks/brick-hash, tests/core/bricks.cc: here.
      aecdda37
    • 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
      Twacube must share the order of atomic propositions · 6d44a2a3
      Etienne Renault authored
      * spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh,
      tests/ltsmin/modelcheck.cc: here.
      6d44a2a3
    • Etienne Renault's avatar
      modelcheck: support for csv extraction · 9d9d3197
      Etienne Renault authored
      * tests/ltsmin/modelcheck.cc: here.
      9d9d3197
    • 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
      modelcheck: support for twacube · 49048600
      Etienne Renault authored
      * spot/ltsmin/ltsmin.cc, spot/ltsmin/ltsmin.hh,
      tests/ltsmin/modelcheck.cc: here.
      49048600
    • Etienne Renault's avatar
      convert: simplify interfaces · 7ae9bce6
      Etienne Renault authored
      * spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
      tests/core/twacube.cc: here.
      7ae9bce6
    • 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
      bricks: add bricks for concurrent hashmap · 2e644e0d
      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.
      2e644e0d
    • Etienne Renault's avatar
      modelcheck: rewrite and use argp · 1ea046a5
      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.
      1ea046a5
    • Etienne Renault's avatar
      convert: twacube to twa translation · fba4bdeb
      Etienne Renault authored
      * spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh,
      tests/core/twacube.cc, tests/core/twacube.test: here.
      fba4bdeb
    • 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
    • Etienne Renault's avatar
      convert: BDD to cube conversions · 9725456b
      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.
      9725456b
    • Etienne Renault's avatar
      Introduce cube data structure · 1e271b5a
      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.
      1e271b5a
  2. 16 May, 2020 3 commits
    • Alexandre Duret-Lutz's avatar
      ltlsynt: make sure the previous Xor optimization actually works · 66aa6d08
      Alexandre Duret-Lutz authored
      * spot/tl/simplify.hh, spot/tl/simplify.cc,
      spot/twaalgos/translate.cc: Update the tl_simplification
      options after all preferences have been given.
      * bin/ltlsynt.cc: Display the size of the translation output.
      * tests/core/ltlsynt.test: Add test case.
      66aa6d08
    • Alexandre Duret-Lutz's avatar
      translate: improve handling of Xor and Equiv at top-level for -G -D · 6bfa9793
      Alexandre Duret-Lutz authored
      * spot/tl/formula.hh: Add variant of formula::is that support 4
      arguments.
      * spot/tl/simplify.hh, spot/tl/simplify.cc: Add option keep_top_xor
      to preserve Xor and Equiv at the top-level.
      * spot/twaalgos/translate.cc: Adjust ltl-split to deal with Xor and
      Equiv for the -D -G case.
      * NEWS: Mention that.
      * tests/core/ltl2tgba2.test: Add test case.
      * tests/python/simstate.py: Adjust expected result.
      6bfa9793
    • Alexandre Duret-Lutz's avatar
      product: add product_xor() and product_xnor() · 3ab2dd17
      Alexandre Duret-Lutz authored
      * spot/twaalgos/product.cc, spot/twaalgos/product.hh: Add those
      functions.
      * tests/python/_product_weak.ipynb, tests/python/except.py: Test them.
      * NEWS: Mention them.
      3ab2dd17
  3. 30 Apr, 2020 1 commit
  4. 29 Apr, 2020 2 commits
    • Alexandre Duret-Lutz's avatar
      dot: fix #393 · a7051b32
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Add support for option 'E', and default to
      rectangle nodes for large labels.
      * bin/common_aoutput.cc, NEWS: Document it.
      * tests/core/alternating.test, tests/core/dstar.test,
      tests/core/readsave.test, tests/core/sccdot.test,
      tests/core/tgbagraph.test, tests/python/_product_weak.ipynb,
      tests/python/alternation.ipynb, tests/python/atva16-fig2b.ipynb,
      tests/python/automata.ipynb, tests/python/decompose.ipynb,
      tests/python/gen.ipynb, tests/python/highlighting.ipynb,
      tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
      tests/python/parity.ipynb, tests/python/pdegen.py,
      tests/python/satmin.ipynb, tests/python/stutter-inv.ipynb: Adjust all
      test cases.
      a7051b32
    • Alexandre Duret-Lutz's avatar
      dot: fix #392 · 3ea63e9a
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Add tooltips to "..." states and edges.
      * tests/core/readsave.test: Test this.
      * tests/python/highlighting.ipynb: Adjust.
      3ea63e9a
  5. 25 Apr, 2020 2 commits
    • Alexandre Duret-Lutz's avatar
      postproc: fix issue #402 · 67060420
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
      spot/twaalgos/translate.cc: Introduce a gen-reduce-parity option and
      use it on sub-automata built by ltl-split.
      * bin/spot-x.cc: Document it.
      * tests/core/ltl2tgba2.test: Add test case reported by Juraj Major.
      67060420
    • Alexandre Duret-Lutz's avatar
      ltlsynt: fix lar.old implementation · fe340ae8
      Alexandre Duret-Lutz authored
      * bin/ltlsynt.cc: Make sure to_parity_old() receive a deterministic
      automaton, for correctness.   Also call reduce_parity() afterward,
      to match what was done in 2.8.7.
      * tests/core/ltlsynt.test: Include lar.old in the comparison of all
      results to make sure it give the same result as the other 3
      algorithms.
      fe340ae8
  6. 18 Apr, 2020 2 commits
  7. 17 Apr, 2020 6 commits
    • Alexandre Duret-Lutz's avatar
      to_parity: only call reduce_parity() when prefix_parity is enabled · fd0d752b
      Alexandre Duret-Lutz authored
      Calling reduce_parity() in to_parity() is confusing, because then
      running to_parity() on one SCC does not necessarily produce the same
      output as running to_parity() on the entire automaton.  However it is
      necessary for the implementation of parity_prefix.  As a compromise,
      disable reduce_parity() when parity_prefix is disabled, this way we
      can use that to demonstrate how the algorithm works.
      
      * spot/twaalgos/toparity.hh, spot/twaalgos/toparity.cc: Do not
      call reduce_parity() when parity_prefix is disabled.
      * tests/python/toparity.py: Adjust.
      fd0d752b
    • Alexandre Duret-Lutz's avatar
      simplify_acc: loop over the simplifications · 102ef043
      Alexandre Duret-Lutz authored
      * spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Run the
      simplifications in a loop until the condition does not change anymore.
      * tests/python/simplacc.py, tests/core/accsimpl.test,
      tests/core/remfin.test, tests/python/merge.py,
      tests/python/simplacc.py, tests/python/toparity.py: Update expected
      results.
      * tests/python/automata.ipynb: Update the failing example to a more
      interesting one, matching the one in doc/org/autfilt.org.
      102ef043
    • Alexandre Duret-Lutz's avatar
      simplify_acc: fix an infinite loop · b62e1bb1
      Alexandre Duret-Lutz authored
      * spot/twaalgos/cleanacc.cc (fuse_mark_here): Fix incorrect cancelling
      of n-ary subterms, causing an invalid acceptance condition, and then
      an infinite loop.
      * tests/python/simplacc.py: Add test case.
      b62e1bb1
    • Florian Renkin's avatar
      to_parity: Correct the expected number of states · 68012e6a
      Florian Renkin authored
      * tests/python/toparity.py: here.
      68012e6a
    • Florian Renkin's avatar
      to_parity: Remove merge_states · 527b62c5
      Florian Renkin authored
      * spot/twaalgos/toparity.cc: Remove merge_states.
      * tests/python/automata.ipynb, tests/python/toparity.py: Update tests.
      527b62c5
    • Florian Renkin's avatar
      unit_propagation: Add a test with multiple unit clauses · 142f1afa
      Florian Renkin authored
      * tests/core/acc.cc, tests/core/acc.test: here.
      142f1afa
  8. 16 Apr, 2020 3 commits
  9. 12 Apr, 2020 1 commit
    • Florian Renkin's avatar
      to_parity: Improve to_parity and update tests · 0ba10976
      Florian Renkin authored
      * spot/twaalgos/toparity.cc: Use a better search of the
      transitions when we search compatible states.
      * spot/twaalgos/toparity.hh: Use less that 80 columns.
      * tests/python/merge.py, tests/python/toparity.py: Update tests.
      0ba10976