spot.in 23 KB
Newer Older
1
#!@PYTHON@
2
3
# -*- mode: python; coding: utf-8 -*-
# Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
4
# de l'Epita (LRDE).
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
#
# This file is part of Spot, a model checking library.
#
# Spot is free software; you can redistribute it and/or modify it
# under the terms of the GNU General Public License as published by
# the Free Software Foundation; either version 2 of the License, or
# (at your option) any later version.
#
# Spot is distributed in the hope that it will be useful, but WITHOUT
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
# License for more details.
#
# You should have received a copy of the GNU General Public License
# along with Spot; see the file COPYING.  If not, write to the Free
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
# 02111-1307, USA.

import os
24
import sys
25

26
script = ('SCRIPT_NAME' in os.environ)
27
28

if script:
29
30
31
32
33
    # 3600s = 1h
    sys.stdout.write("""Cache-Control: max-age=3600
Content-Type: text/html

""")
34

35
36
37
# Directory for temporary files (images and other auxiliary files).
imgdir = 'spotimg'

38
39
40
41
42
# Cache lookup for the QUERY_STRING
qs = os.getenv('QUERY_STRING')
if qs:
    import hashlib
    # We (optimistically) assume no collision from sha1(qs)
43
    cachedir = imgdir + '/' + hashlib.sha1(qs.encode('utf-8')).hexdigest()
44
    cachename = cachedir + '/html'
45
46
    try:
        # Is this a request we have already processed?
47
48
49
50
51
52
53
        cache = open(cachename, "rb", 0)
        if hasattr(sys.stdout, 'buffer'):
            # Python 3+
            sys.stdout.buffer.write(cache.read())
        else:
            # Python 2.x
            sys.stdout.write(cache.read())
54
55
        # Touch the directory containing the files we used, so
        # it that it survives the browser's cache.
56
        os.utime(cachedir, None)
57
58
59
60
61
62
        exit(0)
    except IOError:
        # We failed to open the file.
        # Let's run the rest of the script to create it.
        pass
elif script:
63
    sys.stdout.write("<b>QUERY_STRING unset!</b>\n")
64
65
    exit(0)

66
67
68
69
# Location of the dot command
dot = '@DOT@'
dot_bgcolor = '-Gbgcolor=#FFFFFF00'

70
71
72
73
74
75
76
77
svg_output = False # SVG output used to working well with Firefox
                   # only.  It now seems to work with recent Chrome
                   # versions as well, but it is still a problem with
                   # Safari, and IE.
output_both = True # Create both PNG and SVG.  If svg_output is False,
                   # the SVG will be given as a link under the PNG.
                   # Otherwise the PNG is used as alternate contents
                   # for the SVG object.
78

79
if not script:
80
    # If this is not run as a cgi script, let's start an HTTP server.
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
    try:
        # Python 3+
        from http.server import CGIHTTPRequestHandler, HTTPServer
    except ImportError:
        # Python 2.x
        from CGIHTTPServer import CGIHTTPRequestHandler
        from BaseHTTPServer import HTTPServer

    class MyHandler(CGIHTTPRequestHandler):
        def is_cgi(self):
            if self.path.startswith('/cgi-bin/spot.py'):
                self.cgi_info = '', self.path[9:]
                return True
            return False

96
97
    server_address=('',8000)
    if not os.access(imgdir, os.F_OK):
98
99
100
101
        # 493 = 0755 but we would have to write 0755 or 0o755
        # depending on the python version...
        os.mkdir(imgdir, 493)
        sys.stdout.write("Directory spotimg/ created.\n")
102
    httpd = HTTPServer(server_address, MyHandler)
103
    sys.stdout.write("Point your browser to http://localhost:8000/ltl2tgba.html\n")
104
105
106
107
108
    httpd.serve_forever()

import cgi
import cgitb; cgitb.enable()
import signal
109
110
import time
import os.path
111

112
113
114
115
116
# We do not output in cachedir directely, in case two
# CGI scripts process the same request concurrently.
tmpdir = cachedir + '-' + str(os.getpid())
cachename = tmpdir + '/html'

117
118
sys.stdout.flush()
# Reopen stdout without buffering
119
sys.stdout = os.fdopen(sys.stdout.fileno(), "wb", 0)
120

121
# Redirect stderr to stdout at a low level (so that
122
# even errors from subprocesses get printed).
123
124
os.dup2(sys.stdout.fileno(), sys.stderr.fileno())

