Commit cd348275 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

spotcgi: correctly kill ltl3ba on timeout

* python/spot/ (automata): Do not create a session for
every command, this is only needed if automata() is run with a timeout
* python/ajax/ Adjust exclude the main process from
the process group, so that only children are killed on SIGALRM.
* NEWS: Mention the bug.
parent 55eae0d8
......@@ -46,6 +46,9 @@ New in spot (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:
......@@ -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)
def run_dot(basename, ext):
outname = basename + '.' + ext
......@@ -409,7 +409,6 @@ if output_type == 'v3':
child = os.fork()
if child != 0:
......@@ -425,6 +424,8 @@ if child != 0:
os.waitpid(child, 0)
# 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) + "' |"])
automaton = spot.automaton(" ".join(args))
automaton = spot.automaton(" ".join(args), no_sid=True)
except RuntimeError as e:
unbufprint('<div class="error">{}</div>'.format(e))
......@@ -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.
......@@ -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,
None if no_sid else os.setsid,
if timeout is None:
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment