From 6acf30b2abe70132a7018f360ae8cbb9310e3e4f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 28 Nov 2011 18:17:50 +0100 Subject: [PATCH] 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. --- ChangeLog | 8 + README | 3 +- configure.ac | 1 - wrap/python/Makefile.am | 2 +- wrap/python/ajax/README | 13 +- wrap/python/cgi-bin/.cvsignore | 4 - wrap/python/cgi-bin/.gitignore | 4 - wrap/python/cgi-bin/Makefile.am | 38 -- wrap/python/cgi-bin/README | 61 --- wrap/python/cgi-bin/ltl2tgba.in | 735 -------------------------------- 10 files changed, 15 insertions(+), 854 deletions(-) delete mode 100644 wrap/python/cgi-bin/.cvsignore delete mode 100644 wrap/python/cgi-bin/.gitignore delete mode 100644 wrap/python/cgi-bin/Makefile.am delete mode 100644 wrap/python/cgi-bin/README delete mode 100755 wrap/python/cgi-bin/ltl2tgba.in diff --git a/ChangeLog b/ChangeLog index 4f5aed614..e652e061c 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,11 @@ +2011-11-28 Alexandre Duret-Lutz + + 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 Undocument `.' from the web interface. diff --git a/README b/README index 00067d74d..ddf3ba6d3 100644 --- a/README +++ b/README @@ -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. diff --git a/configure.ac b/configure.ac index 8b42d948f..5cdefd619 100644 --- a/configure.ac +++ b/configure.ac @@ -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], diff --git a/wrap/python/Makefile.am b/wrap/python/Makefile.am index 601921caa..04aec2052 100644 --- a/wrap/python/Makefile.am +++ b/wrap/python/Makefile.am @@ -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 diff --git a/wrap/python/ajax/README b/wrap/python/ajax/README index 714334f59..bff90f76e 100644 --- a/wrap/python/ajax/README +++ b/wrap/python/ajax/README @@ -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. diff --git a/wrap/python/cgi-bin/.cvsignore b/wrap/python/cgi-bin/.cvsignore deleted file mode 100644 index 5e70e476e..000000000 --- a/wrap/python/cgi-bin/.cvsignore +++ /dev/null @@ -1,4 +0,0 @@ -Makefile.in -Makefile -ltl2tgba.py - diff --git a/wrap/python/cgi-bin/.gitignore b/wrap/python/cgi-bin/.gitignore deleted file mode 100644 index 5e70e476e..000000000 --- a/wrap/python/cgi-bin/.gitignore +++ /dev/null @@ -1,4 +0,0 @@ -Makefile.in -Makefile -ltl2tgba.py - diff --git a/wrap/python/cgi-bin/Makefile.am b/wrap/python/cgi-bin/Makefile.am deleted file mode 100644 index 3172a00c2..000000000 --- a/wrap/python/cgi-bin/Makefile.am +++ /dev/null @@ -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 diff --git a/wrap/python/cgi-bin/README b/wrap/python/cgi-bin/README deleted file mode 100644 index 838924632..000000000 --- a/wrap/python/cgi-bin/README +++ /dev/null @@ -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. diff --git a/wrap/python/cgi-bin/ltl2tgba.in b/wrap/python/cgi-bin/ltl2tgba.in deleted file mode 100755 index cb53e670d..000000000 --- a/wrap/python/cgi-bin/ltl2tgba.in +++ /dev/null @@ -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 = '' - -# 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 '
' - print 'ltl2tgba.py ' + ltl2tgba_version + '; Spot', spot.version() - print '' - -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 """

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() - - -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 '
'; 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 - 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 "

" - 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 ('' - + 'Your browser does not support SVG.') - else: - print ('
(dot source)') - 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 ('

' + dont_run_dot + ''' to be rendered on-line. However -you may download the source in dot format 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 """ - - -Spot's on-line LTL-to-TGBA translator - -%s - -

Spot's on-line -LTL-to-TGBA translator

""" % extra_header - -formula = form.getfirst('formula', '') - -color_fm = "#DFC6F8" -color_lacim = "#F8C6DF" -color_taa = "#F8DFC6" - -new = ' (NEW)' - -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), - ('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 ' - + 'options:', ''), - ] - -print ("""

-Formula to translate: -
""" - % (myself, cgi.escape(formula, True))) - -if not filled: - print """ -

Use alphanumeric identifiers or double-quoted strings for atomic -propositions, and parentheses for grouping.
Identifiers cannot -start with the letter of a prefix operator (F, -G, or X): for instance GFa -means G(F(a)). Use "GFa" if you really want -to refer to GFa as a proposition.
Conversely, infix -letter operators are not assumed to be operators if they are part of -an identifier: aUb is an atomic proposition, unlike -a U b and (a)U(b).

- -
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
Unary operators
(prefix)		Binary operators
(infix)		Constants
not:! ~and:& && - . /\(strong) until:Utrue:1 - true
eventually:F - <>or:| || - + \/weak until:Wfalse:0 - false
always:G - []implies:-> - --> - =>(weak) release:R - V
next:X ()equivalent:<-> - <--> - <=>strong release:M
xor:^ xor
""" - -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(("" % opt_color) + opt_group + "") - 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 = '%s' % (opt_color, prefix); - if isinstance(desc, list): - s += '%s ' - val = desc[val] - elif isinstance(arg, str): - val = form.getfirst(opt, arg) - s += (('%s ') % - (desc, opt, cgi.escape(val, True))) - else: - if val: - chk = ' checked' - else: - chk = '' - s += '%s' % (opt, chk, - desc) - - column[opt_column].append((s + '')) - globals()[opt] = val - - -column[0].append("Algorithm") -trans = form.getfirst("trans", default_translator) -for opt, desc, color in translators: - if trans == opt: - chk = "checked" - else: - chk = "" - globals()[opt] = chk - s = \ - '%s' - 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 '' -width = range(len(column)) -depth = 0 -for i in width: - depth = max(len(column[i]), depth) -for d in range(depth): - print '' - for i in width: - if d < len(column[i]): - print column[i][d] - else: - print '' - print '' -print '
' - -print '%s' % 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 "

Output

" - -env = spot.default_environment.instance() - -print "

LTL Formula

" - -if show_parse: print '
'
-sys.stdout.flush()
-sys.stderr.flush()
-
-pel = spot.empty_parse_error_list()
-f = spot.parse(formula, pel, env, show_parse)
-if show_parse: print '
' - -if pel: - print '
'
-    err = spot.format_parse_errors(spot.get_cout(), formula, pel)
-    print '
' - -if not f: - print '

Aborting...

' - sys.exit(0) -if pel: - print '

Continuing anyway...

' - -print "

Formula is", f, "

" - -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 "

Reduced formula is", f, "

" - - if show_formula_png: - outfile = spot.ofstream(imgprefix + '-f2.txt') - spot.dotty(outfile, f) - del outfile - render_dot(imgprefix + '-f2') - -print '

Automaton

' - -dict = spot.bdd_dict() - -print '

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.

' -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 '

Degeneralized automaton

' - 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 '

Never claim (for degeneralized automaton)

' - print '
'
-    s = spot.ostringstream()
-    spot.never_claim_reachable(s, degen, f)
-    print cgi.escape(s.str())
-    del s
-    print '
' - sys.stdout.flush() - -if show_dictionnary: - print '

BDD dictionary

' - print '
'
-    sys.stdout.flush()
-    automaton.get_dict().dump(spot.get_cout())
-    print '
' - -if (type(automaton) == spot.tgba_bdd_concrete - and (show_relation_set or show_relation_png)): - print '

Transition relation

' - 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 '

Acceptance relation

' - 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 '

LBTT conversion

' - if degen: - print '

Conversion of the generalized automaton

' - print '
'
-    sys.stdout.flush()
-    spot.lbtt_reachable(spot.get_cout(), automaton)
-    print '
' - if degen: - print '

Conversion of the degeneralized automaton

' - print '
'
-	sys.stdout.flush()
-	spot.lbtt_reachable(spot.get_cout(), degen)
-	print '
' - - -ec = 0 -if draw_acc_run or print_acc_run: - print '

Accepting run

' - 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 ('Cannot parse "' + opt + '" near "' + err - + '".') - 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 += ' on degeneralized automaton' - issba = True - else: - print ('Cannot run ' + emptiness_check - + ' on automata with more than ' + str(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.') - - 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.
" - else: - ec_run = ec_res.accepting_run() - print "accepting run found.
" - if ec_run: - if print_acc_run: - print '
'; sys.stdout.flush()
-                    s = spot.ostringstream()
-                    spot.print_tgba_run(s, ec_a, ec_run)
-                    print cgi.escape(s.str())
-                    del s
-                    print '
'; 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()