125
# Create the temporary cache directory
126
os.mkdir(tmpdir, 493) # See comment above about 0o755 or 0755.
127

128
# Redirect stdout to the cache file, at a low level
129
# for similar reason.
130
fd = os.open(cachename, os.O_CREAT | os.O_WRONLY, 420) # 420 = 0644
131
132
os.dup2(fd, sys.stdout.fileno())

133
134
135
136
137
# We had to reopen stdout in binary mode to enable unbuffered output,
# (disallowed on text I/O by Python 3.x) so starting now, we are not
# allowed to send strings to sys.stdout.  Always use the following
# method instead.
def unbufprint(s):
138
139
140
141
    if sys.getdefaultencoding() != 'ascii':
        sys.stdout.write(s.encode("utf-8"))
    else:
        sys.stdout.write(s)
142

143
144
145
def finish(kill = False):
    # Output the result and exit.
    os.dup2(sys.stderr.fileno(), sys.stdout.fileno())
146
147
148

    cache = open(cachename, "rb", 0)
    sys.stdout.write(cache.read())
149
150
151
152
153
154
155
156
157
158
159
160
161
162

    # Rename tmpdir to its permanent name for caching purpose.
    # os.rename will fail if cachedir already exist.  Since we tested
    # that initially, it can only happen when two CGI script are
    # processing the same request concurrently.  In that case the
    # other result is as good as ours, so we just ignore the error.
    # (We don't bother removing the temporary directory -- it will be
    # removed by the next cache prune and cannot be created again in
    # the meantime.)
    try:
        os.rename(tmpdir, cachedir)
    except OSError:
        pass

163
    if kill:
164
        # Kill all children
165
        os.kill(0, signal.SIGTERM)
166
167
168
169
    # Should we prune the cache?
    stamp = imgdir + '/cache.stamp'
    now = time.time()
    try:
170
171
        # Prune at most once every hour
        if now - os.path.getmtime(stamp) < 3600:
172
173
            exit(0)
    except OSError:
174
175
        # It's OK if the file did not exist.
        # We will create it.
176
        pass
177
    # Erase all directories that are older than 2 hours, and all
178
179
180
    # files that have only one hardlinks.  Files that have more than
    # one hardlinks are referenced to by directories; so the hardlink
    # count will decrease when the directory is purged.
181
    os.system('find ' + imgdir  + ' -mindepth 1 -maxdepth 1 -mmin +120 '
182
183
              + '\( -type d -o -links 1 \) -exec rm -rf {} +')
    # Create or update the stamp so we know when to run the next prune.
184
    open(stamp, "wb", 0)
185
186
    exit(0)

187
188
189
# Assume Spot is installed
sys.path.insert(0, '@pythondir@')

190
191
if ('SERVER_SOFTWARE' in os.environ and
    os.environ['SERVER_SOFTWARE'].startswith('SimpleHTTP')):
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
    # We might be running from the build tree (but it's not sure).
    # Add the build and source directories first in the search path.
    # If we are not in the right place, python will find the installed
    # libraries later.
    sys.path.insert(0, '@srcdir@/../.libs')
    sys.path.insert(0, '@srcdir@/..')
    sys.path.insert(0, '../.libs')
    sys.path.insert(0, '..')
    # Darwin needs some help in figuring out where non-installed libtool
    # libraries are (on this platform libtool encodes the expected final
    # path of dependent libraries in each library).
    m = '../.libs:@top_builddir@/src/.libs:@top_builddir@/buddy/src/.libs'
    os.environ['DYLD_LIBRARY_PATH'] = m

try:
207
    # execfile('ltl2tgba.opt') no longuer work with Python 3.
208
    exec(compile(open("ltl2tgba.opt").read(), "ltl2tgba.opt", 'exec'))
209
210
211
212
213
214
215
except IOError:
    pass

import spot
import buddy

def alarm_handler(signum, frame):
216
    unbufprint("""<p><font color="red">The script was aborted because
217
218
219
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
220
better to install Spot on your own computer.</p>\n""")
221
    finish(kill = True)
222

223
def run_dot(basename, ext):
224
225
226
227
228
    outname = basename + '.' + ext
    # Do not call "dot" to generate a file that already exists.
    if not os.access(outname, os.F_OK):
        os.spawnlp(os.P_WAIT, dot, dot, dot_bgcolor, '-T' + ext,
                   '-Gsize=8.2,8.2', '-o', outname, basename + '.txt')
229
    # Create a unused hardlink that points to the output picture
230
    # just to remember how many cache entries are sharing it.
231
    os.link(outname, tmpdir + "/" + ext)
232
233
234

def render_dot(basename):
    unbufprint('<div class="dot">')
235
    b = cgi.escape(basename)
236
237
238
239
240
241
242

    if svg_output or output_both:
        run_dot(basename, 'svg')
    if not svg_output or output_both:
        run_dot(basename, 'png')
        pngstr = '<img src="' + b + '.png">'

243
    if svg_output:
244
245
246
247
248
249
250
        unbufprint('<object type="image/svg+xml" data="' + b + '.svg">')
        if output_both:
            unbufprint(pngstr)
        else:
            unbufprint('Your browser does not support SVG.')
        unbufprint('</object>' + '<br>(<a href="' + b
                   + '.txt">dot</a>)')
251
    else:
252
        unbufprint('<img src="' + b + '.png"><br>(<a href="' + b
253
254
255
                   + '.txt">dot</a>)')
        if output_both:
            unbufprint(' (<a href="' + b + '.svg">svg</a>)')
256
    unbufprint('</div>\n')
257

258
259
def render_dot_maybe(dotsrc, dont_run_dot):
    # The dot output is named after the SHA1 of the dot source.
260
261
    # This way we can cache two different requests that generate
    # the same automaton (e.g., when changing a simplification
262
    # option that has no influence).
263
264
    if sys.getdefaultencoding() != 'ascii':
        dotsrc = dotsrc.encode('utf-8')
265
266
267
268
269
270
    # If the text rendering engine (usually Pango) used by dot does
    # not draw overlines correctly, uncomment the following two
    # lines.  Pango 1.28.4 seems not to support combining overline
    # while 1.30 does.
    #import re
    #dotsrc = re.sub(r'(.)(̅|̄)', r'¬\1', dotsrc);
271
    autprefix = (imgdir + '/' + hashlib.sha1(dotsrc).hexdigest())
272
273
    dotname = autprefix + '.txt'
    if not os.access(dotname, os.F_OK):
274
        dotout = open(dotname, "wb", 0)
275
276
        dotout.write(dotsrc)
        dotout.close()
277
    # Create a unused hardlink that points to the output picture
278
    # just to remember how many cache entries are sharing it.
279
    os.link(dotname, tmpdir + "/txt")
280

281
    if dont_run_dot:
282
283
284
        unbufprint('<p>' + dont_run_dot + ''' to be rendered on-line.
However you may download the <a href="''' + cgi.escape(autprefix)
        + '.txt">source in dot format</a> and render it yourself.</p>\n')
285
    else:
286
287
        render_dot(autprefix)

288
def render_automaton(automaton, dont_run_dot, issba, deco = None):
289
    dotsrc = spot.ostringstream()
290
291
    spot.dotty_reachable(dotsrc, automaton, issba, deco)
    render_dot_maybe(dotsrc.str(), dont_run_dot)
292

293
294
295
296
def render_formula(f):
    dotsrc = spot.ostringstream()
    spot.dotty(dotsrc, f)
    render_dot_maybe(dotsrc.str(), False)
297
298
299

def print_stats(automaton):
    stats = spot.stats_reachable(automaton)
300
301
302
303
304
305
    unbufprint("<p>%d state" % stats.states)
    if stats.states > 1:
        unbufprint("s")
    unbufprint(", %d transition" % stats.transitions)
    if stats.transitions > 1:
        unbufprint("s")
306
307
    count = automaton.number_of_acceptance_conditions()
    if count > 0:
308
309
310
        unbufprint(", %d acceptance condition" % count)
        if count > 1:
            unbufprint("s")
311
        acc = automaton.all_acceptance_conditions()
312
        unbufprint(": " + spot.bdd_format_accset(automaton.get_dict(), acc))
313
    else:
314
315
        unbufprint(", no acceptance condition (all cycles are accepting)")
    unbufprint("</p>\n")
316
    # Decide whether we will render the automaton or not.
317
    # (A webserver is not a computation center...)
318
319
320
    if stats.states > 64:
        return "Automaton has too much states"
    if float(stats.transitions)/stats.states > 10:
321
        return "Automaton has too much transitions per state"
322
323
    return False

324
325
326
327
328
329
330
def format_formula(f, kind='div'):
    if utf8:
        s = spot.to_utf8_string(f)
    else:
        s = str(f)
    return '<%s class="formula spot-format">%s</%s>' % (kind, s, kind)

331
332
333
334
335
form = cgi.FieldStorage()

output_type = form.getfirst('o', 'v');

# Version requested.
336
if output_type == 'v':
337
    unbufprint('Spot version %s\n' % spot.version())
338
    finish()
339
340
341
342

spot.unblock_signal(signal.SIGALRM)
spot.unblock_signal(signal.SIGTERM)
os.setpgrp()
343
344
345
346
347
348
349
350
351
352
353
354
355
356

child = os.fork()
if child != 0:
    # In parent.  We are just waiting for the termination of the
    # child, or for the timeout alarm.  On SIGALRM, we will kill the
    # child.
    #
    # We cannot avoid forking, because Python will not deliver a
    # signal when a C function is running.  So if Spot takes too long
    # to translate some formula, it would not get interrupted.
    signal.signal(signal.SIGALRM, alarm_handler)
    signal.alarm(30)
    os.waitpid(child, 0)
    exit(0)
357

358
359
360
361
362
363
364
# Global options
utf8 = False
for g in form.getlist('g'):
    if g == '8':
        utf8 = True
        spot.enable_utf8()

365
366
367
368
369
370
371
formula = form.getfirst('f', '')

env = spot.default_environment.instance()
pel = spot.empty_parse_error_list()
f = spot.parse(formula, pel, env)

if pel:
372
    unbufprint('<div class="parse-error">')
373
    err = spot.format_parse_errors(spot.get_cout(), formula, pel)
374
375
376
377
378
    unbufprint('</div>')

# Do not continue if we could not parse anything sensible.
if not f:
    finish()
379
380

# Formula simplifications
381
382
simpopt = spot.ltl_simplifier_options(False, False, False,
                                      False, False, False, True)
383
dored = False
384
for r in form.getlist('r'):
385
    dored = True
386
    if r == 'br':
387
        simpopt.reduce_basics = True
388
389
    elif r == 'lf':
        simpopt.reduce_size_strictly = False
390
    elif r == 'si':
391
        simpopt.synt_impl = True
392
    elif r == 'eu':
393
        simpopt.event_univ = True
394
    elif r == 'lc':
395
396
397
398
399
        simpopt.containment_checks = True
        simpopt.containment_checks_stronger = True
if dored:
    simp = spot.ltl_simplifier(simpopt)
    f2 = simp.simplify(f)
400
401
    f.destroy()
    f = f2
402
403
    # This also clears the as_bdd() cache.
    simp = None
404
405
406

# Formula manipulation only.
if output_type == 'f':
407
    formula_format = form.getfirst('ff', 'o')
408
    # o = Spot, i = Spin, g = GraphViz, p = properties
409
    if formula_format == 'o':
410
        unbufprint(format_formula(f))
411
    elif formula_format == 'i':
412
413
        unbufprint('<div class="formula spin-format">'
                   + spot.to_spin_string(f) + '</div>')
414
415
416
417
418
        if f.is_psl_formula() and not f.is_ltl_formula():
            s = ''
            if simpopt.reduce_size_strictly:
                s = '<br><b>Try enabling larger formula rewritings.</b>'
            unbufprint('<div class="error">The above formula contains PSL operators that Spin will not understand.%s</div>' % s)
419
    elif formula_format == 'g':
420
        render_formula(f)
421
    elif formula_format == 'p':
422
423
424
425
426
        if utf8:
            s = spot.to_utf8_string(f)
        else:
            s = str(f)
        unbufprint('Properties for ' + format_formula(f, 'span') + '<ul>\n')
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
        for p in spot.list_formula_props(f):
            unbufprint('<li>%s</li>\n' % p)

        # Attempt to refine the hierarchy class using WDBA minimization
        if not f.is_syntactic_safety() or not f.is_syntactic_guarantee():
            dict = spot.bdd_dict()
            automaton = spot.ltl_to_tgba_fm(f, dict, False, True)
            minimized = spot.minimize_obligation_new(automaton, f)
            if minimized:
                g = spot.is_guarantee_automaton(minimized)
                s = spot.is_safety_mwdba(minimized)
                if s and not f.is_syntactic_safety():
                    unbufprint('<li>pathologic safety</li>')
                if g and not f.is_syntactic_guarantee():
                    unbufprint('<li>pathologic guarantee</li>')
                if not f.is_syntactic_obligation():
                    unbufprint('<li>obligation (although not syntactically)</li>')
            else:
                unbufprint('<li>not an obligation</li>')
            minimized = 0
            automaton = 0
        unbufprint('</ul>\n')
