alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Rename wrap/python/cgi/ as wrap/python/cgi-bin/.

Browse source 
* wrap/python/cgi/: Rename as ...
* wrap/python/cgi-bin/: ... this.
* configure.ac, spot/wrap/python/Makefile.am, README: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2010-01-29 15:19:25 +01:00
parent 28289f95b5
commit 7d5f493fb2
9 changed files with 15 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
wrap/python/cgi-bin/.cvsignore Normal file
View file

@ -0,0 +1,4 @@
Makefile.in
Makefile
ltl2tgba.py

4
wrap/python/cgi-bin/.gitignore vendored Normal file
View file

@ -0,0 +1,4 @@
Makefile.in
Makefile
ltl2tgba.py

32
wrap/python/cgi-bin/Makefile.am Normal file
View file

@ -0,0 +1,32 @@
## Copyright (C) 2003 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.
nodist_noinst_SCRIPTS = ltl2tgba.py
EXTRA_DIST = $(srcdir)/ltl2tgba.in README
CLEANFILES = $(nodist_noinst_SCRIPTS)
ltl2tgba.py: $(srcdir)/ltl2tgba.in Makefile
sed -e 's|[@]PYTHON[@]|@PYTHON@|g' \
-e 's|[@]pythondir[@]|@pythondir@|g' \
-e 's|[@]PACKAGE_VERSION[@]|@PACKAGE_VERSION@|g' \
<$(srcdir)/ltl2tgba.in >ltl2tgba.tmp
chmod +x ltl2tgba.tmp
mv -f ltl2tgba.tmp $@

45
wrap/python/cgi-bin/README Normal file
View file

@ -0,0 +1,45 @@
ltl2tgba.py is a CGI script that translate user-supplied LTL formulae
to Transition-based Generalized Büchi Automata.
You have to install the script yourself if you want to test it.
1) Install Spot first (run `make install' from the top-level).
The CGI scripts uses the Python bindings and assume they
have been installed. Near the top of the script, you
should see a call to sys.path.insert(), with the expected
location og the Python bindings for spot. This path was
configured from ./configure's arguments and you should not
have to fiddle with it. I'm mentionning it just in case.
2) Copy ltl2tgba.py to some place were CGI execution is allowed.
Depending on your HTTP server's configuration, you may have
to rename the script as ltl2tgba.cgi or something else, so
that the server accept to run it.
Apache users in trouble should look at the following options
before digging the Apache manual deeper. These can go
in a .htaccess file (if allowed).
# Treat *.py files as CGI scripts
AddHandle cgi-script .py
# Allow CGI execution in some directory.
Options +ExecCGI
3) In the directory where you have installed ltl2tgba.py,
create a subdirectory called spotimg/. This is where
the script will output its images and other temporary
files. (If you want to change this name, see the imgdir
variable at the top of the script.)
This directory must be writable by the Unix user that
will run the script when the HTTP server processes the
request.
ltl2tgba purges old files (>10min) from this directory
each time it runs.
4) `dot', from the GraphViz package, should be in the PATH.
5) Apache should have its unique_id module loaded.

645
wrap/python/cgi-bin/ltl2tgba.in Executable file
View file

