1. 23 Oct, 2015 4 commits
    • Alexandre Duret-Lutz's avatar
      python: change postprocess to take an optional formula · 337925c9
      Alexandre Duret-Lutz authored
      Doing so also work around some differences between Swig 3.0.2 and 3.0.7
      observed on our build farm.
      
      * wrap/python/spot.py: Here.
      * wrap/python/spot_impl.i: Recognize None as a null formula
      on input.
      337925c9
    • Alexandre Duret-Lutz's avatar
      doc: show more metadata about automata · 84f9be9e
      Alexandre Duret-Lutz authored
      * src/twa/bdddict.hh (varnum): New method.
      * doc/org/tut21.org: Show more metadata.
      84f9be9e
    • Alexandre Duret-Lutz's avatar
      parseaut: Add a trust_hoa option. · 51a75a31
      Alexandre Duret-Lutz authored
      Fixes #114.
      
      * src/parseaut/public.hh: Add support for a trust_hoa option.
      * src/parseaut/parseaut.yy: If trust_hoa is set, recognize the
      "inherently-weak" and "stutter-invariant" properties.
      * src/bin/common_conv.cc, src/bin/common_conv.hh (read_automaton):
      Move...
      * src/bin/common_hoaread.cc, src/bin/common_hoaread.hh: ... in this
      new file, that also handle the --trust-hoa option.
      * src/bin/Makefile.am: Add them.
      * src/bin/autfilt.cc, src/bin/dstar2tgba.cc, src/bin/ltlcross.cc,
      src/bin/ltldo.cc: Use them.
      * src/tests/parseaut.test, src/tests/ltldo.test: Adjust, and test
      --trust-hoa=no.
      * src/tests/complement.test, src/tests/prodor.test,
      src/tests/sbacc.test: Adjust.
      * wrap/python/spot.py (automata): Add option trust_hoa.
      * NEWS: Update.
      51a75a31
    • Alexandre Duret-Lutz's avatar
      parseaut: change the interface to allow new options · 585e29e7
      Alexandre Duret-Lutz authored
      * src/parseaut/public.hh, src/parseaut/parseaut.yy: Make it easier to
      pass new options to the parser.
      * src/tests/ikwiad.cc, wrap/python/spot.py: Adjust.
      585e29e7
  2. 22 Oct, 2015 1 commit
  3. 21 Oct, 2015 5 commits
  4. 20 Oct, 2015 3 commits
  5. 19 Oct, 2015 3 commits
  6. 18 Oct, 2015 4 commits
    • Alexandre Duret-Lutz's avatar
      python: add get_name & set_name for automata · 43a5187a
      Alexandre Duret-Lutz authored
      * wrap/python/spot_impl.i (get_name, set_name): New methods for twa.
      * wrap/python/tests/remfin.py: Test them.
      * wrap/python/ajax/spotcgi.in: Use set_name().
      * NEWS: Mention it.
      43a5187a
    • Alexandre Duret-Lutz's avatar
      tl: rename ltl_simplifier to tl_simplifier · 176c9e2e
      Alexandre Duret-Lutz authored
      * doc/org/tut01.org, doc/tl/tl.tex, src/bin/common_r.hh,
      src/bin/ltlfilt.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
      src/tests/randtgba.cc, src/tests/reduc.cc, src/tests/syntimpl.cc,
      src/tl/nenoform.cc, src/tl/randomltl.cc, src/tl/randomltl.hh,
      src/tl/simplify.cc, src/tl/simplify.hh, src/twaalgos/ltl2tgba_fm.cc,
      src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/stutter.cc,
      src/twaalgos/translate.cc, src/twaalgos/translate.hh,
      wrap/python/ajax/spotcgi.in, wrap/python/spot.py,
      wrap/python/tests/interdep.py: Rename ltl_simplifier to tl_simplifier.
      * NEWS: Mention it.
      176c9e2e
    • Alexandre Duret-Lutz's avatar
      * src/tl/simplify.hh: Fix comment. · 21be883c
      Alexandre Duret-Lutz authored
      21be883c
    • Alexandre Duret-Lutz's avatar
      python: update the formulaiterator bindings · 9689c4cc
      Alexandre Duret-Lutz authored
      * wrap/python/spot.py: Add the unabbreviate() method, and
      remove unabbrivate_ltl() and get_literal().
      * wrap/python/tests/randltl.ipynb: Demonstrate unabbreviate().
      9689c4cc
  7. 17 Oct, 2015 1 commit
  8. 16 Oct, 2015 2 commits
  9. 15 Oct, 2015 5 commits
    • Alexandre Duret-Lutz's avatar
      parseaut: better diagnostic of unsupported versions · 9e7d0677
      Alexandre Duret-Lutz authored
      * src/parseaut/parseaut.yy: Add and the a check_version() function.
      * src/tests/parseaut.test: Test it.
      * NEWS: Mention it.
      9e7d0677
    • Alexandre Duret-Lutz's avatar
      ltlgrind: fix handling of FILENAME/COL · 0671d628
      Alexandre Duret-Lutz authored
      This additionally fixes #107.
      
      * src/bin/ltlgrind.cc: Fix handling for FILEANAME/COL.  Document FORMAT
      in --help.  Assume -F for arguments given without options.
      * src/tests/ltlgrind.test: Add two tests.
      * NEWS: Mention this.
      0671d628
    • Alexandre Duret-Lutz's avatar
      autfilt: easier simplification defaults · e3682a23
      Alexandre Duret-Lutz authored
      This is motivated by an email from Fanda.
      
      * src/bin/common_post.cc, src/bin/common_post.hh: Add variables to
      detect when level or pref are sets.
      * src/bin/autfilt.cc: Adjust default for pref/sets.
      * src/tests/readsave.test: Add test cases.
      * NEWS: Mention it.
      e3682a23
    • Alexandre Duret-Lutz's avatar
      autfilt: implement --complement · 2ae1b6a6
      Alexandre Duret-Lutz authored
      * src/bin/autfilt.cc: Add option --complete.
      * src/twaalgos/complete.cc: Better handling of 0-edge automata.
      * src/tests/complement.test: New file.
      * src/tests/Makefile.am: Add it.
      2ae1b6a6
    • Alexandre Duret-Lutz's avatar
      fix crash of randaut -Q0 · 6cf807da
      Alexandre Duret-Lutz authored
      * src/twaalgos/randomgraph.cc: Replace an assertion by an exception.
      * src/bin/randaut.cc: Diagnose -Q0.
      * src/tests/randaut.test: Test it.
      * NEWS: Mention the bug.
      6cf807da
  10. 14 Oct, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      scc_filter_states: also remove useless acceptance marks · cd2e5275
      Alexandre Duret-Lutz authored
      * src/twaalgos/sccfilter.hh,
      src/twaalgos/sccfilter.cc (scc_filter_states): Remove useless acceptance
      marks while preserving state-based acceptance.  Add a new argument
      to specify if all useless mark have to be removed, like for scc_filter.
      * src/twaalgos/simulation.cc: Use the new parameter.
      * src/twaalgos/postproc.cc: Likewise.  Also call do_scc_filter even
      after WDBA simplification to cleanup trivial SCCs.  Preserve state-based
      acceptance for weak automata.
      * src/tests/readsave.test: Add one test.
      * src/tests/dstar.test, src/tests/prodor.test, src/tests/remfin.test,
      src/tests/sim3.test, wrap/python/tests/automata.ipynb,
      wrap/python/tests/piperead.ipynb: Adjust expected output.
      * NEWS: Mention the change.
      cd2e5275
    • Alexandre Duret-Lutz's avatar
      2af36788
  11. 13 Oct, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      restructure the complementation code · 06d3bc67
      Alexandre Duret-Lutz authored
      The previous code was sometime doing the work of remove_fin() in
      addition to complementing the acceptance conditions.  This separate
      the two operations clearly.  Also the specialized code for
      complementing weak automata is now a specialized code for remove_fin()
      on weak automata.
      
      * src/twaalgos/dtgbacomp.hh, src/twaalgos/dtgbacomp.cc: Rename as ...
      * src/twaalgos/complement.hh, src/twaalgos/complement.cc: ... these.
      * src/twaalgos/Makefile.am: Adjust.
      * src/twaalgos/complement.hh (dtgba_complement): Rename as ...
      (dtwa_complement): ... this, and restrict the purpose to completion
      and accetance complementation.  Further acceptance simplification
      can be done with remove_fin() and to_generalized_buchi().
      * src/twaalgos/remfin.cc (remove_fin): Specialize handling of weak
      automata using the code that was originally in dtgba_complement().
      Also mark the output as state-based when the input has to Inf.
      * src/twaalgos/postproc.cc, src/twaalgos/postproc.hh: Make sure
      scc_filter is always called after to_generalized_buchi().
      * bench/stutter/stutter_invariance_randomgraph.cc,
      src/bin/ltlcross.cc, src/tests/ikwiad.cc, src/twaalgos/minimize.cc,
      src/twaalgos/powerset.cc, src/twaalgos/stutter.cc: Adjust usage.
      * src/tests/dstar.test, src/tests/ltl2dstar4.test,
      src/tests/remfin.test: Adjust expected outputs.
      * wrap/python/spot_impl.i: Export dtwa_complement().
      06d3bc67
    • Alexandre Duret-Lutz's avatar
      * src/bin/ltlcross.cc: Typo. · fb642c6d
      Alexandre Duret-Lutz authored
      fb642c6d
  12. 08 Oct, 2015 1 commit
  13. 04 Oct, 2015 2 commits
  14. 03 Oct, 2015 5 commits
    • Alexandre Duret-Lutz's avatar
      org: better syntax highlighting · 24a8affb
      Alexandre Duret-Lutz authored
      * doc/org/init.el.in: Activate CSS for code fragments.
      * doc/org/spot.css: Style relevant elements.
      24a8affb
    • Alexandre Duret-Lutz's avatar
      python: implement formula.__format__ · 5bfd0267
      Alexandre Duret-Lutz authored
      Fixes #105.
      
      * src/bin/common_trans.cc (quote_shell_string): Move ...
      * src/misc/escape.cc, src/misc/escape.hh (quote_shell_string):
      ... here.
      * wrap/python/spot_impl.i: Wrap escape.hh.
      * wrap/python/spot.py: Implement formula.__format__.
      * wrap/python/tests/ltlsimple.py: Test it.
      * NEWS, doc/org/tut01.org, wrap/python/tests/formulas.ipynb: Document
      it.
      5bfd0267
    • Alexandre Duret-Lutz's avatar
      * NEWS: Summarize recent changes. · 20bb1719
      Alexandre Duret-Lutz authored
      20bb1719
    • Alexandre Duret-Lutz's avatar
      Work around weird Python 3.5 generator/iterator interaction · 6ff4fa97
      Alexandre Duret-Lutz authored
      * wrap/python/spot.py: Python 3.5 reports some unexpected SystemError
      messages when the stack of iterator(...(iterator(generator))) we build
      for random LTL generation raises a StopIteration.  The messages are
      attached either to delete_formula or delete_randltlgenerator, claiming
      that these functions exit with an error; but I have checked that they
      do not.  I've been unable to understand the cause of the issue.
      Replacing the generator by an iterator at least fixes the problem in a
      way that is transparent for our API.
      * wrap/python/tests/randltl.ipynb: Adjust expected formulas.
      6ff4fa97
    • Alexandre Duret-Lutz's avatar
      python: do not crash when a function returns a null formula · 5f2d55ab
      Alexandre Duret-Lutz authored
      * wrap/python/spot_impl.i: Map null formulas to None.
      * wrap/python/tests/randgen.py: New file.
      * wrap/python/tests/Makefile.am: Add it.
      5f2d55ab