* wrap/python/spot.i (unblock_signal): New function.

* wrap/python/cgi/ltl2tgba.in (print_footer, alarm_handler)
(reset_alarm): New functions.  Kill the script and its
children if it runs for too long.
(render_dot): Call reset_alarm.

ChangeLog

@@ -1,3 +1,11 @@
+2004-02-05  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* wrap/python/spot.i (unblock_signal): New function.
+	* wrap/python/cgi/ltl2tgba.in (print_footer, alarm_handler)
+	(reset_alarm): New functions.  Kill the script and its
+	children if it runs for too long.
+	(render_dot): Call reset_alarm.
+
 2004-02-03  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* configure.ac, NEWS: Bump version to 0.0p.

wrap/python/cgi/ltl2tgba.in

@@ -25,6 +25,7 @@ import sys
 import os
 import cgi
 import cgitb; cgitb.enable()
+import signal
 
 print "Content-Type: text/html"
 print
@@ -40,6 +41,43 @@ imgdir = 'spotimg'
 import spot
 import buddy
 
+def print_footer():
+    print '<hr>'
+    print 'ltl2tgba.py @PACKAGE_VERSION@; Spot', spot.version()
+
+# 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 +10 -print | xargs rm -f')
@@ -101,6 +139,7 @@ def print_stats(automaton):
 def render_dot(basename):
     os.spawnlp(os.P_WAIT, 'dot', 'dot', '-Tpng', '-Gsize=14,14', '-o',
                basename + '.png', basename + '.dot')
+    reset_alarm()
     print '<img src="' + basename + '.png">'
 
 def render_automaton(basename, automata):
@@ -210,9 +249,8 @@ an indentifier: <code>aUb</code> is an atomic proposition, unlike
     </tr>
     <tr>
       <td align="right">next:</td><td><code>X</code> <code>()</code></td>
-      <td align="right">equivalent:</td><td><code>&lt;-&gt;
+      <td align="right">equivalent:</td><td><code>&lt;-&gt;</code>
-                                            </code> <code>&lt;=&gt;
+                                            <code>&lt;=&gt;</code></td>
-                                            </code></td>
       <td></td><td></td>
       <td></td><td></td>
     </tr>
@@ -252,6 +290,8 @@ print '</TD></TR></TABLE><INPUT type="submit" value="Send"></FORM>'
 if not filled:
     sys.exit(0)
 
+reset_alarm()
+
 print "<hr><H1>Output</H1>"
 
 env = spot.default_environment.instance()
@@ -395,5 +435,4 @@ spot.destroy(f)
 del degen
 del automaton
 
-print '<hr>'
+print_footer()
-print 'ltl2tgba.py @PACKAGE_VERSION@; Spot', spot.version()

wrap/python/spot.i

@@ -30,6 +30,7 @@
 #include <iostream>
 #include <fstream>
 #include <sstream>
+#include <signal.h>
 
 #include "misc/version.hh"
 #include "misc/bddalloc.hh"
@@ -207,4 +208,13 @@ print_on(std::ostream& on, const std::string& what)
   on << what;
 }
 
+int
+unblock_signal(int signum)
+{
+  sigset_t set;
+  sigemptyset(&set);
+  sigaddset(&set, signum);
+  return sigprocmask(SIG_UNBLOCK, &set, 0);
+}
+
 %}