61127a3fd5
* 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() instead. * 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.
544 lines
18 KiB
Python
Executable file
544 lines
18 KiB
Python
Executable file
#!@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 # FIXME: SVG output seems to be working well with
|
|
# Firefox only. We have to figure out how
|
|
# to get the correct size and transparent
|
|
# background in Chrome.
|
|
|
|
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):
|
|
sys.stdout.write(s.encode("utf-8"))
|
|
|
|
|
|
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'),
|
|
global_vars, local_vars)
|
|
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 (not drawing automata usually helps).
|
|
If you want to benchmark big formulae it is
|
|
better to install Spot on your own computer.</p>\n""")
|
|
finish(kill = True)
|
|
|
|
def reset_alarm():
|
|
signal.alarm(30)
|
|
|
|
def render_dot(basename):
|
|
unbufprint('<div class="dot">')
|
|
if svg_output:
|
|
ext = 'svg'
|
|
else:
|
|
ext = 'png'
|
|
|
|
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')
|
|
reset_alarm()
|
|
# Create an unused hardlink that point to the output picture
|
|
# just to remember how many cache entries are sharing it.
|
|
os.link(outname, tmpdir + "/" + ext)
|
|
b = cgi.escape(basename)
|
|
if svg_output:
|
|
unbufprint('<object type="image/svg+xml" data="' + b +
|
|
'.svg">Your browser does not support SVG.</object>')
|
|
else:
|
|
unbufprint('<img src="' + b + '.png"><br>(<a href="' + b
|
|
+ '.txt">dot source</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).
|
|
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 = False):
|
|
dotsrc = spot.ostringstream()
|
|
if not deco:
|
|
spot.dotty_reachable(dotsrc, automaton, issba)
|
|
else:
|
|
spot.dotty_reachable(dotsrc, automaton, issba, deco)
|
|
render_dot_maybe(dotsrc.str().encode('utf-8'), 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
|
|
|
|
form = cgi.FieldStorage()
|
|
|
|
output_type = form.getfirst('o', 'v');
|
|
|
|
# Version requested.
|
|
if output_type == 'v':
|
|
unbufprint('Spot version %s\n' % spot.version())
|
|
finish()
|
|
|
|
spot.unblock_signal(signal.SIGALRM)
|
|
spot.unblock_signal(signal.SIGTERM)
|
|
os.setpgrp()
|
|
signal.signal(signal.SIGALRM, alarm_handler)
|
|
reset_alarm()
|
|
|
|
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
|
|
opt = spot.Reduce_None
|
|
for r in form.getlist('r'):
|
|
if r == 'br':
|
|
opt = opt + spot.Reduce_Basics
|
|
elif r == 'si':
|
|
opt = opt + spot.Reduce_Syntactic_Implications
|
|
elif r == 'eu':
|
|
opt = opt + spot.Reduce_Eventuality_And_Universality
|
|
elif r == 'lc':
|
|
opt = opt + spot.Reduce_Containment_Checks_Stronger
|
|
if opt != spot.Reduce_None:
|
|
f2 = spot.reduce(f, opt)
|
|
f.destroy()
|
|
f = f2
|
|
|
|
# Formula manipulation only.
|
|
if output_type == 'f':
|
|
formula_format = form.getfirst('ff', 'o')
|
|
# o = Spot, i = Spin, g = GraphViz
|
|
if formula_format == 'o':
|
|
unbufprint('<div class="formula spot-format">%s</div>' % f)
|
|
elif formula_format == 'i':
|
|
unbufprint('<div class="formula spin-format">'
|
|
+ spot.to_spin_string(f) + '</div>')
|
|
elif formula_format == 'g':
|
|
render_formula(f)
|
|
finish()
|
|
|
|
# Formula translation.
|
|
translator = form.getfirst('t', 'fm')
|
|
|
|
dict = spot.bdd_dict()
|
|
|
|
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)
|
|
|
|
# Should it be displayed as a SBA?
|
|
issba = False
|
|
|
|
# Monitor output
|
|
if output_type == 'm':
|
|
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
|
|
for s in form.getlist('as'):
|
|
if s == 'ps':
|
|
prune_scc = True
|
|
elif s == 'wd':
|
|
wdba_minimize = 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 is requested: keeping those that lead to
|
|
# accepting states usually helps.
|
|
automaton = spot.scc_filter(automaton, not degen)
|
|
|
|
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
|
|
|
|
if degen or neverclaim:
|
|
degen = spot.tgba_sba_proxy(automaton)
|
|
issba = True
|
|
else:
|
|
degen = 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>')
|
|
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ü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ü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()
|