449
    finish()
450
451
452
453

# Formula translation.
translator = form.getfirst('t', 'fm')

454
if f.is_psl_formula() and not f.is_ltl_formula() and translator != 'fm':
455
    unbufprint('''<div class="error">The PSL formula %s
456
cannot be translated using this algorithm.  Please use Couveur/FM.'''
457
               % format_formula(f, 'span'))
458
459
    finish()

460
461
dict = spot.bdd_dict()

462
463
464
# Should the automaton be displayed as a SBA?
issba = False

465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
if translator == 'fm':
    exprop = False
    symb_merge = False
    branching_postponement = False
    fair_loop_approx = False
    for fm in form.getlist('fm'):
        if fm == 'od':
            exprop = True
        elif fm == 'sm':
            symb_merge = True
        elif fm == 'bp':
            branching_postponement = True
        elif fm == 'fl':
            fair_loop_approx = True
    automaton = spot.ltl_to_tgba_fm(f, dict,
480
                                    exprop, symb_merge,
481
482
483
484
485
486
487
488
489
490
                                    branching_postponement, fair_loop_approx)
elif translator == 'la':
    automaton = spot.ltl_to_tgba_lacim(f, dict)
    if form.getfirst('la', '') == 'sp':
        automaton.delete_unaccepting_scc()
elif translator == 'ta':
    refined_rules = False
    if form.getfirst('ta', '') == 'lc':
        refined_rules = True
    automaton = spot.ltl_to_taa(f, dict, refined_rules)
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
elif translator == 'l3':
    l3out = '-T'
    l3opt = { '-l', '-P', '-A', '-c', '-C' }
    for lo in form.getfirst('lo', 'T'):
        if lo == 'U':
            l3out = '-U'
            issba = True
    for l3 in form.getlist('l3'):
        if l3 == 'l':
            l3opt.remove('-l')
        elif l3 == 'P':
            l3opt.remove('-P')
        elif l3 == 'A':
            l3opt.remove('-A')
        elif l3 == 'C':
            l3opt.remove('-C')
            l3opt.remove('-c')
        elif l3 == 'M':
            l3opt.add('-M')
        elif l3 == 'S':
            l3opt.add('-S')
    args = ["@LTL3BA@", l3out]
    args.extend(l3opt)
    args.extend(['-f', spot.to_spin_string(f)])
    import subprocess
    l3file = tmpdir + "/aut"
    l3aut = open(l3file, "w+")
    l3proc = subprocess.Popen(args, stdout=l3aut)
    l3aut.close()
    ret = l3proc.wait()
    if ret != 0:
        unbufprint('''<div class="error">ltl3ba exited with error %s</div>'''
                   % ret)
        finish()
    tpel = spot.empty_tgba_parse_error_list()
    automaton = spot.tgba_parse(l3file, tpel, dict, env)
    if tpel:
        unbufprint('''<div class="error">failed to read ltl3ba's output</div>''')
        unbufprint('<div class="parse-error">')
        err = spot.format_tgba_parse_errors(spot.get_cout(), "output", tpel)
        unbufprint('</div>')
        automaton = 0
        finish()
534

535
536
# Monitor output
if output_type == 'm':
537
    issba = False
538
539
    automaton = spot.scc_filter(automaton)
    automaton = spot.minimize_monitor(automaton)
540
    unbufprint('<div class="automata-stats">')
541
    dont_run_dot = print_stats(automaton)
542
    unbufprint('</div>')
543
    render_automaton(automaton, dont_run_dot, issba)
544
    automaton = 0
545
    finish()
546
547
548
549

# Automaton simplifications
prune_scc = False
wdba_minimize = False
550
direct_simul = False
551
552
553
554
555
for s in form.getlist('as'):
    if s == 'ps':
        prune_scc = True
    elif s == 'wd':
        wdba_minimize = True
556
557
    elif s == 'ds':
        direct_simul = True
558
559
560
561
562
563

if output_type == 'a':
    buchi_type = form.getfirst('af', 't')
elif output_type == 'r':
    buchi_type = form.getfirst('ra', 't')
else:
564
    unbufprint("Unkown output type 'o=%s'.\n" % output_type)
565
    automaton = 0
566
    finish()
567
568
569
570
571
572
573
574
575
576
577

