1. 20 Apr, 2015 2 commits
  2. 14 Apr, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      python: fix non-determinism in the test suite. · 39b92a6d
      Alexandre Duret-Lutz authored
      Some tests calling spot.automaton('non-existing|') where failing either
      with a "process returned 127", or, under heavier load, with "failed to
      read from...".  The latter occur if we poll() the exit status before the
      children has had the tame to finish.
      
      * wrap/python/spot.py: Make sure we wait for the child process if we
      reach EOF, so that we can report the error status.
      * wrap/python/tests/automata-io.ipynb, wrap/python/tests/piperead.ipynb:
      Update.
      39b92a6d
    • Alexandre Duret-Lutz's avatar
      python: avoid some locking errors with the history · ebdb5b7c
      Alexandre Duret-Lutz authored
      * wrap/python/tests/ipnbdoctest.py: Store all the history
      in memory.
      ebdb5b7c
  3. 13 Apr, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      python: fix error handling while reading automata · ab7ee2c4
      Alexandre Duret-Lutz authored
      * wrap/python/tests/run.in: Make it easier to run python with gdb.
      * wrap/python/tests/automata-io.ipynb: Add test case.
      * wrap/python/spot.py (spot.automata): Make sure p is defined in all
      cases.
      * src/hoaparse/hoascan.ll: Make sure we do not close a file that
      hasn't been opened.
      ab7ee2c4
  4. 02 Apr, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      python: better bindings for testing automata · 16204e8e
      Alexandre Duret-Lutz authored
      * src/taalgos/dotty.cc, src/taalgos/dotty.hh: Add an interface
      similar to that of tgba/dotty.hh, even if we have to ignore
      most options.
      * src/taalgos/tgba2ta.cc, src/taalgos/tgba2ta.hh: Add an option
      to display the intermediate automaton with explicit stuttering
      transitions, for the purpose of making demonstrations.
      * src/tgba/tgbagraph.hh: Tweak the file so that SWIG can
      read it.
      * wrap/python/spot.py: Add wrappers for testing automata.
      * wrap/python/spot_impl.i: Fix support for
      atomic_prop_collect_as_bdd, and include a few more files.
      * wrap/python/tests/testingaut.ipynb: New file.
      * wrap/python/tests/Makefile.am: Add it.
      16204e8e
  5. 01 Apr, 2015 1 commit
  6. 31 Mar, 2015 2 commits
  7. 30 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      python: read automata from pipes · 961d005b
      Alexandre Duret-Lutz authored
      * src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll,
      src/hoaparse/parsedecl.hh, src/hoaparse/public.hh:
      Add a way to read automata from a file descriptor.
      * wrap/python/spot.py: Add machinery to read from
      pipes.
      * wrap/python/tests/piperead.ipynb: New file.
      * wrap/python/tests/Makefile.am: Add it.
      * wrap/python/tests/run.in: Setup PATH.
      961d005b
  8. 27 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      python: add a spot.automata(filename) interface, yielding automata · 25de479e
      Alexandre Duret-Lutz authored
      * src/hoaparse/fmterror.cc, src/hoaparse/public.hh,
      src/hoaparse/hoaparse.yy (hoa_stream_parser::parse_strict): New method
      that raises an exception whenever a syntax error is encountered.
      * src/ltlparse/public.hh (parse_error): Move ...
      * src/misc/common.hh: ... here.
      * wrap/python/spot_impl.i: Wrap the hoa output.
      * wrap/python/spot.py: Implement spot.automata.
      * wrap/python/tests/automata-io.ipynb: New test.
      * wrap/python/tests/Makefile.am: Add it.
      25de479e
  9. 26 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      org: uses nice dot arrows · 8e6b35e5
      Alexandre Duret-Lutz authored
      Suggested by Akim Demaille.  Fixes #69.
      
      * doc/org/.dir-locals.el, doc/org/init.el.in,
      wrap/python/tests/automata.ipynb: Set arrowhead and arrowsize.
      * doc/org/autfilt.org, doc/org/dstar2tgba.org,
      doc/org/ltl2tgba.org, doc/org/oaut.org: Adjust.
      8e6b35e5
  10. 24 Mar, 2015 1 commit
  11. 21 Mar, 2015 1 commit
  12. 20 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      Do not store getenv() pointers in static variables. · 125fa983
      Alexandre Duret-Lutz authored
      ... or the pointer might be invalidated if the environments
      changes.  Fixes #63.
      
      * src/taalgos/dotty.cc, src/tgbaalgos/dotty.cc,
      src/tgbaalgos/dtbasat.cc, src/tgbaalgos/dtgbasat.cc:
      Copy the environment in strings instead.
      * wrap/python/tests/automata.ipynb: Adjust comment.
      125fa983
  13. 18 Mar, 2015 1 commit
  14. 17 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      dotty: colored acceptance sets · 838bfb2a
      Alexandre Duret-Lutz authored
      This implement several new options for --dot in order to
      allow emptiness sets to be output as colored ⓿ or ❶...
      Also add a SPOT_DOTDEFAULT environment variable.
      
      * NEWS, src/bin/man/spot-x.x, src/bin/common_aoutput.cc,
      src/bin/dstar2tgba.cc: Document the new options.
      * doc/org/.dir-locals.el, doc/org/init.el.in: Setup
      SPOT_DOTEXTRA and SPOT_DOTDEFAULT for all documents.
      * doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org,
      doc/org/ltldo.org, doc/org/oaut.org, doc/org/randaut.org,
      doc/org/satmin.org: Adjust to this new setup.
      * src/misc/escape.cc, src/misc/escape.hh (escape_html): New function.
      * src/tgba/acc.cc, src/tgba/acc.hh (to_text, to_html): New method.
      * src/tgbaalgos/dotty.cc: Implement the new options.
      * src/tgbatest/readsave.test, wrap/python/tests/automata.ipynb: More
      tests.
      * wrap/python/spot.py: Make sure the default argument for
      dotty_reachable is None, so that SPOT_DOTDEFAULT is honored.
      838bfb2a
  15. 16 Mar, 2015 3 commits
  16. 15 Mar, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      python: some bindings for translating formulas and diplaying automata · 3c38780d
      Alexandre Duret-Lutz authored
      * wrap/python/spot.py: Introduce spot.translate (and
      spot.formula.translate) as well, as a wrapper around the
      spot.translator class.  Also implement spot.tgba.show()
      to allow passing argument to dotty_reachable() before
      the result is converted to SVG.
      * wrap/python/tests/automata.ipynb: New test file.
      * wrap/python/tests/Makefile.am: Add it.
      3c38780d
  17. 13 Mar, 2015 1 commit
  18. 11 Mar, 2015 3 commits
  19. 08 Mar, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
    • Thibaud Michaud's avatar
      Adding python functions to mirror the functionalities found in src/bin · 3bf3d2c8
      Thibaud Michaud authored
      * wrap/python/spot.i: Rename to...
      * wrap/python/spot_impl.i: ...this, and import spot_impl from spot.py so
      that it is not needed to recompile everything when modifying python
      code.
      * wrap/python/spot.py: Adding python functions to mirror the
      functionalities found in src/bin.
      * src/bin/common_r.cc: Move simplification level...
      * src/ltlvisit/simplify.hh: ... here as a constructor of
      ltl_simplifier_options, to make it available in wrap/python.
      * src/bin/ltlfilt.cc: Set simplification level using the new
      ltl_simplifier_options constructor.
      * src/bin/randltl.cc: Move most of the code...
      * src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: ... here, as a
      class named randltlgenerator.
      * wrap/python/tests/bddnqueen.py, wrap/python/tests/minato.py: Avoid
      calling bdd_init twice by moving 'import spot' after bdd initialization.
      * wrap/python/Makefile.am: Rename spot to spot_impl
      * wrap/python/tests/Makefile.am: Add ipnbdoctest.py.
      * wrap/python/.gitignore: Rename spot.py to spot_impl.py
      * src/ltlvisit/tostring.cc: \ttrue and \ffalse should be \top and \bot.
      * wrap/python/tests/ipnbdoctest.py: Run code cells of a python notebook
      and compare the output to the actual content of the notebook.
      * wrap/python/tests/randltl.ipynb: Document and test randltl.
      * wrap/python/tests/run.in: Call ipnbdoctest.py to run ipython
      notebooks.
      3bf3d2c8
  20. 31 Jan, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      save: remove · dbd824c5
      Alexandre Duret-Lutz authored
      Get rid of the output in Spot's format.
      
      This finally fixes #1.
      
      * src/tgbaalgos/save.cc, src/tgbaalgos/save.hh: Delete.
      * src/tgbaalgos/Makefile.am: Adjust.
      * src/ltlvisit/contain.cc: Remove useless includes.
      * src/bin/dstar2tgba.cc, src/bin/common_aoutput.cc,
      src/bin/common_aoutput.hh: Remove the "Spot" output.
      * doc/org/dstar2tgba.org, doc/org/ioltl.org,
      doc/org/ltl2tgba.org, doc/org/oaut.org: Update doc.
      * NEWS: Mention that Spot i/o is gone.
      * src/tgbatest/randtgba.cc: Output in HOA.
      * src/tgbatest/randtgba.test: Use randaut instead of
      randtgba.
      * wrap/python/spot.i: Do not provide binding for save.hh
      dbd824c5
  21. 27 Jan, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      python: use hoa_parse instead of tgba_parse · 44f98219
      Alexandre Duret-Lutz authored
      * src/hoaparse/public.hh: Cope with SWIG.
      * wrap/python/spot.i: Bind hoa_parse instead of tgba_parse.
      Remove the binding for tgba_parse because it will be removed
      soon from Spot (cf. #1).
      * wrap/python/ajax/spot.in: Use the HOA output of ltl3ba.
      * wrap/python/tests/parsetgba.py: Adjust test case.
      44f98219
  22. 25 Jan, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      update to ltl3ba 1.1.1 · 25af8e7e
      Alexandre Duret-Lutz authored
      Compared to 1.1.0, -L/-M have been renamed to -M0,-M1.
      
      * bench/ltl2tgba/tools, bench/spin13/README,
      bench/spin13/run.sh, doc/org/ltlcross.org,
      wrap/python/ajax/spot.in: Adjust all references.
      25af8e7e
  23. 24 Jan, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      dotty: get rid of the decorated version · 49701ca3
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh,
      src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: Delete.
      * src/tgbaalgos/Makefile.am, wrap/python/spot.i: Adjust.
      * src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: Remove the
      decorated version, and the related arguments.
      * src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/complementation.cc,
      src/tgbatest/emptchk.cc: Adjust calls.
      * wrap/python/ajax/spot.in: Draw the accepting run as an
      automaton instead of painting it.
      * wrap/python/ajax/ltl2tgba.html: Update help text.
      49701ca3
  24. 23 Jan, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      ltl2tgba.html: Adjust for ltl3ba 1.1.0 · a4b6faba
      Alexandre Duret-Lutz authored
      ltl3ba 1.1.0 was released today
      
      * wrap/python/ajax/spot.in: Use -T3 instead of -U.
      * wrap/python/ajax/README: Adjust version.
      * wrap/python/ajax/ltl2tgba.html: Turn on improved determinism
      of ltl3ba by default.
      * bench/ltl2tgba/tools, bench/spin13/run.sh: Adjust options.
      * bench/spin13/README: Mention the update.
      a4b6faba
  25. 19 Jan, 2015 1 commit
  26. 08 Jan, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      stutter: gather all code in one place · bb9b204d
      Alexandre Duret-Lutz authored
      * src/tgba/tgbasl.cc, src/tgba/tgbasl.hh, src/tgbaalgos/closure.cc,
      src/tgbaalgos/closure.hh, src/tgbaalgos/stutter_invariance.cc,
      src/tgbaalgos/stutter_invariance.hh, src/tgbaalgos/stutterize.cc,
      src/tgbaalgos/stutterize.hh: Delete these files, and merge their
      contents into...
      * src/tgbaalgos/stutter.cc, src/tgbaalgos/stutter.hh: ... these two.
      * src/tgba/Makefile.am, src/tgbaalgos/Makefile.am: Adjust.
      * wrap/python/spot.i: Adjust.
      bb9b204d
  27. 03 Jan, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      tgba_digraph: force selection of properties kept on copy · 87c2b291
      Alexandre Duret-Lutz authored
      * src/tgba/tgba.hh: Declare a prop_set to specify the types.
      * src/tgba/tgbagraph.hh: Use prop_set for all copy constructors.
      * iface/ltsmin/ltsmin.cc, src/bin/autfilt.cc, src/bin/randaut.cc,
      src/tgbaalgos/are_isomorphic.cc, src/tgbaalgos/closure.cc,
      src/tgbaalgos/complete.cc, src/tgbaalgos/degen.cc,
      src/tgbaalgos/dotty.cc, src/tgbaalgos/dtgbacomp.cc,
      src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh,
      src/tgbaalgos/sccfilter.cc, src/tgbaalgos/simulation.cc,
      src/tgbaalgos/stutterize.cc, src/tgbatest/checkpsl.cc,
      src/tgbatest/emptchk.cc, src/tgbatest/ltl2tgba.cc,
      wrap/python/spot.i,src/graphtest/tgbagraph.test: Adjust all uses.
      87c2b291
    • Alexandre Duret-Lutz's avatar
      dotty: switch to horizontal output and add options · 0f178288
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: Add an options
      parameter.
      * src/bin/randaut.cc, src/bin/autfilt.cc, src/bin/dstar2tgba.cc,
      src/bin/ltl2tgba.cc, wrap/python/ajax/spot.in: Use it.
      * src/tgbatest/det.test, src/tgbatest/dstar.test,
      src/tgbatest/ltl2tgba.cc, src/tgbatest/monitor.test,
      src/tgbatest/neverclaimread.test, src/tgbatest/tgbaread.test,
      src/graphtest/tgbagraph.test: Adjust
      because automata are now output horizontally.
      * NEWS: Mention the change.
      0f178288
  28. 27 Nov, 2014 1 commit
  29. 14 Nov, 2014 1 commit
    • Thibaud Michaud's avatar
      Adding tgba-based stutter-invariance checking · 37bcb5d9
      Thibaud Michaud authored
      * src/tgbaalgos/closure.cc, src/tgbaalgos/closure.hh:
      Add closure function.
      * src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh:
      Add two implementations of "self-loopize" function.
      * src/tgbaalgos/Makefile.am: Add them.
      * src/tgba/tgbasl.cc, src/tgba/tgbasl.hh: On-the-fly implementation of
      self-loopize.
      * src/tgba/Makefile.am: Add it.
      * src/tgbatest/ltl2tgba.cc, src/tgbatest/stutter_invariant.test: Test
      closure and sl.
      * src/tgbatest/Makefile.am: Adjust.
      * src/bin/ltlfilt.cc: Modify stutter-invariant option to use
      automaton-based checking rather than syntactic-based checking.
      * src/ltlvisit/remove_x.cc, src/ltlvisit/remove_x.hh:
      Remove is_stutter_insensitive function.
      * src/tgbaalgos/stutter_invariance.cc,
      src/tgbaalgos/stutter_invariance.hh: Check if a formula is
      stutter-invariant using closure and sl.
      * wrap/python/spot.i: Add closure and sl bindings.
      * bench/stutter/stutter_invariance_formulas.cc: Generate benchmarks from
      given formulas.
      * bench/stutter/stutter_invariance_randomgraph.cc: Generate benchmarks
      from random automata.
      * bench/stutter/Makefile.am: Add them.
      * configure.ac: Add bench/stutter/Makefile.
      * bench/Makefile.am: Add stutter subdirectory.
      * README: Document bench/stutter directory.
      37bcb5d9
  30. 30 Oct, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      buddy: rename libbdd to libbddx · ad8d2422
      Alexandre Duret-Lutz authored
      * buddy/src/bdd.h, buddy/src/bvec.h, buddy/src/fdd.h: Rename as...
      * buddy/src/bddx.h, buddy/src/bvecx.h, buddy/src/fddx.h: ... these.
      * buddy/src/Makefile.am: Build libbddx.la instead of libbdd.la.
      * buddy/examples/Makefile.def: Use it.
      * Makefile.am, buddy/src/bddtest.cxx, buddy/src/bvec.c,
      buddy/src/cppext.cxx, buddy/src/fdd.c, buddy/src/imatrix.h,
      buddy/src/kernel.h, buddy/examples/adder/adder.cxx,
      buddy/examples/bddcalc/parser_.h, buddy/examples/bddtest/bddtest.cxx,
      buddy/examples/cmilner/cmilner.c, buddy/examples/fdd/fdd.cxx,
      buddy/examples/milner/milner.cxx, buddy/examples/money/money.cxx,
      buddy/examples/queen/queen.cxx, buddy/examples/solitare/solitare.cxx,
      m4/buddy.m4, src/ltlvisit/apcollect.hh, src/ltlvisit/simplify.hh,
      src/misc/bddlt.hh, src/misc/bddop.hh, src/misc/minato.hh,
      src/priv/acccompl.hh, src/priv/accconv.hh, src/priv/accmap.hh,
      src/priv/bddalloc.cc, src/tgba/bdddict.hh, src/tgba/bddprint.hh,
      src/tgba/tgbamask.hh, src/tgba/tgbasafracomplement.cc,
      src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/sccstack.hh,
      src/tgbaalgos/neverclaim.cc, src/tgbaalgos/powerset.cc,
      src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccinfo.hh,
      src/tgbaalgos/weight.hh, wrap/python/buddy.i: Adjust.
      * NEWS, README: Document it.
      ad8d2422