spotcgi: correctly kill ltl3ba on timeout

* python/spot/__init__.py (automata): Do not create a session for
every command, this is only needed if automata() is run with a timeout
parameter.
* python/ajax/spotcgi.in: Adjust exclude the main process from
the process group, so that only children are killed on SIGALRM.
* NEWS: Mention the bug.

python/ajax/spotcgi.in

@@ -164,7 +164,7 @@ def finish(kill = False):
 
     if kill:
         # Kill all children
-        os.kill(0, signal.SIGTERM)
+        os.killpg(child, signal.SIGTERM)
     # Should we prune the cache?
     stamp = imgdir + '/cache.stamp'
     now = time.time()
@@ -217,7 +217,7 @@ it has been running for too long.</font>  Please try a shorter formula,
 or different options.
 If you want to benchmark big formulae it is
 better to install Spot on your own computer.</p>\n""")
-    finish(kill = True)
+    finish(kill=True)
 
 def run_dot(basename, ext):
     outname = basename + '.' + ext
@@ -409,7 +409,6 @@ if output_type == 'v3':
 
 spot.unblock_signal(signal.SIGALRM)
 spot.unblock_signal(signal.SIGTERM)
-os.setpgrp()
 
 child = os.fork()
 if child != 0:
@@ -425,6 +424,8 @@ if child != 0:
     os.waitpid(child, 0)
     exit(0)
 
+os.setpgrp()
+
 # Global options
 utf8 = False
 for g in form.getlist('g'):
@@ -608,7 +609,7 @@ elif translator == 'l3':
     g = spot.relabel(f, spot.Pnn, m)
     args.extend(['-f', "'" + spot.str_spin_ltl(g) + "' |"])
     try:
-        automaton = spot.automaton(" ".join(args))
+        automaton = spot.automaton(" ".join(args), no_sid=True)
     except RuntimeError as e:
         unbufprint('<div class="error">{}</div>'.format(e))
         finish()

python/spot/__init__.py

@@ -307,7 +307,7 @@ class formula:
 
 
 def automata(*sources, timeout=None, ignore_abort=True,
-             trust_hoa=True, debug=False):
+             trust_hoa=True, no_sid=False, debug=False):
     """Read automata from a list of sources.
 
     Parameters
@@ -326,6 +326,10 @@ def automata(*sources, timeout=None, ignore_abort=True,
     trust_hoa : bool, optional
         If True (the default), supported HOA properies that
         cannot be easily verified are trusted.
+    no_sid : bool, optional
+        When an automaton is obtained from a subprocess, this
+        subprocess is started from a shell with its own session
+        group (the default) unless no_sid is set to True.
     debug : bool, optional
         Whether to run the parser in debug mode.
 
@@ -386,11 +390,15 @@ def automata(*sources, timeout=None, ignore_abort=True,
             p = None
             proc = None
             if filename[-1] == '|':
+                setsid_maybe = None
+                if not no_sid:
+                    setsid_maybe = os.setsid
                 # universal_newlines for str output instead of bytes
                 # when the pipe is read from Python (which happens
                 # when timeout is set).
                 proc = subprocess.Popen(filename[:-1], shell=True,
-                                        preexec_fn=os.setsid,
+                                        preexec_fn=
+                                        None if no_sid else os.setsid,
                                         universal_newlines=True,
                                         stdout=subprocess.PIPE)
                 if timeout is None: