spot.in 24.5 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
it has been running for too long.</font>  Please try a shorter formula,
218
or different options.
219
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
292
293
    if isinstance(automaton, spot.ta):
        spot.dotty_reachable(dotsrc, automaton)
    else:
        spot.dotty_reachable(dotsrc, automaton, issba, deco)
294
    render_dot_maybe(dotsrc.str(), dont_run_dot)
295

296
297
298
299
def render_formula(f):
    dotsrc = spot.ostringstream()
    spot.dotty(dotsrc, f)
    render_dot_maybe(dotsrc.str(), False)
300
301
302

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

328
329
330
331
332
333
334
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)

335
336
337
338
339
form = cgi.FieldStorage()

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

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

344
345
346
347
# ltl3ba's version
if output_type == 'v3':
    import subprocess
    try:
348
        l3proc = subprocess.Popen(['@LTL3BA@', '-v'], stdout=subprocess.PIPE)
349
350
351
352
353
354
355
356
357
358
        (ver, err) = l3proc.communicate()
        err = l3proc.returncode
    except:
        err = 1
    if err != 0:
        unbufprint('not available')
    else:
        unbufprint(ver.replace("\n", "<br>"))
    finish()

359
360
361
spot.unblock_signal(signal.SIGALRM)
spot.unblock_signal(signal.SIGTERM)
os.setpgrp()
362
363
364
365
366
367
368
369
370
371
372
373
374
375

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)
376

377
378
379
380
381
382
383
# Global options
utf8 = False
for g in form.getlist('g'):
    if g == '8':
        utf8 = True
        spot.enable_utf8()

384
385
386
387
388
389
390
formula = form.getfirst('f', '')

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

if pel:
391
    unbufprint('<div class="parse-error">')
392
    err = spot.format_parse_errors(spot.get_cout(), formula, pel)
393
394
395
396
397
    unbufprint('</div>')

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

# Formula simplifications
400
401
simpopt = spot.ltl_simplifier_options(False, False, False,
                                      False, False, False, True)
402
dored = False
403
for r in form.getlist('r'):
404
    dored = True
405
    if r == 'br':
406
        simpopt.reduce_basics = True
407
408
    elif r == 'lf':
        simpopt.reduce_size_strictly = False
409
    elif r == 'si':
410
        simpopt.synt_impl = True
411
    elif r == 'eu':
412
        simpopt.event_univ = True
413
    elif r == 'lc':
414
415
416
417
418
        simpopt.containment_checks = True
        simpopt.containment_checks_stronger = True
if dored:
    simp = spot.ltl_simplifier(simpopt)
    f2 = simp.simplify(f)
419
420
    f.destroy()
    f = f2
421
422
    # This also clears the as_bdd() cache.
    simp = None
423
424
425

# Formula manipulation only.
if output_type == 'f':
426
    formula_format = form.getfirst('ff', 'o')
427
    # o = Spot, i = Spin, g = GraphViz, p = properties
428
    if formula_format == 'o':
429
        unbufprint(format_formula(f))
430
    elif formula_format == 'i':
431
432
        unbufprint('<div class="formula spin-format">'
                   + spot.to_spin_string(f) + '</div>')
433
434
435
436
437
        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)
438
    elif formula_format == 'g':
439
        render_formula(f)
440
    elif formula_format == 'p':
441
442
443
444
445
        if utf8:
            s = spot.to_utf8_string(f)
        else:
            s = str(f)
        unbufprint('Properties for ' + format_formula(f, 'span') + '<ul>\n')
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
        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')
468
    finish()
469
470
471
472

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

473
if f.is_psl_formula() and not f.is_ltl_formula() and translator != 'fm':
474
    unbufprint('''<div class="error">The PSL formula %s
475
cannot be translated using this algorithm.  Please use Couveur/FM.'''
476
               % format_formula(f, 'span'))
477
478
    finish()

479
480
dict = spot.bdd_dict()

481
482
483
# Should the automaton be displayed as a SBA?
issba = False

484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
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,
499
                                    exprop, symb_merge,
500
501
502
503
504
505
506
507
508
509
                                    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)
510
511
elif translator == 'l3':
    l3out = '-T'
512
    l3opt = { '-l', '-P', '-A', '-c', '-C', '-o', '-p' }
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
    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')
531
532
533
534
        elif l3 == 'o':
            l3opt.remove('-o')
        elif l3 == 'p':
            l3opt.remove('-p')
535
536
537
538
539
540
    args = ["@LTL3BA@", l3out]
    args.extend(l3opt)
    args.extend(['-f', spot.to_spin_string(f)])
    import subprocess
    l3file = tmpdir + "/aut"
    l3aut = open(l3file, "w+")
541
542
543
544
545
546
    try:
        l3proc = subprocess.Popen(args, stdout=l3aut)
        ret = l3proc.wait()
    except:
        unbufprint('<div class="error">Failed to run ltl3ba. Is it installed?</div>')
        finish()
547
    if ret != 0:
548
        unbufprint('<div class="error">ltl3ba exited with error %s</div>' % ret)
549
        finish()
550
    l3aut.close()
551
552
553
554
555
556
557
558
559
    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()
560

561
562
# Monitor output
if output_type == 'm':
563
    issba = False
564
565
    automaton = spot.scc_filter(automaton)
    automaton = spot.minimize_monitor(automaton)
566
    unbufprint('<div class="automata-stats">')
567
    dont_run_dot = print_stats(automaton)
568
    unbufprint('</div>')
569
    render_automaton(automaton, dont_run_dot, issba)
570
    automaton = 0
571
    finish()
572
573
574
575

# Automaton simplifications
prune_scc = False
wdba_minimize = False
576
direct_simul = False
577
578
579
580
581
for s in form.getlist('as'):
    if s == 'ps':
        prune_scc = True
    elif s == 'wd':
        wdba_minimize = True
582
583
    elif s == 'ds':
        direct_simul = True
584

585
586
587
ta_type = None
buchi_type = None

588
589
590
591
if output_type == 'a':
    buchi_type = form.getfirst('af', 't')
elif output_type == 'r':
    buchi_type = form.getfirst('ra', 't')
592
593
elif output_type == 't':
    ta_type = form.getfirst('tf', 't')
594
else:
595
    unbufprint("Unkown output type 'o=%s'.\n" % output_type)
596
    automaton = 0
597
    finish()
598
599
600

degen = False
neverclaim = False
601
602

if buchi_type == 's' or ta_type == 't':
603
604
605
606
607
    degen = True
elif buchi_type == 'i':
    degen = True
    neverclaim = True

608
609
610
611
612
if output_type == 't':
    ta_type = form.getfirst('tf', 't')
    if ta_type == 't':
        degen = True

613
614
if prune_scc:
    # Do not suppress all useless acceptance conditions if
615
616
617
    # degeneralization or simulation is requested: keeping those that
    # lead to accepting states usually helps.
    automaton = spot.scc_filter(automaton, not (degen or direct_simul))
618
    issba = False
619
620
621
622
623
624
625

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

629
if direct_simul:
630
    automaton = spot.simulation(automaton)
631
    issba = False
632
633

if degen or neverclaim:
634
    degen = spot.degeneralize(automaton)
635
    issba = True
636
637
638
else:
    degen = automaton

639
if utf8:
640
    spot.tgba_enable_utf8(degen)
641

642
643
644
645
646
# Buchi Automaton Output
if output_type == 'a':
    if buchi_type == 'i':
        s = spot.ostringstream()
        spot.never_claim_reachable(s, degen, f)
647
        unbufprint('<div class="neverclaim">%s</div>' % cgi.escape(s.str()))
648
649
650
        del s
    else: # 't' or 's'
        dont_run_dot = print_stats(degen)
651
        render_automaton(degen, dont_run_dot, issba)
652
653
    degen = 0
    automaton = 0
654
    finish()
655

656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
# Testing automaton Output
if output_type == 't':
    propset = spot.atomic_prop_collect_as_bdd(f, automaton)
    if ta_type == 'a':
        tautomaton = spot.tgba_to_tgta(degen, propset)
        tautomaton = spot.minimize_tgta(tautomaton)
    else:
        tautomaton = spot.tgba_to_ta(degen, propset,
                                     False, False, False, False)
        tautomaton = spot.minimize_ta(tautomaton)
    dont_run_dot = print_stats(tautomaton)
    render_automaton(tautomaton, dont_run_dot, False)
    tautomaton = 0
    degen = 0
    automaton = 0
    finish()

673
674
675
676
677
678
679
680
681
682
# 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
683
684


685
    err = ""
686
    opt = (form.getfirst('ec', 'Cou99') + "(" +
687
688
689
690
           form.getfirst('eo', '') + ")")
    eci, err = spot.emptiness_check_instantiator.construct(opt)

    if not eci:
691
692
        unbufprint('<div class="parse-error">Cannot parse "' + opt
                         + '" near "' + err + '".</div>')
693
        ec = 0
694
695
696
697
    else:
        ec_a = 0
        n_acc = degen.number_of_acceptance_conditions()
        n_max = eci.max_acceptance_conditions()
698
        n_min = eci.min_acceptance_conditions()
699
        if (n_acc <= n_max):
700
701
702
703
704
705
706
707
            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>')
708
        else:
709
710
711
712
713
            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>')
714
715
716
717
718
719
720
721
        if ec_a:
            ec = eci.instantiate(ec_a)
        else:
            ec = 0

    if ec:
        ec_res = ec.check()
        if not ec_res:
722
            unbufprint('<div class="ec">No accepting run found.</div>')
723
724
        else:
            ec_run = ec_res.accepting_run()
725
            unbufprint('<div class="ec">An accepting run was found.<br/>')
726
727
728
729
            if ec_run:
                if print_acc_run:
                    s = spot.ostringstream()
                    spot.print_tgba_run(s, ec_a, ec_run)
730
731
                    unbufprint('<div class="accrun">%s</div>' %
                               cgi.escape(s.str()))
732
733
734
735
736
                    del s

                if draw_acc_run:
                    deco = spot.tgba_run_dotty_decorator(ec_run)
                    dont_run_dot = print_stats(ec_a)
737
                    render_automaton(ec_a, dont_run_dot, issba, deco)
738
739
740
                    del deco
                del ec_run
            del ec_res
741
            unbufprint('</div>')
742
        del ec
743
        del ec_a
744
745
    degen = 0
    automaton = 0
746
    finish()