1. 19 May, 2020 2 commits
  2. 18 May, 2020 8 commits
    • Etienne Renault's avatar
      mc: rework and test conversion into twa · 4bc35906
      Etienne Renault authored
      * spot/mc/Makefile.am,
      spot/mc/reachability.hh,
      spot/mc/utils.hh,
      tests/Makefile.am,
      tests/ltsmin/.gitignore,
      tests/ltsmin/testconvert.cc,
      tests/ltsmin/testconvert.test: Here.
      4bc35906
    • Etienne Renault's avatar
      prefer -pthread to -lpthread · 03436697
      Etienne Renault authored
      * configure.ac,
      spot/ltsmin/Makefile.am,
      tests/Makefile.am: Here.
      03436697
    • 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
      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
  3. 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
  4. 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
  5. 12 Mar, 2020 2 commits
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
  11. 11 Dec, 2019 1 commit
  12. 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
  13. 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
  14. 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
  15. 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
  16. 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
  17. 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
  18. 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
  19. 02 Feb, 2019 1 commit
  20. 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
  21. 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
  22. 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
  23. 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
  24. 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
  25. 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
  26. 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
  27. 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
  28. 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
  29. 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