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

Remove the old CGI interface.

Browse source 
* wrap/python/cgi-bin: Remove this directory.
* wrap/python/Makefile.am (SUBDIRS): Remove it.
* configure.ac, README, wrap/python/ajax/README: Likewise.
This commit is contained in:
Alexandre Duret-Lutz 2011-11-28 18:17:50 +01:00
parent 6794b8570a
commit 6acf30b2ab
10 changed files with 15 additions and 854 deletions
Download patch file Download diff file Expand all files Collapse all files

8
ChangeLog
View file

@ -1,3 +1,11 @@
2011-11-28 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Remove the old CGI interface.
* wrap/python/cgi-bin: Remove this directory.
* wrap/python/Makefile.am (SUBDIRS): Remove it.
* configure.ac, README, wrap/python/ajax/README: Likewise.
2011-11-28 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Undocument `.' from the web interface.

3
README
View file

@ -142,8 +142,7 @@ bench/ Benchmarks for ...
wrap/ Wrappers for other languages.
python/ Python bindings for Spot and BuDDy
tests/ Tests for these bindings
cgi-bin/ Python-based CGI script (ltl-to-tgba translator)
ajax/ Moderner LTL-to-TGBA translator, using Ajax.
ajax/ LTL-to-TGBA translator with web interface, using Ajax.
iface/ Interfaces to other libraries.
dve2/ Interface with DiVinE2.
gspn/ GreatSPN interface.

1
configure.ac
View file

@ -141,7 +141,6 @@ AC_CONFIG_FILES([
wrap/Makefile
wrap/python/Makefile
wrap/python/ajax/Makefile
wrap/python/cgi-bin/Makefile
wrap/python/tests/Makefile
])
AC_CONFIG_FILES([bench/ltl2tgba/ltl2baw.pl:bench/ltl2tgba/ltl2baw.in],

2
wrap/python/Makefile.am
View file

@ -21,7 +21,7 @@
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA.
SUBDIRS = . cgi-bin ajax tests
SUBDIRS = . ajax tests
AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) \
-DSWIG_TYPE_TABLE=spot

13
wrap/python/ajax/README
View file

@ -2,10 +2,7 @@ ltl2tgba.html is a dynamic web page that translates user-supplied LTL
formulae to Transition-based Generalized Büchi Automata. The actual
translation work is performed by a CGI script in Python: spot.py.
This is actually meant to be a moderner rewrite of the cgi script in
../cgi-bin/
There are two ways to use the page: using a web server such as
There are two ways to use the script: using a web server such as
Apache, or standalone.
In both cases you should ensure that the command `dot', from the
@ -16,10 +13,10 @@ GraphViz package, is in the PATH. configure should have picked it up.
Standalone usage
================
Simply run the spot.py from this directory. This will create a
directory called spotimg/ in the current directory (this will hold the
generated pictures) and start an HTTP server on port 8000. Point your
browser to http://localhost:8000/ltl2tgba.html and you should be OK.
Simply run spot.py from this directory. This will create a directory
called spotimg/ in the current directory (this will hold the generated
pictures) and start an HTTP server on port 8000. Point your browser
to http://localhost:8000/ltl2tgba.html and you should be OK.
After you have killed the server process (e.g. with Control-C),
you may want to erase the spotimg/ directory.

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

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

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

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

38
wrap/python/cgi-bin/Makefile.am
View file

@ -1,38 +0,0 @@
## Copyright (C) 2003, 2010 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|[@]srcdir[@]|@srcdir@|g' \
-e 's|[@]top_builddir[@]|@top_builddir@|g' \
-e 's|[@]PACKAGE_VERSION[@]|@PACKAGE_VERSION@|g' \
-e 's|[@]DOT[@]|@DOT@|g' \
<$(srcdir)/ltl2tgba.in >ltl2tgba.tmp
chmod +x ltl2tgba.tmp
mv -f ltl2tgba.tmp $@
clean-local:
rm -rf spotimg

61
wrap/python/cgi-bin/README
View file