@ -0,0 +1,645 @@
#!@PYTHON@
# -*- mode: python; coding: iso-8859-1 -*-
# Copyright (C) 2009 Laboratoire de Recherche et Développement
# de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2006, 2007 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
import uuid
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'
# Extra HTML headers.
extra_header = ''
# extra_header = '<LINK REL="stylesheet" TYPE="text/css" HREF="style.css">'
# Extra notice to display after the Send button.
extra_form_notice = ''
# Location of the dot command
dot = 'dot' # in PATH.
dot_bgcolor = '-Gbgcolor=#FFFFFF'
# dot = '/usr/local/bin/dot'
ltl2tgba_version = '@PACKAGE_VERSION@'
def print_footer():
print '<hr>'
print 'ltl2tgba.py ' + ltl2tgba_version + '; Spot', spot.version()
print '</BODY></HTML>'
try:
execfile('ltl2tgba.opt')
except IOError:
pass
import spot
import buddy
# 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 """<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>"""
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 +15 -print | xargs rm -f')
myself = os.environ['SCRIPT_NAME'];
form = cgi.FieldStorage()
filled = form.has_key('formula')
uid = str(uuid.uuid1())
imgprefix = imgdir + '/' + uid
def escaped_print_set(dict, what):
print '<pre>'; sys.stdout.flush()
s = spot.ostringstream()
spot.bdd_print_set(s, dict, what)
print cgi.escape(s.str())
del s
print '</pre>'; sys.stdout.flush()
def print_stats(automaton):
stats = spot.stats_reachable(automaton)
print "<p>", 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
count = automaton.number_of_acceptance_conditions()
if count > 0:
print count,
if count <= 1:
print "acceptance condition:",
else:
print "acceptance conditions:",
sys.stdout.flush()
acc = automaton.all_acceptance_conditions()
spot.bdd_print_accset(spot.get_cout(), automaton.get_dict(), acc)
else:
print "no acceptance condition (all cycles are accepting)"
print "</p>"
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, dot_bgcolor, '-Tpng',
'-Gsize=14,14', '-o', basename + '.png', basename + '.txt')
reset_alarm()
b = cgi.escape(basename)
print '<img src="' + b + '.png"><br>(<a href="' + b + '.txt">dot source</a>)'
sys.stdout.flush()
def render_automaton(basename, automata, dont_run_dot, deco = False):
outfile = spot.ofstream(basename + '.txt')
if not deco:
spot.dotty_reachable(outfile, automata)
else:
spot.dotty_reachable(outfile, automata, deco)
del outfile
if dont_run_dot:
print ('<p>' + dont_run_dot + ''' to be rendered on-line. However
you may download the <a href="''' + cgi.escape(basename)
+ '.txt">source in dot format</a> and 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 """
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<HTML lang="en"><HEAD>
<TITLE>Spot's on-line LTL-to-TGBA translator</TITLE>
<META NAME="keywords" CONTENT="Spot,LTL,automata,B&uuml;chi,translation,TGBA">
%s</HEAD>
<BODY>
<H1><a href="http://spot.lip6.fr/">Spot</a>'s on-line
LTL-to-TGBA translator</H1>""" % extra_header
formula = form.getfirst('formula', '')
color_fm = "#DFC6F8"
color_lacim = "#F8C6DF"
color_taa = "#D8C6FF"
options_common = [
('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_never_claim', 'output Spin never claim', 0),
('show_lbtt', 'convert automaton for LBTT', 0),
]
options_reduce = [
('reduce_basics', 'basic rewritings', 1),
('reduce_syntimpl', 'syntactic implication', 1),
('reduce_eventuniv', 'eventuality and universality', 1),
]
options_debug = [
('show_parse', 'show traces during parsing', 0),
('show_dictionnary', 'print BDD dictionary', 0),
]
options_trans_fm = [
('opt_exprop', 'optimize determinism', 1),
('opt_symb_merge',
'merge states with same symbolic successor representation', 1),
('opt_branch_post', 'branching postponement', 0),
('opt_fair_loop_approx','fair-loop approximations', 0),
]
options_trans_lacim = [
('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),
]
options_trans_taa = [
('refined_rules',
'refined rules', 1)
]
default_translator = 'trans_fm';
translators = [
('trans_fm', 'Couvreur/FM', color_fm),
('trans_lacim', 'Couvreur/LaCIM', color_lacim),
('trans_taa', 'Tauriainen/TAA', color_taa),
]
options_accepting_run = [
('print_acc_run', 'print an accepting run...', 0),
('draw_acc_run', 'draw an accepting run...', 0),
('emptiness_check',
['... found using this algorithm: ',
'Cou99',
'CVWY90',
'GV04',
'SE05',
'Tau03',
'Tau03_opt'], 'no'),
('emptiness_check_options',
'...with these <a href="http://spot.lip6.fr/wiki/EmptinessCheckOptions">'
+ 'options</a>:', ''),
]
print ("""<FORM action="%s" method="post"><P>
Formula to translate:
<INPUT size=50 type="text" name="formula" value="%s"><BR>"""
% (myself, cgi.escape(formula, True)))
if not filled:
print """
<p>Use alphanumeric identifiers or double-quoted strings for atomic
propositions, and parentheses for grouping.<BR>Identifiers cannot
start with the letter of a prefix operator (<code>F</code>,
<code>G</code>, or <code>X</code>): for instance <code>GFa</code>
means <code>G(F(a))</code>. Use <code>"GFa"</code> if you really want
to refer to <code>GFa</code> as a proposition.<br>Conversely, infix
letter operators are not assumed to be operators if they are part of
an identifier: <code>aUb</code> is an atomic proposition, unlike
<code>a&nbsp;U&nbsp;b</code> and <code>(a)U(b)</code>.</p>
<table border="1"><tr><td>
<table border="0" rules="groups" frame="void" cellpadding="3" cellspacing=0>
<colgroup span=2>
<colgroup span=2>
<colgroup span=2>
<colgroup span=2>
<thead>
<tr>
<th colspan=2>Unary operators<br>(prefix)</th>
<th colspan=4>Binary operators<br>(infix)</th>
<th colspan=2>Constants</th>
</tr>
</thead>
<tbody>
<tr>
<td align="right">not:</td><td><code>!</code></td>
<td align="right">and:</td><td><code>&</code> <code>&&</code>
<code>.</code> <code>*</code>
<code>/\</code></td>
<td align="right">xor:</td><td><code>^</code> <code>xor</code></td>
<td align="right">true:</td><td><code>1</code>
<code>true</code></td>
</tr>
<tr>
<td align="right">eventually:</td><td><code>F</code>
<code>&lt;&gt;</code></td>
<td align="right">or:</td><td><code>|</code> <code>||</code>
<code>+</code> <code>\/</code></td>
<td align="right">until:</td><td><code>U</code></td>
<td align="right">false:</td><td><code>0</code>
<code>false</code></td>
</tr>
<tr>
<td align="right">always:</td><td><code>G</code>
<code>[]</code></td>
<td align="right">implies:</td><td><code>-&gt;</code>
<code>=&gt;</code></td>
<td align="right">release:</td><td><code>R</code>
<code>V</code></td>
<td></td><td></td>
</tr>
<tr>
<td align="right">next:</td><td><code>X</code> <code>()</code></td>
<td align="right">equivalent:</td><td><code>&lt;-&gt;</code>
<code>&lt;=&gt;</code></td>
<td></td><td></td>
<td></td><td></td>
</tr>
</tbody>
</table></td></tr></table>"""
column = [[], []]
def add_options(opt_group, opt_column, opt_color, opt_list):
if opt_color:
opt_color = ' bgcolor="%s"' % opt_color
if opt_group:
column[opt_column].append(("<TH%s>" % opt_color) + opt_group + "</TH>")
prefix = ''
else:
prefix = '&nbsp;&nbsp;&nbsp;&nbsp;'
for opt, desc, arg, in opt_list:
if not isinstance(arg, str):
if formula:
val = int(form.getfirst(opt, 0))
else:
val = arg
s = '<TD%s>%s' % (opt_color, prefix);
if isinstance(desc, list):
s += '%s <select name="%s">' % (desc[0], opt);
n = 1
if val >= len(desc) or val < 1:
val = n
for i in desc[1:]:
if n == val:
chk = ' selected'
else:
chk = ''
s += '<option value="%s"%s>%s' % (n, chk, i);
n += 1
s += '</select>'
val = desc[val]
elif isinstance(arg, str):
val = form.getfirst(opt, arg)
s += (('%s <INPUT type="text" maxlength="40" '
+ 'name="%s" value="%s">') %
(desc, opt, cgi.escape(val, True)))
else:
if val:
chk = ' checked'
else:
chk = ''
s += '<INPUT type="checkbox" name="%s" value="1"%s>%s' % (opt, chk,
desc)
column[opt_column].append((s + '</TD>'))
globals()[opt] = val
column[0].append("<TH>Algorithm</TH>")
trans = form.getfirst("trans", default_translator)
for opt, desc, color in translators:
if trans == opt:
chk = "checked"
else:
chk = ""
globals()[opt] = chk
s = \
'<TD bgcolor="%s"><INPUT type="radio" name="trans" value="%s" %s>%s</TD>'
column[0].append(s % (color, opt, chk, desc))
add_options('', 0, color, globals()['options_' + opt])
add_options("Search accepting run?", 0, '', options_accepting_run)
add_options("Common Options", 1, '', options_common)
add_options("Formula Simplications", 1, '', options_reduce)
add_options("Debugging Options", 1, '', options_debug)
print '<TABLE>'
width = range(len(column))
depth = 0
for i in width:
depth = max(len(column[i]), depth)
for d in range(depth):
print '<TR>'
for i in width:
if d < len(column[i]):
print column[i][d]
else:
print '<TD></TD>'
print '</TR>'
print '</TABLE>'
print '<INPUT type="submit" value="Send">%s</FORM>' % extra_form_notice
if not filled:
print_footer()
sys.exit(0)
reset_alarm()
print "<hr><H1>Output</H1>"
env = spot.default_environment.instance()
print "<H2>LTL Formula</H2>"
if show_parse: print '<pre>'
sys.stdout.flush()
sys.stderr.flush()
pel = spot.empty_parse_error_list()
f = spot.parse(formula, pel, env, show_parse)
if show_parse: print '</pre>'
print '<font color="red"><pre>'
err = spot.format_parse_errors(spot.get_cout(), formula, pel)
print '</pre></font>'
if not f:
print '<p><b>Aborting...</b></p>'
sys.exit(0)
if err:
print '<p><b>Continuing anyway...</b></p>'
print "<p>Formula is<code>", f, "</code></p>"
if show_formula_png:
outfile = spot.ofstream(imgprefix + '-f.txt')
spot.dotty(outfile, f)
del outfile
render_dot(imgprefix + '-f')
opt = spot.Reduce_None
if reduce_basics:
opt = opt + spot.Reduce_Basics
if reduce_syntimpl:
opt = opt + spot.Reduce_Syntactic_Implications
if reduce_eventuniv:
opt = opt + spot.Reduce_Eventuality_And_Universality
if opt != spot.Reduce_None:
f2 = spot.reduce(f, opt)
f.destroy()
f = f2
print "<p>Reduced formula is<code>", f, "</code></p>"
if show_formula_png:
outfile = spot.ofstream(imgprefix + '-f2.txt')
spot.dotty(outfile, f)
del outfile
render_dot(imgprefix + '-f2')
print '<H2>Automaton</H2>'
dict = spot.bdd_dict()
print '<p>Building automaton...',
sys.stdout.flush()
if opt_exprop:
exprop = 1
else:
exprop = 0
if opt_symb_merge:
symb_merge = 1
else:
symb_merge = 0
if opt_branch_post:
branching_postponement = 1
else:
branching_postponement = 0
if opt_fair_loop_approx:
fair_loop_approx = 1
else:
fair_loop_approx = 0
if trans_lacim:
automaton = spot.ltl_to_tgba_lacim(f, dict)
elif trans_fm:
automaton = spot.ltl_to_tgba_fm(f, dict,
exprop, symb_merge, branching_postponement,
fair_loop_approx)
elif trans_taa:
automaton = spot.ltl_to_taa(f, dict, refined_rules)
print 'done.</p>'
sys.stdout.flush()
dont_run_dot = print_stats(automaton)
if show_automaton_png:
render_automaton(imgprefix + '-a', automaton, dont_run_dot)
if show_degen_png or show_never_claim:
print '<H3>Degeneralized automaton</H3>'
degen = spot.tgba_sba_proxy(automaton)
dont_run_dot = print_stats(degen)
if show_degen_png:
render_automaton(imgprefix + '-d', degen, dont_run_dot)
else:
degen = 0
if show_never_claim:
print '<H3>Never claim (for degeneralized automaton)</H3>'
print '<PRE>'
s = spot.ostringstream()
spot.never_claim_reachable(s, degen, f)
print cgi.escape(s.str())
del s
print '</PRE>'
sys.stdout.flush()
if show_dictionnary:
print '<H3>BDD dictionary</H3>'
print '<pre>'
sys.stdout.flush()
automaton.get_dict().dump(spot.get_cout())
print '</pre>'
if (type(automaton) == spot.tgba_bdd_concrete
and (show_relation_set or show_relation_png)):
print '<H3>Transition relation</H3>'
if show_relation_set:
escaped_print_set(automaton.get_dict(),
automaton.get_core_data().relation)
if show_relation_png:
render_bdd(imgprefix + '-b', automaton.get_dict(),
automaton.get_core_data().relation)
if (type(automaton) == spot.tgba_bdd_concrete
and (show_acceptance_set or show_acceptance_png)):
print '<H3>Acceptance relation</H3>'
if show_acceptance_set:
escaped_print_set(automaton.get_dict(),
automaton.get_core_data().acceptance_conditions)
if show_acceptance_png:
render_bdd(imgprefix + '-c', automaton.get_dict(),
automaton.get_core_data().acceptance_conditions)
if show_lbtt:
print '<H3>LBTT conversion</H3>'
if degen:
print '<H4>Conversion of the generalized automaton</H4>'
print '<pre>'
sys.stdout.flush()
spot.lbtt_reachable(spot.get_cout(), automaton)
print '</pre>'
if degen:
print '<H4>Conversion of the degeneralized automaton</H4>'
print '<pre>'
sys.stdout.flush()
spot.lbtt_reachable(spot.get_cout(), degen)
print '</pre>'
if draw_acc_run or print_acc_run:
print '<H3>Accepting run</H3>'
sys.stdout.flush()
err = ""
opt = emptiness_check + "(" + emptiness_check_options + ")"
eci, err = spot.emptiness_check_instantiator.construct(opt)
ec_msg = "Running " + opt
if not eci:
print ('<font color="red">Cannot parse "' + opt + '" near "' + err
+ '".</font>')
else:
ec_a = 0
n_acc = automaton.number_of_acceptance_conditions()
n_max = eci.max_acceptance_conditions()
if (n_acc <= n_max):
ec_a = automaton
else:
if degen:
ec_a = degen
ec_msg += ' <b>on degeneralized automaton</b>'
else:
print ('<font color="red">Cannot run ' + emptiness_check
+ ' on automata with more than ' + n_max + ' acceptance '
+ 'conditions. Please select "draw degeneralized '
+ 'Büchi automaton" if you want to try this'
+ ' algorithm on the degeneralized version of the'
+ ' automaton.</font>')
if ec_a:
ec = eci.instantiate(ec_a)
if ec:
print '%s: ' % ec_msg
sys.stdout.flush()
ec_res = ec.check()
if not ec_res:
print "no accepting run found.<br>"
else:
ec_run = ec_res.accepting_run()
print "accepting run found.<br>"
if ec_run:
if print_acc_run:
print '<pre>'; sys.stdout.flush()
s = spot.ostringstream()
spot.print_tgba_run(s, ec_a, ec_run)
print cgi.escape(s.str())
del s
print '</pre>'; sys.stdout.flush()
if draw_acc_run:
deco = spot.tgba_run_dotty_decorator(ec_run)
dont_run_dot = print_stats(ec_a)
render_automaton(imgprefix + '-e', ec_a, dont_run_dot, deco)
del deco
del ec_run
del ec_res
del ec
del ec_a
sys.stdout.flush()
f.destroy()
# Make sure degen is cleared before automaton.
del degen
del automaton
del dict
print_footer()