1. 18 May, 2020 5 commits
    • Etienne Renault's avatar
      tests: add pthread library · 866f75f1
      Etienne Renault authored
      * tests/Makefile.am: here.
      866f75f1
    • 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: 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
      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. 11 Apr, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      ignore false edges in emptiness checks and scc_info · 0b258202
      Alexandre Duret-Lutz authored
      Based on reports by Florian Renkin and Jens Kreber.
      
      * spot/twaalgos/bfssteps.cc, spot/twaalgos/couvreurnew.cc,
      spot/twaalgos/gtec/gtec.cc, spot/twaalgos/gv04.cc,
      spot/twaalgos/magic.cc, spot/twaalgos/sccinfo.cc
      spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc: Ignore bddfalse edges.
      * spot/twaalgos/gtec/gtec.hh: Remove debugging function.
      * tests/core/neverclaimread.test: Adjust.
      * tests/python/ecfalse.py: New test file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the bug.
      0b258202
  3. 24 Mar, 2020 1 commit
    • Florian Renkin's avatar
      Moved IAR and the new version of to_parity in toparity.cc · 75990063
      Florian Renkin authored
      * python/spot/__init__.py: Use keyword arguments in to_parity()
      * python/spot/impl.i: remove useless includes.
      * spot/twaalgos/car.cc, spot/twaalgos/car.hh,
      spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh,
      tests/Makefile.am, spot/twaalgos/Makefile.am:
      content moved to toparity.
      * spot/twaalgos/postproc.cc: Use the new version of to_parity in
      postprocessor::run.
      * spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: Add the
      content of rabin2parity and car.
      * tests/python/car.py, tests/python/toparity.py: Moved all tests
      from car.py to toparity.py.
      * tests/python/except.py: Change iar() to iar_old().
      75990063
  4. 12 Mar, 2020 2 commits
  5. 24 Feb, 2020 1 commit
    • Florian Renkin's avatar
      CAR: new algorithm for paritizing · 96531f29
      Florian Renkin authored
      * NEWS: Mention it.
      * spot/twaalgos/car.cc, spot/twaalgos/car.hh, tests/python/car.py:
      New files.
      * spot/twaalgos/Makefile.am, tests/Makefile.am: Add them.
      * python/spot/impl.i: Include CAR.
      * spot/twa/acc.cc, spot/twa/acc.hh, spot/twa/twagraph.cc,
      spot/twa/twagraph.hh: Add supporting methods.
      96531f29
  6. 15 Feb, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      autfilt add support for --partial-degeneralize · b5e464e0
      Alexandre Duret-Lutz authored
      * bin/autfilt.cc: Add a --partial-degeneralize option.
      * NEWS: Mention it.
      * spot/twaalgos/degen.cc: Do not restrict partial_degeneralize() to
      deterministic automata.
      * spot/twaalgos/degen.hh: Adjust documentation.
      * tests/core/pdegen.test: New test case.
      * tests/Makefile.am: Add it.
      * tests/python/pdegen.py: Adjust.
      b5e464e0
  7. 28 Jan, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      Inf(i)|Inf(j) -> Inf(k) and Fin(i)&Fin(j) -> Fin(k) · 50c0f880
      Alexandre Duret-Lutz authored
      Implement those rules in simplify_acceptance_here().
      
      * NEWS: Mention the change.
      * spot/twa/acc.cc,
      spot/twa/acc.hh (acc_cond::acc_code::used_once_sets): New method.
      * spot/twaalgos/cleanacc.cc, spot/twaalgos/cleanacc.hh:
      Implement the above rule.
      * tests/core/remfin.test: Adjust expected results.
      * tests/python/simplacc.py: New file.
      * tests/Makefile.am: Add it.
      50c0f880
  8. 31 Dec, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      tmpfile: improve error message · 67b9bfda
      Alexandre Duret-Lutz authored
      * spot/misc/tmpfile.cc: Display strerror(errno) plus some suggestions
      that depend on the error.  Based on a report from Shengping Shaw.
      * THANKS: Add reporter.
      * tests/core/ltlcross5.test: New file.
      * tests/Makefile.am: Add it.
      67b9bfda
  9. 15 Dec, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      tmpfile: improve error message · d2ba5545
      Alexandre Duret-Lutz authored
      * spot/misc/tmpfile.cc: Display strerror(errno) plus some suggestions
      that depend on the error.  Based on a report from Shengping Shaw.
      * THANKS: Add reporter.
      * tests/core/ltlcross5.test: New file.
      * tests/Makefile.am: Add it.
      d2ba5545
  10. 11 Dec, 2019 1 commit
  11. 12 Sep, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      fix failing tests on Debian unstable · b1007a3d
      Alexandre Duret-Lutz authored
      * tests/Makefile.am (ltsmin_modelcheck_LDADD): Add -lpthread as it
      seems Debian's libtool does not carries this dependency over from
      libspotltsmin.la.  Also using $(LTLIBMULTITHREAD) does not work,
      because that would add -pthread which is currently ignored when
      linking shared libraries (because libtool adds -nostdlib for some
      reason).
      b1007a3d
  12. 18 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      simplify: GF(f)=GF(dnf(f)) FG(f)=FG(cnf(f)) · da5d23f0
      Alexandre Duret-Lutz authored
      These rules come from Delag's paper, and help some cases
      in issue #385.
      
      * spot/tl/simplify.cc: Implement the simplification.
      * doc/tl/tl.tex, NEWS: Document it.
      * tests/core/385.test: New file.
      * tests/Makefile.am: Add it.
      * tests/core/reduccmp.test: More tests.
      * tests/core/ltl2tgba2.test: Adjust one improved case.
      * tests/python/automata.ipynb, tests/python/twagraph-internals.ipynb:
      Adjust expected output, as the cnf/dnf reorder some subformulas.
      da5d23f0
  13. 04 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      remprop: reset no-terminal property · 7d6bfe54
      Alexandre Duret-Lutz authored
      Reported by Yong Li.
      
      * spot/twaalgos/remprop.cc: Here.
      * tests/python/removeap.py: New test case.
      * tests/Makefile.am: Add it.
      * NEWS: Document the issue.
      * THANKS: Add Yong Li.
      7d6bfe54
  14. 02 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      remprop: reset no-terminal property · 74786324
      Alexandre Duret-Lutz authored
      Reported by Yong Li.
      
      * spot/twaalgos/remprop.cc: Here.
      * tests/python/removeap.py: New test case.
      * tests/Makefile.am: Add it.
      * NEWS: Document the issue.
      * THANKS: Add Yong Li.
      74786324
  15. 24 May, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      word: introduce use_all_aps() · 36d20696
      Alexandre Duret-Lutz authored
      This allows fixing issue #388 reported by Victor Khomenko.
      
      * spot/twaalgos/word.cc, spot/twaalgos/word.hh (use_all_aps): New
      method.
      * tests/python/stutter-inv.ipynb: Use it.
      * tests/python/stutter.py: New file, with Victor's test case.
      * tests/Makefile.am: Add python/stutter.py.
      36d20696
  16. 16 Mar, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      python: improve kripke_graph bindings · 8f7a0c2f
      Alexandre Duret-Lutz authored
      Related to issue #376.
      
      * spot/kripke/kripkegraph.hh: Avoid indirect type definitions for the
      benefit of Swig.
      * python/spot/impl.i: Add bindings for iterators over kripke_graph
      states and edges.
      * tests/python/kripke.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Update.
      8f7a0c2f
  17. 21 Feb, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      python: improve kripke_graph bindings · eb02db85
      Alexandre Duret-Lutz authored
      Related to issue #376.
      
      * spot/kripke/kripkegraph.hh: Avoid indirect type definitions for the
      benefit of Swig.
      * python/spot/impl.i: Add bindings for iterators over kripke_graph
      states and edges.
      * tests/python/kripke.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Update.
      eb02db85
  18. 02 Feb, 2019 1 commit
  19. 14 Jan, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      python: improve bdd_dict bindings · 3908cc1b
      Alexandre Duret-Lutz authored
      Fixes #372.
      
      * python/spot/impl.i: Refactor the handling of exceptions using a
      Lippincott function.  Map out_of_range to IndexError.  Add
      PyObject* version for bdd_dict's register and unregister functions
      so we can use Python objects as well.
      * tests/python/bdddict.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the changes.
      3908cc1b
  20. 02 Aug, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_info: fix split_on_sets · b2e51545
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.cc (split_on_sets): Correctly register APs.
      * tests/python/sccsplit.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the bug.
      b2e51545
  21. 26 Jul, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_info: fix split_on_sets · 9f81df2c
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.cc (split_on_sets): Correctly register APs.
      * tests/python/sccsplit.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the bug.
      9f81df2c
  22. 24 Jul, 2018 2 commits
    • Maximilien Colange's avatar
      translate any automaton to a parity automaton · 465536d1
      Maximilien Colange authored
      * spot/twaalgos/toparity.cc, spot/twaalgos/toparity.hh: implement it,
        based on last-appearance record (LAR)
      * spot/twaalgos/Makefile.am: build it
      * NEWS: document it
      * python/spot/impl.i: add to python bindings
      * tests/Makefile.am, tests/python/toparity.py: test it
      465536d1
    • Alexandre Duret-Lutz's avatar
      genem: implement a generic emptiness check for twa_graph_ptr · d708174c
      Alexandre Duret-Lutz authored
      * spot/twa/acc.cc, spot/twa/acc.hh (fin_unit, one_fin): New function.
      * spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: New files.
      * spot/twaalgos/Makefile.am: Add it.
      * tests/python/genem.py: New file.
      * tests/Makefile.am: Add it.
      * python/spot/impl.i: Add bindings for genem.hh.
      * NEWS: Mention the new function.
      d708174c
  23. 12 Jul, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      more documentation for twa_graph internals · 46590af6
      Alexandre Duret-Lutz authored
      * spot/graph/graph.hh, spot/twa/twagraph.hh, spot/twa/twagraph.cc:
      Implement a dump_storage_as_dot() method.
      * python/spot/__init__.py (twa_graph.show_storage): New method, above
      dump_storage_as_dot().
      * tests/python/twagraph-internals.ipynb: New file, with documentation
      about the twa_graph internals, using show_storage() to illustrate
      everything.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      * python/spot/impl.i: Add bindings for out_iterasor, demonstrated in
      the Python notebook.
      * spot/twa/twa.hh: Add prop_reset().  Used in the notebook.
      * NEWS: Mention the new notebook and function.
      * doc/org/tut50.org: Link to the notebook.
      * tests/python/ipnbdoctest.py: Adjust for twa_graph_ptr being
      redefined in the spot namespace.
      46590af6
  24. 06 Jul, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      tl: add support for X[n], F[n:m] and G[n:m] · e7aa334a
      Alexandre Duret-Lutz authored
      * NEWS, doc/tl/tl.tex, doc/tl/tl.bib: Document these new operators.
      * spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse those.
      * spot/tl/formula.cc, spot/tl/formula.hh: Add constructors.
      * spot/gen/formulas.cc: Use it.
      * tests/core/sugar.test: New file.
      * tests/Makefile.am: Add it.
      e7aa334a
  25. 02 Jul, 2018 1 commit
    • Antoine Martin's avatar
      implement NCSB complementation · c717b588
      Antoine Martin authored
      * spot/twaalgos/isdet.cc,spot/twaalgos/isdet.hh: Two new functions to
      highlight deterministic SCCs
      * spot/twaalgos/complement.cc,spot/twaalgos/complement.hh:
      Implementation of the NCSB complementation algorithm
      * tests/Makefile.am, tests/python/complement_semidet.py: Test the
      implementation
      * NEWS: document function
      c717b588
  26. 20 Jun, 2018 2 commits
    • Maximilien Colange's avatar
      make valgrind understand our memory pools · 3fe74f1c
      Maximilien Colange authored
      Annotate pools with valgrind macros so that it detects errors in pool
      usage. Typically, we wish valgrind to detect a leak when the user fails
      to call proper deallocation function.
      
      * spot/misc/fixpool.hh, spot/misc/mspool.hh: here
      * configure.ac: ensure that valgrind header exists
      * tests/Makefile.am, tests/core/mempool.cc, tests/core/mempool.test,
        tests/core/.gitignore: add tests to ensure valgrind accurately detects
        leaks
      3fe74f1c
    • Alexandre Duret-Lutz's avatar
      product_susp: new function · 4f2e9512
      Alexandre Duret-Lutz authored
      * spot/twaalgos/product.cc, spot/twaalgos/product.hh: Implement it.
      * tests/python/_product_susp.ipynb: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention it.
      4f2e9512
  27. 24 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      autfilt: better handling of chain of products with -B · c87c13db
      Alexandre Duret-Lutz authored
      Fixes #348, reported by Jeroen Meijer.
      
      * bin/autfilt.cc: If -B is used with many --product,
      degeneralize intermediate products as needed.
      * NEWS: Mention the change.
      * tests/core/prodchain.test: New file.
      * tests/Makefile.am: Add it.
      * spot/twa/acc.cc, spot/twa/acc.hh: Fix reporting of
      overflow.
      * tests/core/acc.cc: Adjust.
      c87c13db
  28. 23 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      product: optimize product with weak automata · a738801e
      Alexandre Duret-Lutz authored
      Fixes #350.
      
      * spot/twaalgos/product.cc: Implement this change.
      * NEWS, spot/twaalgos/product.hh: Mention it.
      * spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::sat_mark): New method.
      * tests/python/_product_weak.ipynb: New file.
      * tests/Makefile.am: Add it.
      * tests/python/automata.ipynb, tests/python/highlighting.ipynb,
      tests/python/product.ipynb, tests/core/prodor.test: Adjust test cases.
      a738801e
  29. 04 May, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      introduce containement checks functions · d6f96181
      Alexandre Duret-Lutz authored
      * spot/twaalgos/contains.hh, spot/twaalgos/contains.cc: New files.
      * spot/twaalgos/Makefile.am, python/spot/impl.i: Add them.
      * python/spot/__init__.py: Also attach these functions as methods,
      and support string arguments.
      * tests/python/contains.ipynb: New file.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      * bin/autfilt.cc, tests/python/streett_totgba.py, tests/python/sum.py,
      tests/python/toweak.py: Use the new function.
      d6f96181
  30. 30 Apr, 2018 1 commit
    • Maximilien Colange's avatar
      ltlsynt: improve construction of turn-based games · 1fdc32f9
      Maximilien Colange authored
      Improve the way transitions are duplicated when preparing the turn-based
      game for synthesis. The resulting arena should now be deterministic on
      nodes owned by the environment. Also move the code to another file, so
      that it is easier to test (e.g. in Python).
      
      * bin/ltlsynt.cc: move the code
      * spot/twaalgos/split.cc, spot/twaalgos/split.hh: move the code and
        implement the improvements
      * tests/Makefile.am, tests/python/split.py: test it
      * tests/core/ltlsynt.test: update existing tests to reflect the changes
      1fdc32f9
  31. 03 Apr, 2018 2 commits
  32. 30 Mar, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      sat_minimize: improve logs and document Python bindings · c766f58d
      Alexandre Duret-Lutz authored
      * spot/priv/satcommon.cc, spot/priv/satcommon.hh: Make it possible to
      set the log file without setting the environment variable.  Adjust
      print_log to take the input state and print it as a new column.
      * spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc: Adjust all
      calls to print_log.  Fix log output for incremental approaches.
      Prefer purge_unreachable_states() over stats_reachable().  Do
      not call scc_filter() on colored automata.
      * spot/twaalgos/dtwasat.hh: Document the new "log" option.
      * NEWS: Mention the changes.
      * tests/python/satmin.ipynb: New file.
      * tests/Makefile.am: Add it.
      * doc/org/satmin.org, doc/org/tut.org: Link to it.
      * doc/org/satmin.org, bin/man/spot-x.x: Adjust description
      of CSV files.
      * bench/dtgbasat/gen.py, bench/dtgbasat/tabl.pl,
      bench/dtgbasat/tabl1.pl, bench/dtgbasat/tabl2.pl,
      bench/dtgbasat/tabl3.pl, bench/dtgbasat/tabl4.pl: Adjust for
      the new column.
      * spot/misc/satsolver.cc, spot/misc/satsolver.hh (stats): Make it
      const.
      * python/spot/__init__.py (sat_minimize): Add display_log and
      return_log options.
      * tests/python/ipnbdoctest.py: Adjust to not compare SAT-minimization
      logs as they contain timings.
      c766f58d