@ -1,61 +0,0 @@
ltl2tgba.py is a CGI script that translate user-supplied LTL formulae
to Transition-based Generalized Büchi Automata.
There are two ways to use the script: using a web server such as
Apache, or standalone.
In both cases you should ensure that the command `dot', from the
GraphViz package, is in the PATH.
Standalone usage
================
Simply run the script from this directory. This will create a
directory called spotimg/ in the current directory (this will hold the
generated pictures) and start an HTTP server on port 8000. Point your
browser to http://localhost:8000/ltl2tgba.py and you should be OK.
After you have killed the server process (e.g. with Control-C),
you may want to erase the spotimg/ directory.
Installing on a real web server
===============================
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 of 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 accepts 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 (>15min) from this directory
each time it runs.

735
wrap/python/cgi-bin/ltl2tgba.in
View file

@ -1,735 +0,0 @@
#!@PYTHON@
# -*- mode: python; coding: iso-8859-1 -*-
# Copyright (C) 2007, 2009, 2010, 2011 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
# Copyright (C) 2003, 2004, 2006 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 os
# Directory for temporary files (images and other auxiliary files).
imgdir = 'spotimg'
from CGIHTTPServer import CGIHTTPRequestHandler
class MyHandler(CGIHTTPRequestHandler):
def is_cgi(self):
if self.path == '/ltl2tgba.py':
self.cgi_info = '', 'ltl2tgba.py'
return True
return False
if not os.environ.has_key('SCRIPT_NAME'):
# If this is not run as a cgi script, let's start an HTTP server.
from BaseHTTPServer import HTTPServer
server_address=('',8000)
if not os.access(imgdir, os.F_OK):
os.mkdir(imgdir, 0755)
print "Directory spotimg/ created."
httpd = HTTPServer(server_address, MyHandler)
print "Point your browser to http://localhost:8000/ltl2tgba.py"
httpd.serve_forever()
import sys
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())
# Assume Spot is installed
sys.path.insert(0, '@pythondir@')
if (os.environ.has_key('SERVER_SOFTWARE') and
os.environ['SERVER_SOFTWARE'].startswith(MyHandler.server_version)):
# 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
# 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@'
dot_bgcolor = '-Gbgcolor=#FFFFFF'
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()
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):
if svg_output:
ext = 'svg'
else:
ext = 'png'
os.spawnlp(os.P_WAIT, dot, dot, dot_bgcolor, '-T' + ext,
'-Gsize=14,14', '-o', basename + '.' + ext, basename + '.txt')
reset_alarm()
b = cgi.escape(basename)
if svg_output:
print ('<object type="image/svg+xml" data="' + b + '.svg">'
+ 'Your browser does not support SVG.</object>')
else:
print ('<img src="' + b + '.png"><br>(<a href="' + b
+ '.txt">dot source</a>)')
sys.stdout.flush()
def render_automaton(basename, automata, dont_run_dot, issba, deco = False):
outfile = spot.ofstream(basename + '.txt')
if not deco:
spot.dotty_reachable(outfile, automata, issba)
else:
spot.dotty_reachable(outfile, automata, issba, 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 = "#F8DFC6"
new = ' <font color="red"><small>(NEW)</small></font>'
options_common = [
('show_formula_png', 'draw the formula', 0),
('show_automaton_png', 'draw B&uuml;chi automaton', 1),
('show_degen_png', 'draw degeneralized B&uuml;chi automaton', 0),
('show_never_claim', 'output Spin never claim', 0),
('show_lbtt', 'convert automaton for LBTT', 0),
('svg_output', 'render automata in SVG instead of PNG', 0),
]
options_reduce = [
('reduce_basics', 'basic rewritings', 1),
('reduce_syntimpl', 'syntactic implication', 1),
('reduce_eventuniv', 'eventuality and universality', 1),
('reduce_langcont', 'language containment', 0),
]
options_aut_reduce = [
('reduce_scc', 'prune unaccepting SCCs', 1),
('reduce_wdba', 'minimize obligation properties' + new, 0),
('reduce_dmonitor', 'build deterministic monitor' + new, 0),
]
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 = [
('symbolically_prune_scc',
'symbolically prune unaccepting SCCs', 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),
]
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> <code>~</code></td>
<td align="right">and:</td><td><code>&</code> <code>&&</code>
<code>.</code> <code>/\</code></td>
<td align="right">(strong) until:</td><td><code>U</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">weak until:</td><td><code>W</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>
<code>=&gt;</code></td>
<td align="right">(weak) 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>
<code>&lt;=&gt;</code></td>
<td align="right">strong release:</td><td><code>M</code></td>
<td></td><td></td>
</tr>
<tr>
<td></td><td></td>
<td align="right">xor:</td><td><code>^</code> <code>xor</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
val = int(form.getfirst(opt, n))
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 Output Options", 1, '', options_common)
add_options("Formula Simplications", 1, '', options_reduce)
add_options("Automata Simplifications", 1, '', options_aut_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()
# Cleanup stale files from our image directory.
os.system('find ' + imgdir + ' -type f -amin +15 -print | xargs rm -f')
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>'
if pel:
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 pel:
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 reduce_langcont:
opt = opt + spot.Reduce_Containment_Checks_Stronger
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)
if symbolically_prune_scc:
automaton.delete_unaccepting_scc()
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)
issba = False
if reduce_dmonitor:
automaton = spot.minimize_monitor(automaton)
elif reduce_wdba:
minimized = spot.minimize_obligation_new(automaton, f)
if minimized:
automaton = minimized
minimized = 0
issba = True
elif reduce_scc:
# Do not suppress all useless acceptance conditions if
# degeneralization is requested: keeping those that lead to
# accepting states usually help.
automaton = spot.scc_filter(automaton, not (show_degen_png or
show_never_claim))
print 'done.</p>'
sys.stdout.flush()
dont_run_dot = print_stats(automaton)
if show_automaton_png:
render_automaton(imgprefix + '-a', automaton, dont_run_dot, issba)
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, True)
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>'
ec = 0
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>'
issba = True
else:
print ('<font color="red">Cannot run ' + emptiness_check
+ ' on automata with more than ' + str(n_max)
+ ' acceptance conditions. Please select '
+ '"draw degeneralized B&uuml;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,
issba, 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()