1. 08 Mar, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      python: add bindings for bdd_to_formula() · 4e9303e3
      Alexandre Duret-Lutz authored
      Follow-up to an email from Ayrat Khalimov.
      
      * python/spot/impl.i: Include twa/formula2bdd.hh.
      * python/spot/__init__.py: Make the dictionnary
      optional.
      * spot/twa/formula2bdd.cc: Throw an exception instead of asserting.
      * tests/python/bdditer.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Update.
      4e9303e3
  2. 07 Mar, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      twa_graph: more test coverage · 2e763a08
      Alexandre Duret-Lutz authored
      The goal is to improve coverage stats, but I discovered two issues
      while doing so.
      
      * tests/python/twagraph.py: New test case.
      * tests/Makefile.am: Add it.
      * spot/twa/twagraph.hh: Add fix typos in error messages.
      * python/spot/impl.i: Fix broken wrappers for state_from_number and
      state_acc_sets.
      2e763a08
    • Alexandre Duret-Lutz's avatar
      tests: remove ltlprod · be4f1397
      Alexandre Duret-Lutz authored
      This very old test did not do anything useful today.
      
      * tests/core/ltlprod.cc, tests/core/ltlprod.test: Delete.
      * tests/Makefile.am: Adjust.
      be4f1397
  3. 21 Feb, 2017 1 commit
    • Clément Gillard's avatar
      Add a decompose_scc() function · 164135d3
      Clément Gillard authored
      See #172.
      While at it, fix typo in doxygen comment.
      
      * spot/twaalgos/strength.cc, spot/twaalgos/strength.hh: New function.
      * tests/python/decompose_scc.py, tests/Makefile.am: Test python
      binding.
      
      * spot/twaalgos/mask.hh: Fix typo.
      164135d3
  4. 20 Feb, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      scc_info: add Python bindings · 289b2383
      Alexandre Duret-Lutz authored
      Related to #172, where we discussed that scc_info bindings were
      missing.
      
      * spot/twaalgos/sccinfo.hh (spot::scc_info::scc_node): Move...
      (spot::scc_info_node): ... here to help Swig.
      * python/spot/impl.i: Add bindings for scc_info.
      * tests/python/sccinfo.py: New file.
      * tests/Makefile.am: Add it.
      289b2383
  5. 23 Jan, 2017 1 commit
  6. 10 Jan, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlfilt: add --recurrence and --persistence · de8a248f
      Alexandre Duret-Lutz authored
      * spot/twaalgos/remfin.cc, spot/twaalgos/remfin.hh
      (rabin_to_buchi_maybe): Make this function public.
      * bin/ltlfilt.cc: Implement the two options.
      * tests/core/hierarchy.test: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the new options.
      de8a248f
  7. 29 Dec, 2016 3 commits
    • Alexandre Duret-Lutz's avatar
      support for semi-deterministic property · 4b013878
      Alexandre Duret-Lutz authored
      * spot/twa/twa.hh (prop_semi_deterministic): New methods.
      * spot/parseaut/parseaut.yy, spot/twaalgos/hoa.cc: Add support for the
      semi-deterministic property.
      * doc/org/concepts.org, doc/org/hoa.org: Document it.
      * spot/twaalgos/isdet.cc,
      spot/twaalgos/isdet.hh (is_semi_deterministic): New function.
      * bin/autfilt.cc: Add --is-semi-deterministic.
      * bin/common_aoutput.cc: Add --check=semi-deterministic.
      * tests/core/semidet.test: New file.
      * tests/Makefile.am: Add it.
      * tests/core/parseaut.test, tests/core/readsave.test: Adjust.
      4b013878
    • Alexandre Duret-Lutz's avatar
      ltlcross: add support for alternating automata · 87c9d6f0
      Alexandre Duret-Lutz authored
      * bin/ltlcross.cc: Add an alternation-removal pass, and
      adjust CSV output.
      * doc/org/ltlcross.org: Update.
      * tests/core/ltl3dra.test, tests/core/ltl3ba.test: Add more tests.
      * tests/Makefile.am: Add tests/core/ltl3ba.test.
      * NEWS: Mention it.
      87c9d6f0
    • Alexandre Duret-Lutz's avatar
      alternation: implement remove_alternation() for weak alt automata · fa06cfa3
      Alexandre Duret-Lutz authored
      This mixes the subset construction (for 1-state rejecting SCCs) and
      the breakpoint construction (for larger rejecting SCCs).  The
      algorithm should probably be rewritten in a cleaner and more efficient
      way, but that should do for a first version.  It should be easy to
      extend it to support Büchi acceptance (since the breakpoint
      construction works for this) when we need it.
      
      * spot/twaalgos/alternation.hh,
      spot/twaalgos/alternation.cc (remove_alternation): New function.
      * tests/python/alternation.ipynb: New file.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      fa06cfa3
  8. 27 Dec, 2016 3 commits
    • Alexandre Duret-Lutz's avatar
      sccinfo: adjust to work with alternating automata · a4ce9994
      Alexandre Duret-Lutz authored
      * spot/twaalgos/sccinfo.cc: Consider universal edges as if they were
      existential edges.
      * spot/twaalgos/sccinfo.hh: Document that.
      * spot/twaalgos/dot.cc: Allow option 's' again, for easy testing.
      * tests/core/alternating.test: Adjust tests.
      * tests/python/_altscc.ipynb: New file (more tests).
      * tests/Makefile.am: Add it.
      a4ce9994
    • Alexandre Duret-Lutz's avatar
      dot: add support for alternating automata · d5c9c345
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Handle universal destinations.
      Ignore option 's' for alternating automata.
      * tests/core/alternating.test: New file.
      * tests/Makefile.am: Add it.
      d5c9c345
    • Alexandre Duret-Lutz's avatar
      twa_graph: add basic support for alternation · 6aad559c
      Alexandre Duret-Lutz authored
      This only allows creating universal edges, and reading the associated
      destinations.
      
      * spot/twa/twagraph.hh (new_univ_edges, univ_dests, is_alternating): New
      function.
      * python/spot/impl.i: Add Python bindings.
      * tests/python/alternating.py: New file.
      * tests/Makefile.am: Add it.
      6aad559c
  9. 24 Nov, 2016 1 commit
  10. 23 Nov, 2016 1 commit
    • Maximilien Colange's avatar
      Add support to load GAL models. · c9aabcdd
      Maximilien Colange authored
      * spot/ltsmin/ltsmin.cc: Handle GAL models.
      * tests/Makefile.am: Test the new feature.
      * tests/ltsmin/check.test: Also check GAL.
      * tests/ltsmin/beem-peterson.4.gal: A new GAL model for tests.
      * tests/ltsmin/finite.gal: A new GAL model for tests.
      * tests/ltsmin/finite3.test: A new test for GAL.
      c9aabcdd
  11. 11 Nov, 2016 2 commits
  12. 09 Nov, 2016 1 commit
  13. 05 Nov, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      from_ltlf: new LTL transformation. · 2e69e045
      Alexandre Duret-Lutz authored
      Fixes #187.
      
      * spot/tl/ltlf.cc, spot/tl/ltlf.hh: New files.
      * spot/tl/Makefile.am: Add them.
      * bin/ltlfilt.cc: Add a new option.
      * bin/man/ltlfilt.x: Add bibliographic reference.
      * tests/core/ltlfilt.test: Add more tests.
      * tests/python/ltlf.py: New file.
      * tests/Makefile.am: Add it.
      * python/spot/impl.i: Python bindings.
      * NEWS: Mention it.
      2e69e045
  14. 01 Nov, 2016 1 commit
  15. 15 Aug, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      bin: %a,%b,%s format specs for LTL output · 926ffbf9
      Alexandre Duret-Lutz authored
      * NEWS: Mention those.
      * bin/common_output.cc, bin/common_output.hh: Implement them.
      * bin/genltl.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randltl.cc: Update
      --help.
      * tests/core/format.test: New file.
      * tests/Makefile.am: Add it.
      * doc/org/ioltl.org, doc/org/ltlfilt.org: Update documentation.
      926ffbf9
  16. 14 Aug, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      bin: diagnose more write errors · e97ea5fa
      Alexandre Duret-Lutz authored
      * tests/core/full.test: New file.
      * tests/Makefile.am: Add it.
      * bin/autfilt.cc, bin/common_aoutput.cc, bin/common_aoutput.hh,
      bin/common_file.cc, bin/common_file.hh, bin/genltl.cc, bin/ltlcross.cc,
      bin/ltlfilt.cc, bin/ltlgrind.cc, bin/randltl.cc: Add diagnostics.
      * NEWS: Mention the fix.
      e97ea5fa
  17. 04 Aug, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      implement conversion to GRA and GSA · 14bee1ae
      Alexandre Duret-Lutz authored
      Fixes #174.
      
      * spot/twaalgos/totgba.hh, spot/twaalgos/totgba.cc
      (to_generalized_streett, to_generalized_rabin): New functions.
      * spot/twa/acc.hh: Declare more methods as static.
      * bin/autfilt.cc: Implement --generalized-rabin and
      --generalized-streett options.
      * NEWS: Mention these.
      * tests/core/gragsa.test: New file.
      * tests/Makefile.am: Add it.
      14bee1ae
  18. 27 Jul, 2016 1 commit
  19. 19 Jul, 2016 1 commit
  20. 18 Jul, 2016 1 commit
  21. 22 Jun, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      option_map: Diagnose unused option on request · e419150c
      Alexandre Duret-Lutz authored
      * spot/misc/optionmap.hh, spot/misc/optionmap.cc (report_unused_options,
      set_, set_set_): New methods.
      * bin/autfilt.cc, bin/dstar2tgba.cc, bin/ltl2tgba.cc,
      bin/ltl2tgta.cc: Call report_unused_options().
      * tests/core/ltlcross2.test, tests/core/readsave.test: Fix typos in
      options.
      * tests/core/minusx.test: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention this.
      e419150c
  22. 17 Jun, 2016 2 commits
  23. 14 Jun, 2016 2 commits
  24. 12 Jun, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      python: add a %%pml magic · 272daf62
      Alexandre Duret-Lutz authored
      Fixes #162.
      
      * python/spot/ltsmin.i: Implement the magic.
      * NEWS: Mention it.
      * tests/python/ltsmin-pml.ipynb: New file.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      * tests/python/ipnbdoctest.py: Adjust.
      272daf62
    • Alexandre Duret-Lutz's avatar
      tests: rename ltsmin.ipynb · a7e4395f
      Alexandre Duret-Lutz authored
      * tests/python/ltsmin.ipynb: Rename as ...
      * tests/python/ltsmin-dve.ipynb: ... this.
      * doc/org/tut.org, tests/Makefile.am: Adjust.
      a7e4395f
  25. 05 May, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      genltl: add formulas from three papers · b708ab77
      Alexandre Duret-Lutz authored
      Fixes #166.
      
      * bin/genltl.cc: Add option --dac-patterns, --eh-patterns,
      --sb-patterns.
      * NEWS, bin/man/genltl.x, doc/org/genltl.org: Document them.
      * bench/ltl2tgba/formulae.ltl: Delete.
      * bench/ltl2tgba/known: Use genltl instead.
      * bench/ltl2tgba/Makefile.am, bench/ltl2tgba/README: Update.
      * tests/core/ltl2tgba2.test: New test case, using genltl.
      * tests/Makefile.am: Add it.
      b708ab77
  26. 17 Mar, 2016 1 commit
  27. 07 Mar, 2016 1 commit
    • Amaury Fauchille's avatar
      autfilt: add new option --accept-word · 1c824443
      Amaury Fauchille authored
      Suggested by Matthias Heizmann. Fixes #109.
      
      * NEWS: notify the new option
      * THANKS: add Matthias Heizmann
      * bin/autfilt.cc: add new option --accept-word=WORD which filters
      automata that accept WORD
      * doc/org/autfilt.org: add an example of the new option
      * tests/Makefile.am: add core/acc_word.test to the list of test files
      * tests/core/acc_word.test: test some uses of the new option
      1c824443
  28. 17 Feb, 2016 2 commits
  29. 16 Feb, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      otf_product: fix deletion of iter_cache_ · 3a3913cf
      Alexandre Duret-Lutz authored
      Fixes #152, reported by Valentin Iovene.
      
      * spot/twa/twaproduct.cc (~twa_product): Delete iter_cache_.
      * tests/python/otfcrash.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the bug.
      3a3913cf
    • Alexandre Duret-Lutz's avatar
      python: report dot errors · 22af7aef
      Alexandre Duret-Lutz authored
      * python/spot/aux.py: Catch errors from dot and signal them.
      * tests/python/_aux.ipynb: New file.
      * tests/Makefile.am: Add it.
      * tests/sanity/ipynb.pl: Support the convention that tests starting with
      '_' should not be published on the web site.
      22af7aef