1. 30 Apr, 2012 3 commits
    • Alexandre Duret-Lutz's avatar
      Prefer -R3 to -R3f when applying direct simulation in the web interface. · 861969b5
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/spot.in: Adjust.
    • Alexandre Duret-Lutz's avatar
      Implement W,M removal for Spin output. · a09ad6b4
      Alexandre Duret-Lutz authored
      * src/ltlvisit/wmunabbrev.hh, src/ltlvisit/wmunabbrev.cc: New files.
      * src/ltlvisit/Makefile.am: Add them.
      * src/ltlvisit/tostring.cc (to_spin_string): Use the new rewriting.
      * wrap/python/ajax/spot.in: Warn when a "Spin" still contain PSL
      * wrap/python/ajax/ltl2tgba.html: Adjust help text.
      * doc/tl/tl.tex, NEWS: Document the new rewriting.
    • Alexandre Duret-Lutz's avatar
      Add an UTF-8 option to the web interface. · 43d1be09
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/ltl2tgba.html: Add the checkbox.
      * wrap/python/ajax/css/ltl2tgba.css: Add the necessary class.
      * wrap/python/ajax/protocol.txt: Add the new option.
      * wrap/python/ajax/spot.in: Handle it.
      * wrap/python/ajax/README: Add a few lines to explain
      how to run the CGI script from the command line for debugging.
  2. 28 Apr, 2012 5 commits
    • Alexandre Duret-Lutz's avatar
      web ltl2tgba: add an option to disable larger rewritings · bdeb87a6
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/ltl2tgba.html: Add a checkbox and some
      code to keep it consistent with the basic rewriting checkbox.
      * wrap/python/ajax/spot.in: Deal with the new option.
      * wrap/python/ajax/protocol.txt: Document it.
    • Alexandre Duret-Lutz's avatar
      ltl2tgba.html: Display properties of formulas. · 3d41bf9f
      Alexandre Duret-Lutz authored
      * src/ltlast/formula.hh, src/ltlast/formula.cc (list_formula_props):
      New function.
      * wrap/python/spot.i: Adjust to wrap list_formula_props.
      * wrap/python/ajax/ltl2tgba.html: Add option to display properties.
      * wrap/python/ajax/spot.in: Handle ff=p and display properties.
      * wrap/python/ajax/protocol.txt: Adjust.
    • Alexandre Duret-Lutz's avatar
      ltl2tgba.html: Provide a link to an SVG output. Suggested by Denis. · 5ce59c01
      Alexandre Duret-Lutz authored
      Because this means we are running dot twice, I have added a flag that
      will allow us to easily turn this off, should it prove too slow.
      * wrap/python/ajax/spot.in (output_both): New variable.
      (run_dot): New function, extracted from ...
      (render_dot): ... here.  Adjust to call run_dot for all needed format.
      And ajust the output accordingly.
    • Alexandre Duret-Lutz's avatar
      Make sure PSL formulae are translated with the FM translation online. · 3d183d68
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/spot.in: Diagnose attempt to use LaCIM or Tau
      on PSL formulae.
      * wrap/python/ajax/css/ltl2tgba.css (.ltl2tgba .error): New entry.
    • Alexandre Duret-Lutz's avatar
      Deprecate reduce() in favor of ltl_simplifier. · 67f4e8b5
      Alexandre Duret-Lutz authored
      * src/ltlvisit/reduce.hh: Mark the file as obsolete.
      (reduce): Declare this function as obsolete.
      * src/ltlvisit/reduce.cc: Define SKIP_DEPRECATED_WARNING
      so we can include reduce.hh.
      * src/sanity/includes.test: Also use SKIP_DEPRECATED_WARNING
      when compiling headers.
      * iface/dve2/dve2check.cc,
      src/ltltest/equals.cc, src/ltltest/randltl.cc,
      src/ltltest/reduc.cc, src/tgbaalgos/ltl2tgba_fm.hh,
      src/tgbaalgos/ltl2tgba_fm.cc, src/tgbatest/randtgba.cc,
      wrap/python/ajax/spot.in, wrap/python/spot.i: Adjust
      to use ltl_simplifier.
      * src/tgbatest/ltl2tgba.cc: Adjust to use ltl_simplifier,
      and replace -fr1...-fr7 options by a single -fr option.
      * src/tgbatest/spotlbtt.test: Adjust -fr flags accordingly.
      * src/tgbatest/reductgba.cc: Do not include reduce.hh.
  3. 27 Apr, 2012 1 commit
  4. 18 Apr, 2012 1 commit
    • Thomas Badie's avatar
      Add the simulation in the Spot web interface. · dfcaed03
      Thomas Badie authored
      * wrap/python/ajax/spot.in: Add the simulation.
      * wrap/python/ajax/protocol.txt: Add the direct simulation in the
      automaton simplifications section.
      * wrap/python/spot.i (simulation_new): Create a function which
      takes an automaton and a call to the simulation with the good
      template parameter.
      * wrap/python/ajax/ltl2tgba.html: Add the direct simulation
  5. 08 Mar, 2012 1 commit
  6. 04 Mar, 2012 1 commit
  7. 25 Feb, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Make all python code compatible with Python 2.x and Python 3.x. · 61127a3f
      Alexandre Duret-Lutz authored
      * wrap/python/buddy.i (__le__, __lt__, __eq__, __ne__, __ge__
      __gt__): New operators for bdd.
      * wrap/python/spot.i (__le__, __lt__, __eq__, __ne__, __ge__
      __gt__, __hash__): New operators for formula.
      (nl_cout, nl_cerr): New functions.
      * wrap/python/tests/bddnqueen.py,
      wrap/python/tests/interdep.py, wrap/python/tests/ltl2tgba.py,
      wrap/python/tests/ltlparse.py, wrap/python/tests/ltlsimple.py,
      wrap/python/tests/minato.py, wrap/python/tests/modgray.py: Adjust
      to the new print syntax by using sys.output.write() or nl_cout()
      * wrap/python/tests/optionmap.py: Remove all print calls.
      * wrap/python/ajax/spot.in: Massive adjustments in order to work
      with both Python 2 and 3.  In python 3, reopening stdout as
      unbuffered requires it to be open as binary, which in turns
      requires any string output to be encoded manually.  BaseHTTPServer
      and CGIHTTPServer have been merged into http.server, so we have
      to try two different import syntaxes.  execfile no longer exists,
      so it has to be emulated.
      This also fixes two bugs where the script would segfault on
      empty input, or when calling Tau03 on automata with less then
      one acceptance conditions.
  8. 15 Feb, 2012 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix a race condition on the CGI script. · 62914059
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/spot.in: Create all cache files in a temporary
      directory, and only rename this directory at the end.  This way if
      two processes are processing the same request, they won't attempt
      to populate the same directory (and only one of the first of two
      renames will succeed, but that is OK).
  9. 17 Jan, 2012 1 commit
  10. 01 Dec, 2011 1 commit
  11. 10 Jun, 2011 1 commit
  12. 08 Jun, 2011 4 commits
    • Alexandre Duret-Lutz's avatar
      Implement cache pruning in the CGI script. · 3216494c
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/spot.in (finish): Prune the cache once in a
      while.  We rely on hardlinks for garbage collecting the pictures
      and dot sources that may be shared by different requests.
    • Alexandre Duret-Lutz's avatar
      Cache dot sources in the CGI script. · 155ba42c
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/spot.in (render_dot, render_dot_maybe)
      (render_automaton, render_formula): Cache the dot source, so that
      we do not have to regenerate two pictures from the same contents.
      * wrap/python/spot.i: Typo in the ostringstream declaration.
    • Alexandre Duret-Lutz's avatar
      Output a "Cache-Control:" header in the CGI script. · 0d2ac81a
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/spot.in: Output a cache-control header, so that
      browsers do no even send two identical requests.
    • Alexandre Duret-Lutz's avatar
      Cache results of the spot.py CGI script. · b8f84411
      Alexandre Duret-Lutz authored
      * wrap/python/ajax/spot.in: Use the QUERY_STRING as a hash key to
      cache the result of the script.  Open stdout without buffering and
      redirect it to a file that we can dump later on cache hits.  Parts
      of this change are extracted from code from Pierre Parutto
      * AUTHORS: Add him.
  13. 05 Mar, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Using double borders for acceptance states in SBAs. · e1ef47d9
      Alexandre Duret-Lutz authored
      * src/tgbaalgos/dotty.hh (dotty_reachable): Take a new
      assume_sba argument.
      * src/tgbaalgos/dotty.cc (dotty_bfs): Take a new
      mark_accepting_states arguments.
      (dotty_bfs::process_state): Check if a state is accepting using
      the state_is_accepting() method for tgba_sba_proxies, or by
      looking at the first outgoing transition of the state.  Pass
      the result to the dectorator.
      (dotty_reachable): Adjust function.
      * src/tgbaalgos/dottydec.hh, src/tgbaalgos/dottydec.cc,
      src/tgbaalgos/rundotdec.hh, src/tgbaalgos/rundotdec.cc
      (state_decl): Add an "accepting" argument, and use it to
      decorate accepting states with a double border.
      * src/tgbatest/ltl2tgba.cc: Keep track of whether the output
      is an SBA or not, so that we can tell it to dotty().
      * wrap/python/ajax/spot.in: Likewise.
      * wrap/python/cgi-bin/ltl2tgba.in: Likewise.
  14. 04 Mar, 2011 1 commit
  15. 05 Feb, 2011 1 commit
  16. 18 Jan, 2011 1 commit
    • Alexandre Duret-Lutz's avatar
      Preliminary implementation of an ajax-based ltl2tgba translator. · 34f49a86
      Alexandre Duret-Lutz authored
      * configure.ac: Output wrap/python/ajax/Makefile.
      * wrap/python/Makefile.am (SUBDIRS): Add ajax.
      * wrap/python/ajax/Makefile.am, wrap/python/ajax/README,
      wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/spot.in: New files.
      * wrap/python/ajax/css/, wrap/python/ajax/js,
      wrap/python/ajax/logos: New directories.
      * README: Document wrap/python/ajax/.