From cd34827510ce4ece31078e3a2fb1c94e6b40ee0c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 15 Dec 2016 13:35:20 +0100 Subject: [PATCH] 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. --- NEWS | 3 +++ python/ajax/spotcgi.in | 9 +++++---- python/spot/__init__.py | 12 ++++++++++-- 3 files changed, 18 insertions(+), 6 deletions(-) diff --git a/NEWS b/NEWS index 6755d07e6..fa0ff25dc 100644 --- a/NEWS +++ b/NEWS @@ -46,6 +46,9 @@ New in spot 2.2.1.dev (Not yet released) * ltlfilt --from-ltlf should ensure that "alive" holds initially in order to reject empty traces. + * the on-line translator had a bug where a long ltl3ba process would + continue running even after the script had timeout'ed. + New in spot 2.2.1 (2016-11-21) Bug fix: diff --git a/python/ajax/spotcgi.in b/python/ajax/spotcgi.in index 308c5d840..baec65f70 100755 --- a/python/ajax/spotcgi.in +++ b/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. 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.

\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('
{}
'.format(e)) finish() diff --git a/python/spot/__init__.py b/python/spot/__init__.py index e1b820161..5dba7a193 100644 --- a/python/spot/__init__.py +++ b/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: