From bdfbf9c5197f23b55bd338b9ad612d66fcf233ef Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 5 Aug 2003 14:17:47 +0000 Subject: [PATCH] * wrap/python/cgi/Makefile.am, wrap/python/cgi/ltl2tgba.in, wrap/python/cgi/README: New files. * wrap/python/Makefile.am (SUBDIRS): Add cgi. * configure.ac: Output wrap/python/cgi/Makefile. --- ChangeLog | 5 + configure.ac | 1 + wrap/python/Makefile.am | 2 +- wrap/python/cgi/.cvsignore | 4 + wrap/python/cgi/Makefile.am | 10 ++ wrap/python/cgi/README | 41 +++++++ wrap/python/cgi/ltl2tgba.in | 227 ++++++++++++++++++++++++++++++++++++ 7 files changed, 289 insertions(+), 1 deletion(-) create mode 100644 wrap/python/cgi/.cvsignore create mode 100644 wrap/python/cgi/Makefile.am create mode 100644 wrap/python/cgi/README create mode 100644 wrap/python/cgi/ltl2tgba.in diff --git a/ChangeLog b/ChangeLog index d64a2f168..9a46e6bdc 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,10 @@ 2003-08-05 Alexandre Duret-Lutz + * wrap/python/cgi/Makefile.am, wrap/python/cgi/ltl2tgba.in, + wrap/python/cgi/README: New files. + * wrap/python/Makefile.am (SUBDIRS): Add cgi. + * configure.ac: Output wrap/python/cgi/Makefile. + * wrap/python/spot.i: Add an ostringstream emulation. 2003-08-04 Alexandre Duret-Lutz diff --git a/configure.ac b/configure.ac index dd36df07e..b436aea00 100644 --- a/configure.ac +++ b/configure.ac @@ -44,6 +44,7 @@ AC_CONFIG_FILES([ src/misc/Makefile wrap/Makefile wrap/python/Makefile + wrap/python/cgi/Makefile wrap/python/tests/Makefile ]) AC_CONFIG_FILES([wrap/python/tests/run], [chmod +x wrap/python/tests/run]) diff --git a/wrap/python/Makefile.am b/wrap/python/Makefile.am index f4852bb8b..68249fe34 100644 --- a/wrap/python/Makefile.am +++ b/wrap/python/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = tests +SUBDIRS = cgi tests AM_CPPFLAGS = -I$(PYTHONINC) -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) diff --git a/wrap/python/cgi/.cvsignore b/wrap/python/cgi/.cvsignore new file mode 100644 index 000000000..5e70e476e --- /dev/null +++ b/wrap/python/cgi/.cvsignore @@ -0,0 +1,4 @@ +Makefile.in +Makefile +ltl2tgba.py + diff --git a/wrap/python/cgi/Makefile.am b/wrap/python/cgi/Makefile.am new file mode 100644 index 000000000..7759195f1 --- /dev/null +++ b/wrap/python/cgi/Makefile.am @@ -0,0 +1,10 @@ +nodist_noinst_SCRIPTS = ltl2tgba.py +EXTRA_DIST = $(srcdir)/ltl2tgba.in README + +ltl2tgba.py: $(srcdir)/ltl2tgba.in + 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 $@ diff --git a/wrap/python/cgi/README b/wrap/python/cgi/README new file mode 100644 index 000000000..6360346d0 --- /dev/null +++ b/wrap/python/cgi/README @@ -0,0 +1,41 @@ +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. diff --git a/wrap/python/cgi/ltl2tgba.in b/wrap/python/cgi/ltl2tgba.in new file mode 100644 index 000000000..4e393fed8 --- /dev/null +++ b/wrap/python/cgi/ltl2tgba.in @@ -0,0 +1,227 @@ +#!@PYTHON@ + +import sys +import os +import cgi +import cgitb; cgitb.enable() + +sys.path.insert(0, '@pythondir@') +# Directory for temporary files (images and other auxiliary files). +imgdir = 'spotimg' + +# Cleanup stale files from our image directory. +os.system('find ' + imgdir + ' -type f -amin +10 -print | xargs rm -f') + +myself = os.environ['SCRIPT_NAME']; +form = cgi.FieldStorage() +filled = form.has_key('formula') +# FIXME: This assumes Apache. +uid = os.environ['UNIQUE_ID']; +imgprefix = imgdir + '/' + uid + +def escaped_print_dot(dict, what): + print '
'; sys.stdout.flush()
+    s = spot.ostringstream()
+    spot.bdd_print_dot(s, dict, what)
+    print cgi.escape(s.str())
+    del s
+    print '
'; sys.stdout.flush() + +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() + + +print "Content-Type: text/html" +print + +os.close(sys.stderr.fileno()) +os.dup2(sys.stdout.fileno(), sys.stderr.fileno()) + +import spot + +print "LTL-to-Büchi test" +print "

Input

" + +formula = form.getfirst('formula', '') + +options = [ + ('show_parse', 'show traces during parsing', 0), + ('show_automaton_dot', 'print Büchi automaton as .dot', 0), + ('show_automaton_gif', 'draw Büchi automaton', 1), + ('show_degen_dot', 'print degeneralized Büchi automaton as .dot', 0), + ('show_degen_gif', 'draw degeneralized Büchi automaton', 0), + ('show_dictionnay', 'print BDD dictionary', 0), + ('show_relation_dot', 'print the transition relation as .dot', 0), + ('show_relation_set', 'print the transition relation as a BDD set', 0), + ('show_relation_gif', 'draw the transition relation', 0), + ('show_acceptance_dot', 'print the acceptance relation as .dot' , 0), + ('show_acceptance_set', 'print the acceptance relation as a BDD set', 0), + ('show_acceptance_gif', 'draw the acceptance relation', 0), + ('show_lbtt', 'convert automaton for LBTT', 0), + ] + +print """

+Formula to translate:
+Options:
""" % (myself, formula) + +for opt, desc, arg, in options: + if formula: + val = int(form.getfirst(opt, 0)) + else: + val = arg + if val: + str = "checked" + else: + str = "" + globals()[opt] = val + print '%s
' % (opt, str, + desc) +print '

' + +if not filled: + sys.exit(0) + +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 '
' + +print '
'
+err = spot.format_parse_errors(spot.get_cout(), formula, pel)
+print '
' + +if not f: + print '

Aborting...

' + sys.exit(0) +if err: + print '

Continuing anyway...

' + +print "

Formula is", f, "

" + +print '

Automaton

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

Building automaton...', +sys.stdout.flush() + +concrete = spot.ltl_to_tgba(f, dict) + +print 'done.

' +sys.stdout.flush() + +if show_automaton_dot: + print '
'; sys.stdout.flush()
+    s = spot.ostringstream()
+    spot.dotty_reachable(s, concrete)
+    print cgi.escape(s.str())
+    del s
+    print '
'; sys.stdout.flush() + +if show_automaton_gif: + outfile = spot.ofstream(imgprefix + '-a.dot') + spot.dotty_reachable(outfile, concrete) + del outfile + os.spawnlp(os.P_WAIT, 'dot', 'dot', '-Tgif', '-o', + imgprefix + '-a.gif', imgprefix + '-a.dot') + print '' + + +if show_degen_dot or show_degen_gif: + print '

Degeneralized automaton

' + degen = spot.tgba_tba_proxy(concrete) + if show_degen_dot: + print '
'; sys.stdout.flush()
+	s = spot.ostringstream()
+	spot.dotty_reachable(s, degen)
+	print cgi.escape(s.str())
+	del s
+	print '
'; sys.stdout.flush() + if show_degen_gif: + outfile = spot.ofstream(imgprefix + '-d.dot') + spot.dotty_reachable(outfile, degen) + del outfile + os.spawnlp(os.P_WAIT, 'dot', 'dot', '-Tgif', '-o', + imgprefix + '-d.gif', imgprefix + '-d.dot') + print '' +else: + degen = 0 + +if show_dictionnay: + print '

BDD dictionary

' + print '
'
+    sys.stdout.flush()
+    concrete.get_dict().dump(spot.get_cout())
+    print '
' + +if show_relation_dot or show_relation_set or show_relation_gif: + print '

Transition relation

' + if show_relation_dot: + escaped_print_dot(concrete.get_dict(), + concrete.get_core_data().relation) + if show_relation_set: + escaped_print_set(concrete.get_dict(), + concrete.get_core_data().relation) + if show_relation_gif: + outfile = spot.ofstream(imgprefix + '-b.dot') + spot.bdd_print_dot(outfile, concrete.get_dict(), + concrete.get_core_data().relation) + del outfile + os.spawnlp(os.P_WAIT, 'dot', 'dot', '-Tgif', '-o', + imgprefix + '-b.gif', imgprefix + '-b.dot') + print '' + +if show_acceptance_dot or show_acceptance_set or show_acceptance_gif: + print '

Acceptance relation

' + if show_acceptance_dot: + escaped_print_dot(concrete.get_dict(), + concrete.get_core_data().accepting_conditions) + if show_acceptance_set: + escaped_print_set(concrete.get_dict(), + concrete.get_core_data().accepting_conditions) + if show_acceptance_gif: + outfile = spot.ofstream(imgprefix + '-c.dot') + spot.bdd_print_dot(outfile, concrete.get_dict(), + concrete.get_core_data().accepting_conditions) + del outfile + os.spawnlp(os.P_WAIT, 'dot', 'dot', '-Tgif', '-o', + imgprefix + '-c.gif', imgprefix + '-c.dot') + print '' + +if show_lbtt: + print '

LBTT conversion

' + if degen: + print '

Conversion of the generalized automaton

' + print '
'
+    sys.stdout.flush()
+    spot.lbtt_reachable(spot.get_cout(), concrete)
+    print '
' + if degen: + print '

Conversion of the degeneralized automaton

' + print '
'
+	sys.stdout.flush()
+	spot.lbtt_reachable(spot.get_cout(), degen)
+	print '
' + +sys.stdout.flush() + +# Make sure degen is cleared before concrete. +del degen +del concrete + +print '
' +print 'Spot @PACKAGE_VERSION@' \ No newline at end of file