1. 26 Jul, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      org: document explicit vs. on-the-fly · da464d81
      Alexandre Duret-Lutz authored
      * doc/org/tut50.org: New file.
      * doc/org/tut.org: Add it.
      * NEWS: Mention it.
      * doc/Makefile.am: Add tut50.org, and download plantuml.jar when needed.
      * doc/org/.dir-locals.el.in, doc/org/init.el.in: Activate plantum.
      * HACKING: Mention the Java dependency.
      da464d81
  2. 25 Jul, 2016 1 commit
  3. 22 Jul, 2016 1 commit
  4. 19 Jul, 2016 7 commits
    • Alexandre Duret-Lutz's avatar
      bin: overhaul default input selection · dd6875d5
      Alexandre Duret-Lutz authored
      If no input have been specified, and the standard input is not a tty all
      tools now default to reading it.  If standard input is a tty, all tools
      display an error message.  Additionally, - is now a shorthand for -F- in
      all tools.
      
      * NEWS: Summarize this.
      * bin/common_finput.cc, bin/common_finput.hh (check_no_formulas,
      check_no_automaton): New functions that implement the above istty()
      logic.
      * bin/autfilt.cc, bin/dstar2tgba.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc,
      bin/ltlcross.cc, bin/ltldo.cc, bin/ltlgrind.cc: Use these function,
      and recognize '-' if it was not the case.
      * tests/core/acc_word.test, tests/core/ltldo.test,
      tests/core/minusx.test, tests/core/readsave.test,
      tests/core/unambig.test: Adjust some tests to exercise this.
      * doc/org/autfilt.org, doc/org/csv.org, doc/org/dstar2tgba.org,
      doc/org/ltl2tgba.org, doc/org/ltlcross.org, doc/org/ltlfilt.org,
      doc/org/oaut.org: Adjust the documentation and simplify some
      examples.
      dd6875d5
    • Alexandre Duret-Lutz's avatar
      simplifier: new PSL simplifications · abff7eba
      Alexandre Duret-Lutz authored
      {e[*0..j]}<>->f = {e[*1..j]}<>->f
      {e[*0..j]}[]->f = {e[*1..j]}[]->f
      
      Fixes #81.
      
      This required a small change to the bounded-star-normal-form to prevent
      infinite recursion.
      
      * spot/tl/simplify.cc: Implement these rules.
      * doc/tl/tl.tex, NEWS: Document them.
      * tests/core/reduccmp.test: Add tests, and adjust others.
      * tests/core/unambig.test: Replace formula that used to generated an
      ambiguous automaton, but now generates a deterministic one.
      abff7eba
    • Alexandre Duret-Lutz's avatar
      simplifier: new LTL simplifications · d5b2de7f
      Alexandre Duret-Lutz authored
      if e is pure eventuality and g => e, then e U g = Fg
      if u is purely universal and u => g, then u R g = Gg
      
      Fixes #93.
      
      * doc/tl/tl.tex, NEWS: Document the rules.
      * spot/tl/simplify.cc: Implement them.
      * tests/core/reduccmp.test: Test them.
      * tests/core/det.test: Adjust.
      d5b2de7f
    • Alexandre Duret-Lutz's avatar
      python: have %%dve and %%pml honor SPOT_TMPDIR and TMPDIR · e37f62dc
      Alexandre Duret-Lutz authored
      * python/spot/aux.py (tmpdir): New context manager.
      * python/spot/ltsmin.i: Use it for the two magics.
      * NEWS: Mention this.
      e37f62dc
    • Alexandre Duret-Lutz's avatar
      autfilt: add --stutter-invariant · 4c0500a8
      Alexandre Duret-Lutz authored
      * bin/autfilt.cc: Implement the option.
      * NEWS: Mention it.
      * tests/core/readsave.test, tests/core/stutter-tgba.test: Add some
      tests.
      4c0500a8
    • Alexandre Duret-Lutz's avatar
      stutter: complement non-det automata via determinization · 5a2bc9f9
      Alexandre Duret-Lutz authored
      Fixes #164.
      
      * spot/twaalgos/stutter.hh, spot/twaalgos/stutter.cc: Implement
      the determinization, while keeping it optional.
      * NEWS: Mention the change.
      * tests/core/ltl2dstar.test, tests/core/stutter-tgba.test: Add
      test cases.
      * tests/core/readsave.test: Adjust.
      5a2bc9f9
    • Alexandre Duret-Lutz's avatar
      python: add missing bindings for randomize() · 29a1e3a2
      Alexandre Duret-Lutz authored
      * python/spot/impl.i: Here.
      * NEWS: Mention it.
      * tests/python/highlighting.ipynb: Add test case.
      29a1e3a2
  5. 18 Jul, 2016 7 commits
  6. 15 Jul, 2016 1 commit
  7. 13 Jul, 2016 2 commits
  8. 11 Jul, 2016 6 commits
  9. 07 Jul, 2016 1 commit
  10. 06 Jul, 2016 2 commits
  11. 22 Jun, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      sat-minimize: check for unused options · e80b443b
      Alexandre Duret-Lutz authored
      Fixes #179.
      
      * spot/twaalgos/dtwasat.cc: Add the check.
      * tests/core/minusx.test: Test it.
      * NEWS: Mention it.
      e80b443b
    • 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
  12. 21 Jun, 2016 1 commit
  13. 17 Jun, 2016 2 commits
  14. 14 Jun, 2016 2 commits
  15. 12 Jun, 2016 1 commit
    • 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
  16. 25 May, 2016 1 commit
    • Alexandre Duret-Lutz's avatar
      add binding for language_containment_checker and document them · b4088271
      Alexandre Duret-Lutz authored
      * spot/tl/contain.cc, spot/tl/contain.hh: Simplify the
      use of language_containment_checker by adding default argument.
      * python/spot/__init__.py, python/spot/impl.i: Bind it in Python.
      * doc/org/tut04.org: New file to illustrate it.
      * doc/org/tut.org, doc/Makefile.am: Add it.
      * NEWS: Mention those changes.
      b4088271
  17. 10 May, 2016 1 commit
  18. 09 May, 2016 1 commit