1. 11 Jun, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      libtool: surrender to Debian's castrated libtool · 97e903b1
      Alexandre Duret-Lutz authored
      The libtool version distributed by Debian is patched to *not* propagate
      dependencies (i.e., if libA depends on libB, then linking against libA
      will not automatically link against libB, it has to be explicit),
      contrary to what the Libtool manual document.  So now we explicitly
      link against both libA and libB in such case.
      
      * configure.ac: Remove the workaround that does not work for
      MinGW.
      * doc/org/compile.org: Mention the issue.
      * bin/Makefile.am, tests/Makefile.am, spot/ltsmin/Makefile.am,
      doc/org/g++wrap.in: Make the dependencies explicit.
      97e903b1
  2. 10 Mar, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      emptiness checks: replace assert-preconditions by exceptions · d6d987bd
      Alexandre Duret-Lutz authored
      * spot/twaalgos/couvreurnew.cc, spot/twaalgos/gv04.cc,
      spot/twaalgos/magic.cc, spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc,
      spot/twaalgos/tau03opt.cc: Throw if precondition on acceptance
      condition is not satisfied.
      * tests/python/misc-ec.py: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the change.
      d6d987bd
  3. 08 Mar, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      python: add bindings for bdd_to_formula() · d1d3ee38
      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.
      d1d3ee38
  4. 07 Mar, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      twa_graph: more test coverage · cd4c326f
      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.
      cd4c326f
  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
  30. 12 Feb, 2016 1 commit