spotcgi.in 28.2 KB
Newer Older
1
#!@PYTHON@
2
# -*- mode: python; coding: utf-8 -*-
3
# Copyright (C) 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
4
# Développement de l'Epita (LRDE).
5
6
7
8
9
#
# 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
10
# the Free Software Foundation; either version 3 of the License, or
11
12
13
14
15
16
17
18
# (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
19
# along with this program.  If not, see <http://www.gnu.org/licenses/>.
20
21

import os
22
import sys
23

24
script = ('SCRIPT_NAME' in os.environ)
25
26

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

""")
32

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

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

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

69
70
71
72
73
74
75
76
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.
77

78
if not script:
79
    # If this is not run as a cgi script, let's start an HTTP server.
80
81
82
83
84
85
86
87
88
89
    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):
90
            if self.path.startswith('/cgi-bin/spotcgi.py'):
91
92
93
                self.cgi_info = '', self.path[9:]
                return True
            return False
94
    MyHandler.extensions_map[".hoa"] = 'text/x-hoa'
95

96
    server_address=('', 8000)
97
    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/trans.html\n")
104
105
106
107
    httpd.serve_forever()

import cgi
import signal
108
109
import time
import os.path
110

111
112
113
114
115
# 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'

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

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

124
125
126
import cgitb
sys.excepthook = cgitb.Hook(file=sys.stderr)

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

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

135
136
137
138
139
# 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):
140
    if sys.getdefaultencoding() != 'ascii' and type(s) != bytes:
141
142
143
        sys.stdout.write(s.encode("utf-8"))
    else:
        sys.stdout.write(s)
144

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

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

    # 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

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

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

192
193
if ('SERVER_SOFTWARE' in os.environ and
    os.environ['SERVER_SOFTWARE'].startswith('SimpleHTTP')):
194
195
196
197
198
199
    # 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@/..')
    sys.path.insert(0, '../.libs')
200
    sys.path.insert(0, '../spot/.libs')
201
202
203
    sys.path.insert(0, '..')

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

import spot
import buddy

212
213
spot.setup(size='8.2,8.2',fillcolor='#FDEDD3')

214
def alarm_handler(signum, frame):
215
    unbufprint("""<p><font color="red">The script was aborted because
216
it has been running for too long.</font>  Please try a shorter formula,
217
or different options.
218
If you want to benchmark big formulae it is
219
better to install Spot on your own computer.</p>\n""")
220
    finish(kill = True)
221

222
def run_dot(basename, ext):
223
224
225
226
    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,
227
                   '-o', outname, basename + '.txt')
228
    # Create a unused hardlink that points to the output picture
229
    # just to remember how many cache entries are sharing it.
230
    os.link(outname, tmpdir + "/" + ext)
231

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
232
def render_dot(basename, hoaname = None):
233
    unbufprint('<div class="dot">')
234
    b = cgi.escape(basename)
235
236
237
238
239
240
241

    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">'

242
    if svg_output:
243
244
245
246
247
248
249
        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>)')
250
    else:
251
        unbufprint('<img src="' + b + '.png"><br>(<a href="' + b
252
253
254
                   + '.txt">dot</a>)')
        if output_both:
            unbufprint(' (<a href="' + b + '.svg">svg</a>)')
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
255
256
    if hoaname:
        unbufprint(' (<a href="' + hoaname + '">hoa</a>)')
257
    unbufprint('</div>\n')
258

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
def save_hoa(automaton):
    hoasrc = spot.ostringstream()
    spot.print_hoa(hoasrc, automaton, 't' if buchi_type == 't' else '')
    hoasrc = hoasrc.str()
    hoasrc += '\n'
    if sys.getdefaultencoding() != 'ascii':
        hoasrc = hoasrc.encode('utf-8')
    autprefix = (imgdir + '/' + hashlib.sha1(hoasrc).hexdigest())
    hoaname = autprefix + '.hoa'
    if not os.access(hoaname, os.F_OK):
        hoaout = open(hoaname, "wb", 0)
        hoaout.write(hoasrc)
        hoaout.close()
    # Create a unused hardlink that points to the output HOA
    # just to remember how many cache entries are sharing it.
    os.link(hoaname, tmpdir + "/hoa")
    return hoaname

def render_dot_maybe(dotsrc, dont_run_dot, hoaname = None):
278
    # The dot output is named after the SHA1 of the dot source.
279
280
    # This way we can cache two different requests that generate
    # the same automaton (e.g., when changing a simplification
281
    # option that has no influence).
282
283
    if sys.getdefaultencoding() != 'ascii':
        dotsrc = dotsrc.encode('utf-8')
284
285
286
287
288
289
    # 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);
290
    autprefix = (imgdir + '/' + hashlib.sha1(dotsrc).hexdigest())
291
292
    dotname = autprefix + '.txt'
    if not os.access(dotname, os.F_OK):
293
        dotout = open(dotname, "wb", 0)
294
295
        dotout.write(dotsrc)
        dotout.close()
296
    # Create a unused hardlink that points to the output picture
297
    # just to remember how many cache entries are sharing it.
298
    os.link(dotname, tmpdir + "/txt")
299

300
    if dont_run_dot:
301
302
303
        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')
304
    else:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
305
        render_dot(autprefix, hoaname)
306

307
def render_automaton(automaton, dont_run_dot):
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
308
    hoaname = None
309
    dotsrc = spot.ostringstream()
310
    if isinstance(automaton, spot.ta): # TA/GTA
311
        spot.print_dot(dotsrc, automaton)
312
    elif hasattr(automaton, 'get_ta'): # TGTA
313
        spot.print_dot(dotsrc, automaton.get_ta())
314
    else:                       # TGBA
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
315
316
        if not dont_run_dot:
            hoaname = save_hoa(automaton)
317
        spot.print_dot(dotsrc, automaton, '.t' if buchi_type == 't' else '.')
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
318
    render_dot_maybe(dotsrc.str(), dont_run_dot, hoaname)
319

320
321
def render_formula(f):
    dotsrc = spot.ostringstream()
322
    spot.print_dot_psl(dotsrc, f)
323
    render_dot_maybe(dotsrc.str(), False)
324

325
326
def print_stats(automaton, detinfo = False, ta = False):
    if ta: # TA/GTA
327
328
        if hasattr(automaton, 'get_ta'): # TGTA
            automaton = automaton.get_ta()
329
330
331
        stats = spot.stats_reachable(automaton)
        detinfo = False
    else:
332
        if (buchi_type == 't' and automaton.prop_inherently_weak() and
333
334
335
336
            automaton.acc().is_buchi()):
            unbufprint("Note: this is a weak automaton, using transition-based "
                       "or generalized acceptance does not bring any benefit."
                       "</br>")
337
        stats = spot.sub_stats_reachable(automaton)
338
339
340
    unbufprint("<p>%d state" % stats.states)
    if stats.states > 1:
        unbufprint("s")
341
342
343
344
345
346
    if detinfo:
        nondet = spot.count_nondet_states(automaton)
        if nondet == 0:
            unbufprint(" (deterministic)")
        else:
            unbufprint(" (%d nondeterministic)" % nondet)
347
348
349
    if not hasattr(stats, 'transitions'):
        unbufprint(", %d edge" % stats.edges)
        if stats.edges > 1:
350
351
352
            unbufprint("s")
    else:
        unbufprint(", %d edge%s (%d transition%s)"
353
354
                   % (stats.edges, 's' if stats.edges > 1 else '',
                      stats.transitions, 's' if stats.transitions > 1 else ''))
355
356
    if hasattr(automaton, 'get_acceptance'):
        acc = automaton.get_acceptance()
357
358
        if (automaton.is_sba() and automaton.acc().is_buchi() and
            buchi_type != 't'):
359
360
361
            unbufprint(", acceptance condition: Büchi")
        else:
            unbufprint(", acceptance condition: " + str(acc))
362
            if acc.is_t():
363
                unbufprint(" (all cycles are accepting)")
364
    unbufprint("</p>\n")
365
    # Decide whether we will render the automaton or not.
366
    # (A webserver is not a computation center...)
367
    if stats.states > 64:
368
369
370
        return "Automaton has too many states"
    if float(stats.edges)/stats.states > 10:
        return "Automaton has too many edges per state"
371
372
    return False

373
374
def format_formula(f, kind='div'):
    if utf8:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
375
        s = f.to_str('utf8')
376
    else:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
377
        s = f.to_str()
378
379
    return '<%s class="formula spot-format">%s</%s>' % (kind, s, kind)

380
381
382
383
384
form = cgi.FieldStorage()

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

# Version requested.
385
if output_type == 'v':
386
    unbufprint('Spot version %s\n' % spot.version())
387
    finish()
388

389
390
391
392
# ltl3ba's version
if output_type == 'v3':
    import subprocess
    try:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
393
        l3proc = subprocess.Popen(['@LTL3BA@', '-v'], stdout=subprocess.PIPE)
394
        (ver, err) = l3proc.communicate()
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
395
396
397
        # -M[0|1] is new in 1.1.1, and we use it.
        l3proc = subprocess.Popen(['@LTL3BA@', '-h'], stdout=subprocess.PIPE)
        (out, err) = l3proc.communicate()
398
        if out.find(b'-M[') < 0:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
399
400
401
            err = 1
        else:
            err = 0
402
403
404
405
406
    except:
        err = 1
    if err != 0:
        unbufprint('not available')
    else:
407
        unbufprint(ver.replace(b"\n", b"<br>"))
408
409
    finish()

410
411
412
spot.unblock_signal(signal.SIGALRM)
spot.unblock_signal(signal.SIGTERM)
os.setpgrp()
413
414
415
416
417
418
419
420
421
422
423
424
425
426

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

428
429
430
431
432
433
434
# Global options
utf8 = False
for g in form.getlist('g'):
    if g == '8':
        utf8 = True
        spot.enable_utf8()

435
436
437
formula = form.getfirst('f', '')

env = spot.default_environment.instance()
438
pf = spot.parse_infix_psl(formula, env)
439
f = pf.f
440

441
if pf.errors:
442
    # Try the LBT parser in case someone is throwing LBT formulas at us.
443
444
    pg = spot.parse_prefix_ltl(formula, env)
    if pg.errors:
445
        unbufprint('<div class="parse-error">')
446
        err = pf.format_errors(spot.get_cout())
447
448
        unbufprint('</div>')
    else:
449
        f = pg.f
450
451
452
453

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

# Formula simplifications
456
simpopt = spot.tl_simplifier_options(False, False, False,
457
                                      False, False, False, True)
458
dored = False
459
for r in form.getlist('r'):
460
    dored = True
461
    if r == 'br':
462
        simpopt.reduce_basics = True
463
464
    elif r == 'lf':
        simpopt.reduce_size_strictly = False
465
    elif r == 'si':
466
        simpopt.synt_impl = True
467
    elif r == 'eu':
468
        simpopt.event_univ = True
469
    elif r == 'lc':
470
471
472
        simpopt.containment_checks = True
        simpopt.containment_checks_stronger = True
if dored:
473
474
    # Not keeping the ltl simplifier aive will also clear the as_bdd()
    # cache.
475
    f = spot.tl_simplifier(simpopt).simplify(f)
476
477
478

# Formula manipulation only.
if output_type == 'f':
479
    formula_format = form.getfirst('ff', 'o')
480
    # o = Spot, i = Spin, l = LBT, g = GraphViz, p = properties
481
    if formula_format == 'o':
482
        unbufprint(format_formula(f))
483
    elif formula_format == 'i':
484
        unbufprint('<div class="formula spin-format">'
485
                   + spot.str_spin_ltl(f) + '</div>')
486
487
488
489
490
        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)
491
492
493
494
    elif formula_format == 'l':
        if not f.is_ltl_formula():
            unbufprint('<div class="error">PSL formulas cannot be expressed in this format.</div>')
        else:
495
            unbufprint('<div class="formula lbt-format">' + spot.str_lbt_ltl(f) + '</div>')
496
    elif formula_format == 'g':
497
        render_formula(f)
498
    elif formula_format == 'p':
499
        if utf8:
500
            s = spot.str_utf8_psl(f)
501
502
503
        else:
            s = str(f)
        unbufprint('Properties for ' + format_formula(f, 'span') + '<ul>\n')
504
505
506
507
508
509
510
        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)
511
512
            minimized = spot.minimize_obligation(automaton, f)
            if minimized != automaton:
513
                g = spot.is_terminal_automaton(minimized)
514
515
516
517
518
519
520
521
522
523
524
                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
525
526
527
528
529
        if not f.is_syntactic_stutter_invariant():
            if spot.is_stutter_invariant(f):
                unbufprint('<li>stutter invariant</li>')
            else:
                unbufprint('<li>stutter sensitive</li>')
530
        unbufprint('</ul>\n')
531
    finish()
532
533
534
535

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

536
if f.is_psl_formula() and not f.is_ltl_formula() and translator != 'fm':
537
    unbufprint('''<div class="error">The PSL formula %s
538
cannot be translated using this algorithm.  Please use Couveur/FM.'''
539
               % format_formula(f, 'span'))
540
541
    finish()

542
dict = spot.make_bdd_dict()
543

544
545
546
if output_type == 't' and not spot.is_stutter_invariant(f):
    unbufprint('<b>Warning:</b> Testing automata are only valid '
               + 'for stutter-insensitive formulas, but the input is not.</br>')
547

548
549
550
# Should the automaton be displayed as a SBA?
issba = False

551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
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,
566
                                    exprop, symb_merge,
567
568
569
570
571
                                    branching_postponement, fair_loop_approx)
elif translator == 'ta':
    refined_rules = False
    if form.getfirst('ta', '') == 'lc':
        refined_rules = True
572
573
    automaton = spot.ensure_digraph(spot.ltl_to_taa(f, dict, refined_rules))

574
elif translator == 'l3':
575
    l3out = '-H2'
576
    # 1.0.1 had determinization and simulation turned off by default,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
577
578
    # we need -M0 and -S0 with 1.1.1 for the same effect
    l3opt = { '-l', '-P', '-A', '-c', '-C', '-o', '-p', '-M0', '-S0' }
579
580
    for lo in form.getfirst('lo', 'T'):
        if lo == 'U':
581
            l3out = '-H3'
582
583
584
585
586
587
588
589
590
591
592
593
            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':
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
594
595
            l3opt.remove('-M0')
            l3opt.add('-M1')
596
        elif l3 == 'S':
597
598
            l3opt.remove('-S0')
            l3opt.add('-S2')  # was -S in 1.0.1
599
600
601
602
        elif l3 == 'o':
            l3opt.remove('-o')
        elif l3 == 'p':
            l3opt.remove('-p')
603
604
    args = ["@LTL3BA@", l3out]
    args.extend(l3opt)
605
606
607
608
609
610
611
612
613
    # Relabel the formula in case it contains unsupported atomic
    # propositions (e.g., starting with _ or double-quoted).
    m = spot.relabeling_map()
    g = spot.relabel(f, spot.Pnn, m)
    args.extend(['-f', "'" + spot.str_spin_ltl(g) + "' |"])
    try:
        automaton = spot.automaton(" ".join(args))
    except RuntimeError as e:
        unbufprint('<div class="error">{}</div>'.format(e))
614
        finish()
615
    spot.relabel_here(automaton, m)
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
elif translator == 'cs':
    donot_inject = False
    cs_nowdba = True
    cs_nosimul = True
    cs_early_start = False
    for cs in form.getlist('cs'):
        if cs == 'c':
            donot_inject = True
        elif cs == 'w':
            cs_nowdba = False
        elif cs == 's':
            cs_nosimul = False
        elif cs == 'e':
            cs_early_start = True

    automaton = spot.compsusp(f, dict, cs_nowdba, cs_nosimul,
                              cs_early_start, donot_inject)
633
634
635
else:
    unbufprint('''<div class="error">unsupported translator</div>''')
    finish()
636

637
638
buchi_type = None

639
640
# Monitor output
if output_type == 'm':
641
642
643
644
645
646
647
648
649
    issba = True
    mf = form.getfirst('mf', 'd')
    pp = spot.postprocessor()
    pp.set_type(spot.postprocessor.Monitor)
    if mf == 'd':
        pp.set_pref(spot.postprocessor.Deterministic)
    elif mf == 'n':
        pp.set_pref(spot.postprocessor.Small)
    automaton = pp.run(automaton, f)
650
    unbufprint('<div class="automata-stats">')
651
    dont_run_dot = print_stats(automaton)
652
    unbufprint('</div>')
653
    automaton.set_name(str(f))
654
    render_automaton(automaton, dont_run_dot)
655
    automaton = 0
656
    finish()
657
658
659
660

# Automaton simplifications
prune_scc = False
wdba_minimize = False
661
direct_simul = False
662
663
reverse_simul = False
iterated_simul = False
664
665
666
667
668
for s in form.getlist('as'):
    if s == 'ps':
        prune_scc = True
    elif s == 'wd':
        wdba_minimize = True
669
670
    elif s == 'ds':
        direct_simul = True
671
672
673
674
    elif s == 'rs':
        reverse_simul = True
    elif s == 'is':
        iterated_simul = True
675

676
677
ta_type = None

678
679
680
681
if output_type == 'a':
    buchi_type = form.getfirst('af', 't')
elif output_type == 'r':
    buchi_type = form.getfirst('ra', 't')
682
683
elif output_type == 't':
    ta_type = form.getfirst('tf', 't')
684
else:
685
    unbufprint("Unkown output type 'o=%s'.\n" % output_type)
686
    automaton = 0
687
    finish()
688
689
690

degen = False
neverclaim = False
691
692

if buchi_type == 's' or ta_type == 't':
693
694
695
696
697
    degen = True
elif buchi_type == 'i':
    degen = True
    neverclaim = True

698
699
if output_type == 't' and ta_type == 't':
    degen = True
700

701
702
if prune_scc:
    # Do not suppress all useless acceptance conditions if
703
704
    # degeneralization or simulation is requested: keeping those that
    # lead to accepting states usually helps.
705
706
707
708
    automaton = spot.scc_filter(automaton, not (degen
                                                or direct_simul
                                                or reverse_simul
                                                or iterated_simul))
709
710

if wdba_minimize:
711
712
    minimized = spot.minimize_obligation(automaton, f)
    if minimized != automaton:
713
714
715
        automaton = minimized
        minimized = 0
        degen = False # No need to degeneralize anymore
716
        direct_simul = False # No need to simulate anymore
717
718
        reverse_simul = False
        iterated_simul = False
719

720
if direct_simul and not iterated_simul:
721
    automaton = spot.simulation(automaton)
722
723
724
725
726
727
728
729
730
if reverse_simul and not iterated_simul:
    automaton = spot.cosimulation(automaton)
if iterated_simul:
    automaton = spot.iterated_simulations(automaton)

if prune_scc and (direct_simul or reverse_simul):
    # Make a second pass after the simulation, since these might leave
    # extra acceptance conditions.
    automaton = spot.scc_filter(automaton, not degen)
731
732

if degen or neverclaim:
733
    degen = spot.degeneralize(automaton)
734
735
736
737
738
739
740
else:
    degen = automaton

# Buchi Automaton Output
if output_type == 'a':
    if buchi_type == 'i':
        s = spot.ostringstream()
741
        spot.print_never_claim(s, degen)
742
        unbufprint('<div class="neverclaim">%s</div>' % cgi.escape(s.str()))
743
744
        del s
    else: # 't' or 's'
745
        dont_run_dot = print_stats(degen, True)
746
        automaton.set_name(str(f))
747
        render_automaton(degen, dont_run_dot)
748
749
    degen = 0
    automaton = 0
750
    finish()
751

752
753
# Testing automaton Output
if output_type == 't':
754
755
756
757
758
759
760
761
762
763
    livelock = False
    singlepass = False
    bisimulation = False
    for to in form.getlist('to'):
        if to == 'l':
            livelock = True
        elif to == 's':
            singlepass = True
        elif to == 'm':
            bisimulation = True
764
765
766
    propset = spot.atomic_prop_collect_as_bdd(f, automaton)
    if ta_type == 'a':
        tautomaton = spot.tgba_to_tgta(degen, propset)
767
768
        if bisimulation:
            tautomaton = spot.minimize_tgta(tautomaton)
769
    else:
770
771
        tautomaton = spot.tgba_to_ta(degen, propset, ta_type == 't',
                                     True, singlepass, livelock)
772
773
        if bisimulation:
            tautomaton = spot.minimize_ta(tautomaton)
774
    dont_run_dot = print_stats(tautomaton, ta = True)
775
    render_automaton(tautomaton, dont_run_dot)
776
777
778
779
780
    tautomaton = 0
    degen = 0
    automaton = 0
    finish()

781
782
783
784
# Buchi Run Output
if output_type == 'r':

    print_acc_run = False
785
    s = form.getfirst('rf', 'd')
786
    draw_acc_run = False
787
788
789
790
    if s == 'p':
        print_acc_run = True
    elif s == 'd':
        draw_acc_run = True
791

792
    err = ""
793
    opt = (form.getfirst('ec', 'Cou99') + "(" +
794
           form.getfirst('eo', '') + ")")
795
    eci, err = spot.make_emptiness_check_instantiator(opt)
796
797

    if not eci:
798
799
        unbufprint('<div class="parse-error">Cannot parse "' + opt
                         + '" near "' + err + '".</div>')
800
        ec = 0
801
802
    else:
        ec_a = 0
803
        n_acc = degen.acc().num_sets()
804
805
        n_max = eci.max_sets()
        n_min = eci.min_sets()
806
        if (n_acc <= n_max):
807
808
809
810
811
            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)
812
                           + ' acceptance set.<br/>Please build '
813
814
                           + 'a degeneralized B&uuml;chi automaton if you '
                           + 'want to try this algorithm.</div>')
815
        else:
816
817
            unbufprint('<div class="ec-error">Cannot run ' + opt
                       + ' on automata with more than ' + str(n_max)
818
                       + ' acceptance set.<br/>Please build '
819
820
                       + 'a degeneralized B&uuml;chi automaton if you '
                       + 'want to try this algorithm.</div>')
821
822
823
824
825
826
827
828
        if ec_a:
            ec = eci.instantiate(ec_a)
        else:
            ec = 0

    if ec:
        ec_res = ec.check()
        if not ec_res:
829
            unbufprint('<div class="ec">No accepting run found.</div>')
830
831
        else:
            ec_run = ec_res.accepting_run()
832
            unbufprint('<div class="ec">An accepting run was found.<br/>')
833
834
            if ec_run:
                if print_acc_run:
835
                    unbufprint('<div class="accrun">%s</div>' %
836
                               cgi.escape(str(ec_run)))
837
                if draw_acc_run:
838
                    render_automaton(ec_run.as_twa(), False)
839
840
                del ec_run
            del ec_res
841
            unbufprint('</div>')
842
    finish()