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.
This commit is contained in:
parent
b535741a90
commit
b8f8441167
3 changed files with 67 additions and 21 deletions
1
AUTHORS
1
AUTHORS
|
|
@ -8,3 +8,4 @@ Thomas Martinez
|
||||||
Damien Lefortier
|
Damien Lefortier
|
||||||
Guillaume Sadegh
|
Guillaume Sadegh
|
||||||
Félix Abecassis
|
Félix Abecassis
|
||||||
|
Pierre Parutto
|
||||||
|
|
|
||||||
11
ChangeLog
11
ChangeLog
|
|
@ -1,3 +1,14 @@
|
||||||
|
2011-06-08 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
|
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-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
2011-06-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||||
|
|
||||||
* src/ltltest/genltl.cc (X_n): Fix assertion.
|
* src/ltltest/genltl.cc (X_n): Fix assertion.
|
||||||
|
|
|
||||||
|
|
@ -22,9 +22,35 @@
|
||||||
|
|
||||||
import os
|
import os
|
||||||
|
|
||||||
|
script = os.environ.has_key('SCRIPT_NAME')
|
||||||
|
|
||||||
|
if script:
|
||||||
|
print "Content-Type: text/html"
|
||||||
|
print
|
||||||
|
|
||||||
# Directory for temporary files (images and other auxiliary files).
|
# Directory for temporary files (images and other auxiliary files).
|
||||||
imgdir = 'spotimg'
|
imgdir = 'spotimg'
|
||||||
|
|
||||||
|
# Cache lookup for the QUERY_STRING
|
||||||
|
qs = os.getenv('QUERY_STRING')
|
||||||
|
if qs:
|
||||||
|
import hashlib
|
||||||
|
# We (optimistically) assume no collision from sha1(qs)
|
||||||
|
imgprefix = imgdir + '/' + hashlib.sha1(qs).hexdigest()
|
||||||
|
cachename = imgprefix + '.html'
|
||||||
|
try:
|
||||||
|
# Is this a request we have already processed?
|
||||||
|
cache = open(cachename, "r", 0)
|
||||||
|
print cache.read()
|
||||||
|
exit(0)
|
||||||
|
except IOError:
|
||||||
|
# We failed to open the file.
|
||||||
|
# Let's run the rest of the script to create it.
|
||||||
|
pass
|
||||||
|
elif script:
|
||||||
|
print "<b>QUERY_STRING unset!</b>"
|
||||||
|
exit(0)
|
||||||
|
|
||||||
# Location of the dot command
|
# Location of the dot command
|
||||||
dot = '@DOT@'
|
dot = '@DOT@'
|
||||||
dot_bgcolor = '-Gbgcolor=#FFFFFF00'
|
dot_bgcolor = '-Gbgcolor=#FFFFFF00'
|
||||||
|
|
@ -42,7 +68,7 @@ class MyHandler(CGIHTTPRequestHandler):
|
||||||
return True
|
return True
|
||||||
return False
|
return False
|
||||||
|
|
||||||
if not os.environ.has_key('SCRIPT_NAME'):
|
if not script:
|
||||||
# If this is not run as a cgi script, let's start an HTTP server.
|
# If this is not run as a cgi script, let's start an HTTP server.
|
||||||
from BaseHTTPServer import HTTPServer
|
from BaseHTTPServer import HTTPServer
|
||||||
server_address=('',8000)
|
server_address=('',8000)
|
||||||
|
|
@ -57,15 +83,30 @@ import sys
|
||||||
import cgi
|
import cgi
|
||||||
import cgitb; cgitb.enable()
|
import cgitb; cgitb.enable()
|
||||||
import signal
|
import signal
|
||||||
import uuid
|
|
||||||
|
|
||||||
print "Content-Type: text/html"
|
sys.stdout.flush()
|
||||||
print
|
# Reopen stdout without buffering
|
||||||
|
sys.stdout = os.fdopen(sys.stdout.fileno(), "w", 0)
|
||||||
|
|
||||||
# Redirect stderr to stdout.
|
# Redirect stderr to stdout at a low-level (so that
|
||||||
os.close(sys.stderr.fileno())
|
# even errors from subprocesses get printed).
|
||||||
os.dup2(sys.stdout.fileno(), sys.stderr.fileno())
|
os.dup2(sys.stdout.fileno(), sys.stderr.fileno())
|
||||||
|
|
||||||
|
# Redirect stdout to the cache file, at a low-level
|
||||||
|
# for similar reason.
|
||||||
|
fd = os.open(cachename, os.O_CREAT | os.O_WRONLY, 0644)
|
||||||
|
os.dup2(fd, sys.stdout.fileno())
|
||||||
|
|
||||||
|
def finish(kill = False):
|
||||||
|
# Output the result and exit.
|
||||||
|
os.dup2(sys.stderr.fileno(), sys.stdout.fileno())
|
||||||
|
cache = open(cachename, "r", 0)
|
||||||
|
print cache.read()
|
||||||
|
if kill:
|
||||||
|
os.kill(0, signal.SIGTERM)
|
||||||
|
exit(0)
|
||||||
|
|
||||||
|
|
||||||
# Assume Spot is installed
|
# Assume Spot is installed
|
||||||
sys.path.insert(0, '@pythondir@')
|
sys.path.insert(0, '@pythondir@')
|
||||||
|
|
||||||
|
|
@ -99,8 +140,7 @@ it has been running for too long.</font> Please try a shorter formula,
|
||||||
or different options (not drawing automata usually helps).
|
or different options (not drawing automata usually helps).
|
||||||
If you want to benchmark big formulae it is
|
If you want to benchmark big formulae it is
|
||||||
better to install Spot on your own computer.</p>"""
|
better to install Spot on your own computer.</p>"""
|
||||||
sys.stdout.flush()
|
finish(kill = True)
|
||||||
os.kill(0, signal.SIGTERM)
|
|
||||||
|
|
||||||
def reset_alarm():
|
def reset_alarm():
|
||||||
signal.alarm(30)
|
signal.alarm(30)
|
||||||
|
|
@ -122,7 +162,6 @@ def render_dot(basename):
|
||||||
print ('<img src="' + b + '.png"><br>(<a href="' + b
|
print ('<img src="' + b + '.png"><br>(<a href="' + b
|
||||||
+ '.txt">dot source</a>)')
|
+ '.txt">dot source</a>)')
|
||||||
print '</div>'
|
print '</div>'
|
||||||
sys.stdout.flush()
|
|
||||||
|
|
||||||
def render_automaton(basename, automata, dont_run_dot, issba, deco = False):
|
def render_automaton(basename, automata, dont_run_dot, issba, deco = False):
|
||||||
outfile = spot.ofstream(basename + '.txt')
|
outfile = spot.ofstream(basename + '.txt')
|
||||||
|
|
@ -159,13 +198,11 @@ def print_stats(automaton):
|
||||||
print "acceptance condition:",
|
print "acceptance condition:",
|
||||||
else:
|
else:
|
||||||
print "acceptance conditions:",
|
print "acceptance conditions:",
|
||||||
sys.stdout.flush()
|
|
||||||
acc = automaton.all_acceptance_conditions()
|
acc = automaton.all_acceptance_conditions()
|
||||||
spot.bdd_print_accset(spot.get_cout(), automaton.get_dict(), acc)
|
print spot.bdd_format_accset(automaton.get_dict(), acc)
|
||||||
else:
|
else:
|
||||||
print "no acceptance condition (all cycles are accepting)"
|
print "no acceptance condition (all cycles are accepting)"
|
||||||
print "</p>"
|
print "</p>"
|
||||||
sys.stdout.flush()
|
|
||||||
# Decide whether we will render the automaton or not.
|
# Decide whether we will render the automaton or not.
|
||||||
# (A webserver is not a calcul center...)
|
# (A webserver is not a calcul center...)
|
||||||
if stats.states > 64:
|
if stats.states > 64:
|
||||||
|
|
@ -175,16 +212,13 @@ def print_stats(automaton):
|
||||||
return False
|
return False
|
||||||
|
|
||||||
form = cgi.FieldStorage()
|
form = cgi.FieldStorage()
|
||||||
uid = str(uuid.uuid1())
|
|
||||||
imgprefix = imgdir + '/' + uid
|
|
||||||
|
|
||||||
|
|
||||||
output_type = form.getfirst('o', 'v');
|
output_type = form.getfirst('o', 'v');
|
||||||
|
|
||||||
# Version requested.
|
# Version requested.
|
||||||
if output_type == 'v':
|
if output_type == 'v':
|
||||||
print 'Spot version ' + spot.version()
|
print 'Spot version ' + spot.version()
|
||||||
exit(0)
|
finish()
|
||||||
|
|
||||||
spot.unblock_signal(signal.SIGALRM)
|
spot.unblock_signal(signal.SIGALRM)
|
||||||
spot.unblock_signal(signal.SIGTERM)
|
spot.unblock_signal(signal.SIGTERM)
|
||||||
|
|
@ -234,7 +268,7 @@ if output_type == 'f':
|
||||||
spot.dotty(outfile, f)
|
spot.dotty(outfile, f)
|
||||||
del outfile
|
del outfile
|
||||||
render_dot(imgprefix + '-f')
|
render_dot(imgprefix + '-f')
|
||||||
exit(0)
|
finish()
|
||||||
|
|
||||||
# Formula translation.
|
# Formula translation.
|
||||||
translator = form.getfirst('t', 'fm')
|
translator = form.getfirst('t', 'fm')
|
||||||
|
|
@ -280,7 +314,7 @@ if output_type == 'm':
|
||||||
print '</div>'
|
print '</div>'
|
||||||
render_automaton(imgprefix + '-a', automaton, dont_run_dot, issba)
|
render_automaton(imgprefix + '-a', automaton, dont_run_dot, issba)
|
||||||
automaton = 0
|
automaton = 0
|
||||||
exit(0)
|
finish()
|
||||||
|
|
||||||
# Automaton simplifications
|
# Automaton simplifications
|
||||||
prune_scc = False
|
prune_scc = False
|
||||||
|
|
@ -298,7 +332,7 @@ elif output_type == 'r':
|
||||||
else:
|
else:
|
||||||
print "Unkown output type 'o=%s'." % output_type
|
print "Unkown output type 'o=%s'." % output_type
|
||||||
automaton = 0
|
automaton = 0
|
||||||
exit(0)
|
finish()
|
||||||
|
|
||||||
degen = False
|
degen = False
|
||||||
neverclaim = False
|
neverclaim = False
|
||||||
|
|
@ -340,7 +374,7 @@ if output_type == 'a':
|
||||||
render_automaton(imgprefix + '-a', degen, dont_run_dot, issba)
|
render_automaton(imgprefix + '-a', degen, dont_run_dot, issba)
|
||||||
degen = 0
|
degen = 0
|
||||||
automaton = 0
|
automaton = 0
|
||||||
exit(0)
|
finish()
|
||||||
|
|
||||||
# Buchi Run Output
|
# Buchi Run Output
|
||||||
if output_type == 'r':
|
if output_type == 'r':
|
||||||
|
|
@ -406,4 +440,4 @@ if output_type == 'r':
|
||||||
del ec_a
|
del ec_a
|
||||||
degen = 0
|
degen = 0
|
||||||
automaton = 0
|
automaton = 0
|
||||||
exit(0)
|
finish()
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue