635 lines
20 KiB
Python
635 lines
20 KiB
Python
#!@PYTHON@
|
|
# -*- mode: python; coding: iso-8859-1 -*-
|
|
# 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 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'
|
|
|
|
# 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')
|
|
# FIXME: This assumes Apache.
|
|
uid = os.environ['UNIQUE_ID'];
|
|
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ü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"
|
|
|
|
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),
|
|
]
|
|
|
|
default_translator = 'trans_fm';
|
|
translators = [
|
|
('trans_fm', 'Couvreur/FM', color_fm),
|
|
('trans_lacim', 'Couvreur/LaCIM', color_lacim),
|
|
]
|
|
|
|
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 U 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><></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>-></code>
|
|
<code>=></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><-></code>
|
|
<code><=></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 = ' '
|
|
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)
|
|
spot.destroy(f)
|
|
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)
|
|
|
|
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_concretePtr
|
|
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_concretePtr
|
|
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()
|
|
|
|
spot.destroy(f)
|
|
# Make sure degen is cleared before automaton.
|
|
del degen
|
|
del automaton
|
|
|
|
del dict
|
|
print_footer()
|