Commit graph

8 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
3216494cf6 Implement cache pruning in the CGI script.
* 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.
2011-06-08 16:44:52 +02:00
Alexandre Duret-Lutz
155ba42c90 Cache dot sources in the CGI script.
* 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.
2011-06-08 16:44:52 +02:00
Alexandre Duret-Lutz
0d2ac81a8c Output a "Cache-Control:" header in the CGI script.
* wrap/python/ajax/spot.in: Output a cache-control header, so that
browsers do no even send two identical requests.
2011-06-08 16:44:47 +02:00
Alexandre Duret-Lutz
b8f8441167 Cache results of the spot.py CGI script.
* 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
<parutto@lrde.epita.fr>.
* AUTHORS: Add him.
2011-06-08 11:36:45 +02:00
Alexandre Duret-Lutz
e1ef47d975 Using double borders for acceptance states in SBAs.
* 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.
2011-03-05 10:26:20 +01:00
Alexandre Duret-Lutz
0792fb741d * wrap/python/ajax/spot.in: Use the degeneralized automaton if
available while computing the emptiness check.
2011-03-04 21:04:38 +01:00
Alexandre Duret-Lutz
97df5b4285 Fix call to scc_filter in the CGI script.
* wrap/python/ajax/spot.in: Do full scc_filter for TGBA (-R3f),
and keep some extra acceptance conditions (-R3) when
degeneralizing.  The converse was done.
2011-02-05 14:27:04 +01:00
Alexandre Duret-Lutz
34f49a8692 Preliminary implementation of an ajax-based ltl2tgba translator.
* 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/.
2011-01-18 16:31:33 +01:00