#!@PYTHON@
# -*- mode: python; coding: iso-8859-1 -*-
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
# et Marie Curie.
#
# 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 sys
import os
import cgi
import cgitb; cgitb.enable()
import signal
print "Content-Type: text/html"
print
# Redirect stderr to stdout.
os.close(sys.stderr.fileno())
os.dup2(sys.stdout.fileno(), sys.stderr.fileno())
sys.path.insert(0, '@pythondir@')
# Directory for temporary files (images and other auxiliary files).
imgdir = 'spotimg'
import spot
import buddy
def print_footer():
print '
'
print 'ltl2tgba.py @PACKAGE_VERSION@; Spot', spot.version()
# We want the script to kill itself whenever it run for more than 30
# seconds. `dot' can be very long at drawing huge graphs, and may
# bring a web server to its knees. Doing so also protects us from any
# infinite loop in Spot.
#
# We use alarm(30) because 30 seconds ought to be enough for everyone.
# We create a process group for the script and its children (dot).
# Upon SIGALRM, we kill the whole process group.
#
# For all this to work, SIGALRM and SIGTERM must not be blocked.
# Apache (at least in my tests with version 2.0.48) blocks them by
# default. I haven't figured a Python way to unblock them, so the
# spot bindings supply unblock_signal(signum) for this purpose.
def alarm_handler(signum, frame):
print """The script was aborted because
it has been running for too long. 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.
"""
print_footer()
sys.stdout.flush()
os.kill(0, signal.SIGTERM)
def reset_alarm():
signal.alarm(30)
spot.unblock_signal(signal.SIGALRM)
spot.unblock_signal(signal.SIGTERM)
os.setpgrp()
signal.signal(signal.SIGALRM, alarm_handler)
reset_alarm()
# Cleanup stale files from our image directory.
os.system('find ' + imgdir + ' -type f -amin +10 -print | xargs rm -f')
myself = os.environ['SCRIPT_NAME'];
form = cgi.FieldStorage()
filled = form.has_key('formula')
# FIXME: This assumes Apache.
uid = os.environ['UNIQUE_ID'];
imgprefix = imgdir + '/' + uid
def escaped_print_set(dict, what):
print ''; sys.stdout.flush()
s = spot.ostringstream()
spot.bdd_print_set(s, dict, what)
print cgi.escape(s.str())
del s
print ''; sys.stdout.flush()
def print_stats(automaton):
stats = spot.stats_reachable(automaton)
print "", stats.states,
if stats.states <= 1:
print " state,",
else:
print " states,",
print stats.transitions,
if stats.transitions <= 1:
print " transition,",
else:
print " transitions,",
# compute the number of acceptance conditions
acc = all = automaton.all_acceptance_conditions()
count = 0
while all != buddy.bddfalse:
all -= buddy.bdd_satone(all)
count += 1
if count > 0:
print count,
if count <= 1:
print "acceptance condition:",
else:
print "acceptance conditions:",
sys.stdout.flush()
spot.bdd_print_accset(spot.get_cout(), automaton.get_dict(), acc)
else:
print "no acceptance condition (all cycles are accepting)"
print "
"
sys.stdout.flush()
# Decide whether we will render the automaton or not.
# (A webserver is not a calcul 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 states"
return False
def render_dot(basename):
os.spawnlp(os.P_WAIT, 'dot', 'dot', '-Tpng', '-Gsize=14,14', '-o',
basename + '.png', basename + '.txt')
reset_alarm()
b = cgi.escape(basename)
print '
(dot source)'
sys.stdout.flush()
def render_automaton(basename, automata, dont_run_dot):
outfile = spot.ofstream(basename + '.txt')
spot.dotty_reachable(outfile, automata)
del outfile
if dont_run_dot:
print ('' + dont_run_dot + ''' to be rendered on-line. However
you may download the source in dot format en render it yourself.')
else:
render_dot(basename)
def render_bdd(basename, dictionary, bdd):
outfile = spot.ofstream(basename + '.txt')
spot.bdd_print_dot(outfile, dictionary, bdd)
del outfile
render_dot(basename)
print "
LTL-to-Büchi test"
print """Spot's on-line
LTL-to-Büchi translator
"""
formula = form.getfirst('formula', '')
options = [(
'Common options', 0, [
('show_formula_png', 'draw the formula', 0),
('show_automaton_png', 'draw Büchi automaton', 1),
('show_degen_png', 'draw degeneralized Büchi automaton', 0),
('show_lbtt', 'convert automaton for LBTT', 0),
]), (
'Debugging options', 0, [
('show_parse', 'show traces during parsing', 0),
('show_dictionnay', 'print BDD dictionary', 0),
]), (
'Couvreur/FM options', 1, [
('opt_exprop', 'optimize determinism', 1),
('opt_symb_merge',
'merge states with same symbolic successor representation', 1),
]), (
'Couvreur/Lacim options', 1, [
('show_relation_set',
'print the transition relation as a BDD set', 0),
('show_relation_png',
'draw the transition relation', 0),
('show_acceptance_set',
'print the acceptance relation as a BDD set', 0),
('show_acceptance_png',
'draw the acceptance relation', 0),
])]
default_translator = 'trans_fm';
translators = [
('trans_fm', 'Convreur/FM'),
('trans_lacim', 'Convreur/LaCIM'),
]
print ("""