7ba4ab7931
* src/tgbaalgos/simulation.hh: Mention the fact that this is a "direct" simulation. * wrap/python/ajax/ltl2tgba.html: Likewise, and change the key to "ds". * wrap/python/ajax/protocol.txt, wrap/python/ajax/spot.in: Adjust.
551 lines
18 KiB
Python
Executable file
551 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'))
|
|
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
|
|
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 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
|
|
direct_simul = False # No need to simulate anymore
|
|
|
|
if direct_simul:
|
|
automaton = spot.simulation(automaton)
|
|
|
|
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>')
|
|
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ü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()
|