alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/wrap/python/ajax/spot.in
Alexandre Duret-Lutz 81d3ee48f0 ltl2tgba.html: Display a loading logo for delayed results. 
* wrap/python/ajax/css/loading.gif: New file.
* wrap/python/ajax/css/ltl2tgba.css (.loading): New class.
* wrap/python/ajax/ltl2tgba.html: Display loading.gif after 200ms if
the answer hasn't arrived
* wrap/python/ajax/spot.in: Do not suggest not to draw the automaton
on timeout.
* wrap/python/ajax/js/jquery.ba-dotimeout.min.js: New file.
* wrap/python/ajax/Makefile.am: Distribute it.
2012-06-19 21:55:08 +02:00

714 lines
24 KiB
Python
Executable file
Raw Blame History

#!@PYTHON@
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with Spot; see the file COPYING. If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.
import os
import sys
script = ('SCRIPT_NAME' in os.environ)
if script:
# 3600s = 1h
sys.stdout.write("""Cache-Control: max-age=3600
Content-Type: text/html
""")
# Directory for temporary files (images and other auxiliary files).
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)
cachedir = imgdir + '/' + hashlib.sha1(qs.encode('utf-8')).hexdigest()
cachename = cachedir + '/html'
try:
# Is this a request we have already processed?
cache = open(cachename, "rb", 0)
if hasattr(sys.stdout, 'buffer'):
# Python 3+
sys.stdout.buffer.write(cache.read())
else:
# Python 2.x
sys.stdout.write(cache.read())
# Touch the directory containing the files we used, so
# it that it survives the browser's cache.
os.utime(cachedir, None)
exit(0)
except IOError:
# We failed to open the file.
# Let's run the rest of the script to create it.
pass
elif script:
sys.stdout.write("<b>QUERY_STRING unset!</b>\n")
exit(0)
# Location of the dot command
dot = '@DOT@'
dot_bgcolor = '-Gbgcolor=#FFFFFF00'
svg_output = False # SVG output used to working well with Firefox
# only. It now seems to work with recent Chrome
# versions as well, but it is still a problem with
# Safari, and IE.
output_both = True # Create both PNG and SVG. If svg_output is False,
# the SVG will be given as a link under the PNG.
# Otherwise the PNG is used as alternate contents
# for the SVG object.
if not script:
# If this is not run as a cgi script, let's start an HTTP server.
try:
# Python 3+
from http.server import CGIHTTPRequestHandler, HTTPServer
except ImportError:
# Python 2.x
from CGIHTTPServer import CGIHTTPRequestHandler
from BaseHTTPServer import HTTPServer
class MyHandler(CGIHTTPRequestHandler):
def is_cgi(self):
if self.path.startswith('/cgi-bin/spot.py'):
self.cgi_info = '', self.path[9:]
return True
return False
server_address=('',8000)
if not os.access(imgdir, os.F_OK):
# 493 = 0755 but we would have to write 0755 or 0o755
# depending on the python version...
os.mkdir(imgdir, 493)
sys.stdout.write("Directory spotimg/ created.\n")
httpd = HTTPServer(server_address, MyHandler)
sys.stdout.write("Point your browser to http://localhost:8000/ltl2tgba.html\n")
httpd.serve_forever()
import cgi
import cgitb; cgitb.enable()
import signal
import time
import os.path
# We do not output in cachedir directely, in case two
# CGI scripts process the same request concurrently.
tmpdir = cachedir + '-' + str(os.getpid())
cachename = tmpdir + '/html'
sys.stdout.flush()
# Reopen stdout without buffering
sys.stdout = os.fdopen(sys.stdout.fileno(), "wb", 0)
# Redirect stderr to stdout at a low level (so that
# even errors from subprocesses get printed).
os.dup2(sys.stdout.fileno(), sys.stderr.fileno())
# Create the temporary cache directory
os.mkdir(tmpdir, 493) # See comment above about 0o755 or 0755.
# Redirect stdout to the cache file, at a low level
# for similar reason.
fd = os.open(cachename, os.O_CREAT | os.O_WRONLY, 420) # 420 = 0644
os.dup2(fd, sys.stdout.fileno())
# We had to reopen stdout in binary mode to enable unbuffered output,
# (disallowed on text I/O by Python 3.x) so starting now, we are not
# allowed to send strings to sys.stdout. Always use the following
# method instead.
def unbufprint(s):
if sys.getdefaultencoding() != 'ascii':
sys.stdout.write(s.encode("utf-8"))
else:
sys.stdout.write(s)
def finish(kill = False):
# Output the result and exit.
os.dup2(sys.stderr.fileno(), sys.stdout.fileno())
cache = open(cachename, "rb", 0)
sys.stdout.write(cache.read())
# Rename tmpdir to its permanent name for caching purpose.
# os.rename will fail if cachedir already exist. Since we tested
# that initially, it can only happen when two CGI script are
# processing the same request concurrently. In that case the
# other result is as good as ours, so we just ignore the error.
# (We don't bother removing the temporary directory -- it will be
# removed by the next cache prune and cannot be created again in
# the meantime.)
try:
os.rename(tmpdir, cachedir)
except OSError:
pass
if kill:
# Kill all children
os.kill(0, signal.SIGTERM)
# Should we prune the cache?
stamp = imgdir + '/cache.stamp'
now = time.time()
try:
# Prune at most once every hour
if now - os.path.getmtime(stamp) < 3600:
exit(0)
except OSError:
# It's OK if the file did not exist.
# We will create it.
pass
# Erase all directories that are older than 2 hours, and all
# files that have only one hardlinks. Files that have more than
# one hardlinks are referenced to by directories; so the hardlink
# count will decrease when the directory is purged.
os.system('find ' + imgdir + ' -mindepth 1 -maxdepth 1 -mmin +120 '
+ '\( -type d -o -links 1 \) -exec rm -rf {} +')
# Create or update the stamp so we know when to run the next prune.
open(stamp, "wb", 0)
exit(0)
# Assume Spot is installed
sys.path.insert(0, '@pythondir@')
if ('SERVER_SOFTWARE' in os.environ and
os.environ['SERVER_SOFTWARE'].startswith('SimpleHTTP')):
# We might be running from the build tree (but it's not sure).
# Add the build and source directories first in the search path.
# If we are not in the right place, python will find the installed
# libraries later.
sys.path.insert(0, '@srcdir@/../.libs')
sys.path.insert(0, '@srcdir@/..')
sys.path.insert(0, '../.libs')
sys.path.insert(0, '..')
# Darwin needs some help in figuring out where non-installed libtool
# libraries are (on this platform libtool encodes the expected final
# path of dependent libraries in each library).
m = '../.libs:@top_builddir@/src/.libs:@top_builddir@/buddy/src/.libs'
os.environ['DYLD_LIBRARY_PATH'] = m
try:
# execfile('ltl2tgba.opt') no longuer work with Python 3.
exec(compile(open("ltl2tgba.opt").read(), "ltl2tgba.opt", 'exec'))
except IOError:
pass
import spot
import buddy
def alarm_handler(signum, frame):
unbufprint("""<p><font color="red">The script was aborted because
it has been running for too long.</font> Please try a shorter formula,
or different options.
If you want to benchmark big formulae it is
better to install Spot on your own computer.</p>\n""")
finish(kill = True)
def run_dot(basename, ext):
outname = basename + '.' + ext
# Do not call "dot" to generate a file that already exists.
if not os.access(outname, os.F_OK):
os.spawnlp(os.P_WAIT, dot, dot, dot_bgcolor, '-T' + ext,
'-Gsize=8.2,8.2', '-o', outname, basename + '.txt')
# Create a unused hardlink that points to the output picture
# just to remember how many cache entries are sharing it.
os.link(outname, tmpdir + "/" + ext)
def render_dot(basename):
unbufprint('<div class="dot">')
b = cgi.escape(basename)
if svg_output or output_both:
run_dot(basename, 'svg')
if not svg_output or output_both:
run_dot(basename, 'png')
pngstr = '<img src="' + b + '.png">'
if svg_output:
unbufprint('<object type="image/svg+xml" data="' + b + '.svg">')
if output_both:
unbufprint(pngstr)
else:
unbufprint('Your browser does not support SVG.')
unbufprint('</object>' + '<br>(<a href="' + b
+ '.txt">dot</a>)')
else:
unbufprint('<img src="' + b + '.png"><br>(<a href="' + b
+ '.txt">dot</a>)')
if output_both:
unbufprint(' (<a href="' + b + '.svg">svg</a>)')
unbufprint('</div>\n')
def render_dot_maybe(dotsrc, dont_run_dot):
# The dot output is named after the SHA1 of the dot source.
# This way we can cache two different requests that generate
# the same automaton (e.g., when changing a simplification
# option that has no influence).
if sys.getdefaultencoding() != 'ascii':
dotsrc = dotsrc.encode('utf-8')
# If the text rendering engine (usually Pango) used by dot does
# not draw overlines correctly, uncomment the following two
# lines. Pango 1.28.4 seems not to support combining overline
# while 1.30 does.
#import re
#dotsrc = re.sub(r'(.)(̅|̄)', r'¬\1', dotsrc);
autprefix = (imgdir + '/' + hashlib.sha1(dotsrc).hexdigest())
dotname = autprefix + '.txt'
if not os.access(dotname, os.F_OK):
dotout = open(dotname, "wb", 0)
dotout.write(dotsrc)
dotout.close()
# Create a unused hardlink that points to the output picture
# just to remember how many cache entries are sharing it.
os.link(dotname, tmpdir + "/txt")
if dont_run_dot:
unbufprint('<p>' + dont_run_dot + ''' to be rendered on-line.
However you may download the <a href="''' + cgi.escape(autprefix)
+ '.txt">source in dot format</a> and render it yourself.</p>\n')
else:
render_dot(autprefix)
def render_automaton(automaton, dont_run_dot, issba, deco = None):
dotsrc = spot.ostringstream()
spot.dotty_reachable(dotsrc, automaton, issba, deco)
render_dot_maybe(dotsrc.str(), dont_run_dot)
def render_formula(f):
dotsrc = spot.ostringstream()
spot.dotty(dotsrc, f)
render_dot_maybe(dotsrc.str(), False)
def print_stats(automaton):
stats = spot.stats_reachable(automaton)
unbufprint("<p>%d state" % stats.states)
if stats.states > 1:
unbufprint("s")
unbufprint(", %d transition" % stats.transitions)
if stats.transitions > 1:
unbufprint("s")
count = automaton.number_of_acceptance_conditions()
if count > 0:
unbufprint(", %d acceptance condition" % count)
if count > 1:
unbufprint("s")
acc = automaton.all_acceptance_conditions()
unbufprint(": " + spot.bdd_format_accset(automaton.get_dict(), acc))
else:
unbufprint(", no acceptance condition (all cycles are accepting)")
unbufprint("</p>\n")
# Decide whether we will render the automaton or not.
# (A webserver is not a computation center...)
if stats.states > 64:
return "Automaton has too much states"
if float(stats.transitions)/stats.states > 10:
return "Automaton has too much transitions per state"
return False
def format_formula(f, kind='div'):
if utf8:
s = spot.to_utf8_string(f)
else:
s = str(f)
return '<%s class="formula spot-format">%s</%s>' % (kind, s, kind)
form = cgi.FieldStorage()
output_type = form.getfirst('o', 'v');
# Version requested.
if output_type == 'v':
unbufprint('Spot version %s\n' % spot.version())
finish()
# ltl3ba's version
if output_type == 'v3':
import subprocess
try:
l3proc = subprocess.Popen(['@LTL3BA@', '-v'], stdout=subprocess.PIPE)
(ver, err) = l3proc.communicate()
err = l3proc.returncode
except:
err = 1
if err != 0:
unbufprint('not available')
else:
unbufprint(ver.replace("\n", "<br>"))
finish()
spot.unblock_signal(signal.SIGALRM)
spot.unblock_signal(signal.SIGTERM)
os.setpgrp()
child = os.fork()
if child != 0:
# In parent. We are just waiting for the termination of the
# child, or for the timeout alarm. On SIGALRM, we will kill the
# child.
#
# We cannot avoid forking, because Python will not deliver a
# signal when a C function is running. So if Spot takes too long
# to translate some formula, it would not get interrupted.
signal.signal(signal.SIGALRM, alarm_handler)
signal.alarm(30)
os.waitpid(child, 0)
exit(0)
# Global options
utf8 = False
for g in form.getlist('g'):
if g == '8':
utf8 = True
spot.enable_utf8()
formula = form.getfirst('f', '')
env = spot.default_environment.instance()
pel = spot.empty_parse_error_list()
f = spot.parse(formula, pel, env)
if pel:
unbufprint('<div class="parse-error">')
err = spot.format_parse_errors(spot.get_cout(), formula, pel)
unbufprint('</div>')
# Do not continue if we could not parse anything sensible.
if not f:
finish()
# Formula simplifications
simpopt = spot.ltl_simplifier_options(False, False, False,
False, False, False, True)
dored = False
for r in form.getlist('r'):
dored = True
if r == 'br':
simpopt.reduce_basics = True
elif r == 'lf':
simpopt.reduce_size_strictly = False
elif r == 'si':
simpopt.synt_impl = True
elif r == 'eu':
simpopt.event_univ = True
elif r == 'lc':
simpopt.containment_checks = True
simpopt.containment_checks_stronger = True
if dored:
simp = spot.ltl_simplifier(simpopt)
f2 = simp.simplify(f)
f.destroy()
f = f2
# This also clears the as_bdd() cache.
simp = None
# Formula manipulation only.
if output_type == 'f':
formula_format = form.getfirst('ff', 'o')
# o = Spot, i = Spin, g = GraphViz, p = properties
if formula_format == 'o':
unbufprint(format_formula(f))
elif formula_format == 'i':
unbufprint('<div class="formula spin-format">'
+ spot.to_spin_string(f) + '</div>')
if f.is_psl_formula() and not f.is_ltl_formula():
s = ''
if simpopt.reduce_size_strictly:
s = '<br><b>Try enabling larger formula rewritings.</b>'
unbufprint('<div class="error">The above formula contains PSL operators that Spin will not understand.%s</div>' % s)
elif formula_format == 'g':
render_formula(f)
elif formula_format == 'p':
if utf8:
s = spot.to_utf8_string(f)
else:
s = str(f)
unbufprint('Properties for ' + format_formula(f, 'span') + '<ul>\n')
for p in spot.list_formula_props(f):
unbufprint('<li>%s</li>\n' % p)
# Attempt to refine the hierarchy class using WDBA minimization
if not f.is_syntactic_safety() or not f.is_syntactic_guarantee():
dict = spot.bdd_dict()
automaton = spot.ltl_to_tgba_fm(f, dict, False, True)
minimized = spot.minimize_obligation_new(automaton, f)
if minimized:
g = spot.is_guarantee_automaton(minimized)
s = spot.is_safety_mwdba(minimized)
if s and not f.is_syntactic_safety():
unbufprint('<li>pathologic safety</li>')
if g and not f.is_syntactic_guarantee():
unbufprint('<li>pathologic guarantee</li>')
if not f.is_syntactic_obligation():
unbufprint('<li>obligation (although not syntactically)</li>')
else:
unbufprint('<li>not an obligation</li>')
minimized = 0
automaton = 0
unbufprint('</ul>\n')
finish()
# Formula translation.
translator = form.getfirst('t', 'fm')
if f.is_psl_formula() and not f.is_ltl_formula() and translator != 'fm':
unbufprint('''<div class="error">The PSL formula %s
cannot be translated using this algorithm. Please use Couveur/FM.'''
% format_formula(f, 'span'))
finish()
dict = spot.bdd_dict()
# Should the automaton be displayed as a SBA?
issba = False
if translator == 'fm':
exprop = False
symb_merge = False
branching_postponement = False
fair_loop_approx = False
for fm in form.getlist('fm'):
if fm == 'od':
exprop = True
elif fm == 'sm':
symb_merge = True
elif fm == 'bp':
branching_postponement = True
elif fm == 'fl':
fair_loop_approx = True
automaton = spot.ltl_to_tgba_fm(f, dict,
exprop, symb_merge,
branching_postponement, fair_loop_approx)
elif translator == 'la':
automaton = spot.ltl_to_tgba_lacim(f, dict)
if form.getfirst('la', '') == 'sp':
automaton.delete_unaccepting_scc()
elif translator == 'ta':
refined_rules = False
if form.getfirst('ta', '') == 'lc':
refined_rules = True
automaton = spot.ltl_to_taa(f, dict, refined_rules)
elif translator == 'l3':
l3out = '-T'
l3opt = { '-l', '-P', '-A', '-c', '-C', '-o', '-p' }
for lo in form.getfirst('lo', 'T'):
if lo == 'U':
l3out = '-U'
issba = True
for l3 in form.getlist('l3'):
if l3 == 'l':
l3opt.remove('-l')
elif l3 == 'P':
l3opt.remove('-P')
elif l3 == 'A':
l3opt.remove('-A')
elif l3 == 'C':
l3opt.remove('-C')
l3opt.remove('-c')
elif l3 == 'M':
l3opt.add('-M')
elif l3 == 'S':
l3opt.add('-S')
elif l3 == 'o':
l3opt.remove('-o')
elif l3 == 'p':
l3opt.remove('-p')
args = ["@LTL3BA@", l3out]
args.extend(l3opt)
args.extend(['-f', spot.to_spin_string(f)])
import subprocess
l3file = tmpdir + "/aut"
l3aut = open(l3file, "w+")
try:
l3proc = subprocess.Popen(args, stdout=l3aut)
ret = l3proc.wait()
except:
unbufprint('<div class="error">Failed to run ltl3ba. Is it installed?</div>')
finish()
if ret != 0:
unbufprint('<div class="error">ltl3ba exited with error %s</div>' % ret)
finish()
l3aut.close()
tpel = spot.empty_tgba_parse_error_list()
automaton = spot.tgba_parse(l3file, tpel, dict, env)
if tpel:
unbufprint('''<div class="error">failed to read ltl3ba's output</div>''')
unbufprint('<div class="parse-error">')
err = spot.format_tgba_parse_errors(spot.get_cout(), "output", tpel)
unbufprint('</div>')
automaton = 0
finish()
# Monitor output
if output_type == 'm':
issba = False
automaton = spot.scc_filter(automaton)
automaton = spot.minimize_monitor(automaton)
unbufprint('<div class="automata-stats">')
dont_run_dot = print_stats(automaton)
unbufprint('</div>')
render_automaton(automaton, dont_run_dot, issba)
automaton = 0
finish()
# Automaton simplifications
prune_scc = False
wdba_minimize = False
direct_simul = False
for s in form.getlist('as'):
if s == 'ps':
prune_scc = True
elif s == 'wd':
wdba_minimize = True
elif s == 'ds':
direct_simul = True
if output_type == 'a':
buchi_type = form.getfirst('af', 't')
elif output_type == 'r':
buchi_type = form.getfirst('ra', 't')
else:
unbufprint("Unkown output type 'o=%s'.\n" % output_type)
automaton = 0
finish()
degen = False
neverclaim = False
if buchi_type == 's':
degen = True
elif buchi_type == 'i':
degen = True
neverclaim = True
if prune_scc:
# Do not suppress all useless acceptance conditions if
# degeneralization or simulation is requested: keeping those that
# lead to accepting states usually helps.
automaton = spot.scc_filter(automaton, not (degen or direct_simul))
issba = False
if wdba_minimize:
minimized = spot.minimize_obligation_new(automaton, f)
if minimized:
automaton = minimized
minimized = 0
degen = False # No need to degeneralize anymore
issba = True
direct_simul = False # No need to simulate anymore
if direct_simul:
automaton = spot.simulation(automaton)
issba = False
if degen or neverclaim:
degen = spot.tgba_sba_proxy(automaton)
issba = True
else:
degen = automaton
if utf8:
spot.tgba_enable_utf8(automaton)
# Buchi Automaton Output
if output_type == 'a':
if buchi_type == 'i':
s = spot.ostringstream()
spot.never_claim_reachable(s, degen, f)
unbufprint('<div class="neverclaim">%s</div>' % cgi.escape(s.str()))
del s
else: # 't' or 's'
dont_run_dot = print_stats(degen)
render_automaton(degen, dont_run_dot, issba)
degen = 0
automaton = 0
finish()
# Buchi Run Output
if output_type == 'r':
print_acc_run = False
draw_acc_run = False
s = form.getfirst('rf', 'p')
if s == 'p':
print_acc_run = True
elif s == 'd':
draw_acc_run = True
err = ""
opt = (form.getfirst('ec', 'Cou99') + "(" +
form.getfirst('eo', '') + ")")
eci, err = spot.emptiness_check_instantiator.construct(opt)
if not eci:
unbufprint('<div class="parse-error">Cannot parse "' + opt
+ '" near "' + err + '".</div>')
ec = 0
else:
ec_a = 0
n_acc = degen.number_of_acceptance_conditions()
n_max = eci.max_acceptance_conditions()
n_min = eci.min_acceptance_conditions()
if (n_acc <= n_max):
if (n_acc >= n_min):
ec_a = degen
else:
unbufprint('<div class="ec-error">Cannot run ' + opt
+ ' on automata with less than ' + str(n_min)
+ ' acceptance condition.<br/>Please build '
+ 'a degeneralized B&uuml;chi automaton if you '
+ 'want to try this algorithm.</div>')
else:
unbufprint('<div class="ec-error">Cannot run ' + opt
+ ' on automata with more than ' + str(n_max)
+ ' acceptance condition.<br/>Please build '
+ 'a degeneralized B&uuml;chi automaton if you '
+ 'want to try this algorithm.</div>')
if ec_a:
ec = eci.instantiate(ec_a)
else:
ec = 0
if ec:
ec_res = ec.check()
if not ec_res:
unbufprint('<div class="ec">No accepting run found.</div>')
else:
ec_run = ec_res.accepting_run()
unbufprint('<div class="ec">An accepting run was found.<br/>')
if ec_run:
if print_acc_run:
s = spot.ostringstream()
spot.print_tgba_run(s, ec_a, ec_run)
unbufprint('<div class="accrun">%s</div>' %
cgi.escape(s.str()))
del s
if draw_acc_run:
deco = spot.tgba_run_dotty_decorator(ec_run)
dont_run_dot = print_stats(ec_a)
render_automaton(ec_a, dont_run_dot, issba, deco)
del deco
del ec_run
del ec_res
unbufprint('</div>')
del ec
del ec_a
degen = 0
automaton = 0
finish()
Reference in a new issue View git blame Copy permalink