degen = False
neverclaim = False
if buchi_type == 's':
    degen = True
elif buchi_type == 'i':
    degen = True
    neverclaim = True

if prune_scc:
    # Do not suppress all useless acceptance conditions if
578
579
580
    # degeneralization or simulation is requested: keeping those that
    # lead to accepting states usually helps.
    automaton = spot.scc_filter(automaton, not (degen or direct_simul))
581
    issba = False
582
583
584
585
586
587
588

if wdba_minimize:
    minimized = spot.minimize_obligation_new(automaton, f)
    if minimized:
        automaton = minimized
        minimized = 0
        degen = False # No need to degeneralize anymore
589
        issba = True
590
        direct_simul = False # No need to simulate anymore
591

592
if direct_simul:
593
    automaton = spot.simulation(automaton)
594
    issba = False
595
596
597

if degen or neverclaim:
    degen = spot.tgba_sba_proxy(automaton)
598
    issba = True
599
600
601
else:
    degen = automaton

602
603
604
if utf8:
    spot.tgba_enable_utf8(automaton)

605
606
607
608
609
# Buchi Automaton Output
if output_type == 'a':
    if buchi_type == 'i':
        s = spot.ostringstream()
        spot.never_claim_reachable(s, degen, f)
610
        unbufprint('<div class="neverclaim">%s</div>' % cgi.escape(s.str()))
611
612
613
        del s
    else: # 't' or 's'
        dont_run_dot = print_stats(degen)
614
        render_automaton(degen, dont_run_dot, issba)
615
616
    degen = 0
    automaton = 0
617
    finish()
618
619
620
621
622
623
624
625
626
627
628

# Buchi Run Output
if output_type == 'r':

    print_acc_run = False
    draw_acc_run = False
    s = form.getfirst('rf', 'p')
    if s == 'p':
        print_acc_run = True
    elif s == 'd':
        draw_acc_run = True
629
630


631
    err = ""
632
    opt = (form.getfirst('ec', 'Cou99') + "(" +
633
634
635
636
           form.getfirst('eo', '') + ")")
    eci, err = spot.emptiness_check_instantiator.construct(opt)

    if not eci:
637
638
        unbufprint('<div class="parse-error">Cannot parse "' + opt
                         + '" near "' + err + '".</div>')
639
        ec = 0
640
641
642
643
    else:
        ec_a = 0
        n_acc = degen.number_of_acceptance_conditions()
        n_max = eci.max_acceptance_conditions()
644
        n_min = eci.min_acceptance_conditions()
645
        if (n_acc <= n_max):
646
647
648
649
650
651
652
653
            if (n_acc >= n_min):
                ec_a = degen
            else:
                unbufprint('<div class="ec-error">Cannot run ' + opt
                           + ' on automata with less than ' + str(n_min)
                           + ' acceptance condition.<br/>Please build '
                           + 'a degeneralized B&uuml;chi automaton if you '
                           + 'want to try this algorithm.</div>')
654
        else:
655
656
657
658
659
            unbufprint('<div class="ec-error">Cannot run ' + opt
                       + ' on automata with more than ' + str(n_max)
                       + ' acceptance condition.<br/>Please build '
                       + 'a degeneralized B&uuml;chi automaton if you '
                       + 'want to try this algorithm.</div>')
660
661
662
663
664
665
666
667
        if ec_a:
            ec = eci.instantiate(ec_a)
        else:
            ec = 0

    if ec:
        ec_res = ec.check()
        if not ec_res:
668
            unbufprint('<div class="ec">No accepting run found.</div>')
669
670
        else:
            ec_run = ec_res.accepting_run()
671
            unbufprint('<div class="ec">An accepting run was found.<br/>')
672
673
674
675
            if ec_run:
                if print_acc_run:
                    s = spot.ostringstream()
                    spot.print_tgba_run(s, ec_a, ec_run)
676
677
                    unbufprint('<div class="accrun">%s</div>' %
                               cgi.escape(s.str()))
678
679
680
681
682
                    del s

                if draw_acc_run:
                    deco = spot.tgba_run_dotty_decorator(ec_run)
                    dont_run_dot = print_stats(ec_a)
683
                    render_automaton(ec_a, dont_run_dot, issba, deco)
684
685
686
                    del deco
                del ec_run
            del ec_res
687
            unbufprint('</div>')
688
        del ec
689
        del ec_a
690
691
    degen = 0
    automaton = 0
692
    finish()