spot.in 17.8 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
70
71
# Location of the dot command
dot = '@DOT@'
dot_bgcolor = '-Gbgcolor=#FFFFFF00'

svg_output = False # FIXME: SVG output seems to be working well with
                   #        Firefox only.  We have to figure out how
72
                   #        to get the correct size and transparent
73
74
                   #        background in Chrome.

75
if not script:
76
    # If this is not run as a cgi script, let's start an HTTP server.
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
    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

92
93
    server_address=('',8000)
    if not os.access(imgdir, os.F_OK):
94
95
96
97
        # 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")
98
    httpd = HTTPServer(server_address, MyHandler)
99
    sys.stdout.write("Point your browser to http://localhost:8000/ltl2tgba.html\n")
100
101
102
103
104
    httpd.serve_forever()

import cgi
import cgitb; cgitb.enable()
import signal
105
106
import time
import os.path
107

108
109
110
111
112
# 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'

113
114
sys.stdout.flush()
# Reopen stdout without buffering
115
sys.stdout = os.fdopen(sys.stdout.fileno(), "wb", 0)
116

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

121
# Create the temporary cache directory
122
os.mkdir(tmpdir, 493) # See comment above about 0o755 or 0755.
123

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

129
130
131
132
133
134
135
136
# 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):
    sys.stdout.write(s.encode("utf-8"))


137
138
139
def finish(kill = False):
    # Output the result and exit.
    os.dup2(sys.stderr.fileno(), sys.stdout.fileno())
140
141
142

    cache = open(cachename, "rb", 0)
    sys.stdout.write(cache.read())
143
144
145
146
147
148
149
150
151
152
153
154
155
156

    # 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

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

181
182
183
# Assume Spot is installed
sys.path.insert(0, '@pythondir@')

184
185
if ('SERVER_SOFTWARE' in os.environ and
    os.environ['SERVER_SOFTWARE'].startswith('SimpleHTTP')):
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
    # 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:
201
    # execfile('ltl2tgba.opt') no longuer work with Python 3.
202
    exec(compile(open("ltl2tgba.opt").read(), "ltl2tgba.opt", 'exec'))
203
204
205
206
207
208
209
except IOError:
    pass

import spot
import buddy

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

def reset_alarm():
    signal.alarm(30)

def render_dot(basename):
221
    unbufprint('<div class="dot">')
222
223
224
225
    if svg_output:
        ext = 'svg'
    else:
        ext = 'png'
226
227
228
229
230
231

    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')
232
    reset_alarm()
233
234
    # Create an unused hardlink that point to the output picture
    # just to remember how many cache entries are sharing it.
235
    os.link(outname, tmpdir + "/" + ext)
236
237
    b = cgi.escape(basename)
    if svg_output:
238
239
        unbufprint('<object type="image/svg+xml" data="' + b +
                   '.svg">Your browser does not support SVG.</object>')
240
    else:
241
242
243
        unbufprint('<img src="' + b + '.png"><br>(<a href="' + b
                   + '.txt">dot source</a>)')
    unbufprint('</div>\n')
244

245
246
def render_dot_maybe(dotsrc, dont_run_dot):
    # The dot output is named after the SHA1 of the dot source.
247
248
    # This way we can cache two different requests that generate
    # the same automaton (e.g., when changing a simplification
249
    # option that has no influence).
250
    autprefix = (imgdir + '/' + hashlib.sha1(dotsrc).hexdigest())
251
252
    dotname = autprefix + '.txt'
    if not os.access(dotname, os.F_OK):
253
        dotout = open(dotname, "wb", 0)
254
255
        dotout.write(dotsrc)
        dotout.close()
256
    # Create a unused hardlink that points to the output picture
257
    # just to remember how many cache entries are sharing it.
258
    os.link(dotname, tmpdir + "/txt")
259

260
    if dont_run_dot:
261
262
263
        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')
264
    else:
265
266
267
268
269
270
271
272
        render_dot(autprefix)

def render_automaton(automaton, dont_run_dot, issba, deco = False):
    dotsrc = spot.ostringstream()
    if not deco:
        spot.dotty_reachable(dotsrc, automaton, issba)
    else:
        spot.dotty_reachable(dotsrc, automaton, issba, deco)
273
    render_dot_maybe(dotsrc.str().encode('utf-8'), dont_run_dot)
274

275
276
277
278
def render_formula(f):
    dotsrc = spot.ostringstream()
    spot.dotty(dotsrc, f)
    render_dot_maybe(dotsrc.str(), False)
279
280
281

def print_stats(automaton):
    stats = spot.stats_reachable(automaton)
282
283
284
285
286
287
    unbufprint("<p>%d state" % stats.states)
    if stats.states > 1:
        unbufprint("s")
    unbufprint(", %d transition" % stats.transitions)
    if stats.transitions > 1:
        unbufprint("s")
288
289
    count = automaton.number_of_acceptance_conditions()
    if count > 0:
290
291
292
        unbufprint(", %d acceptance condition" % count)
        if count > 1:
            unbufprint("s")
293
        acc = automaton.all_acceptance_conditions()
294
        unbufprint(": " + spot.bdd_format_accset(automaton.get_dict(), acc))
295
    else:
296
297
        unbufprint(", no acceptance condition (all cycles are accepting)")
    unbufprint("</p>\n")
298
    # Decide whether we will render the automaton or not.
299
    # (A webserver is not a computation center...)
300
301
302
    if stats.states > 64:
        return "Automaton has too much states"
    if float(stats.transitions)/stats.states > 10:
303
        return "Automaton has too much transitions per state"
304
305
306
307
308
309
310
    return False

form = cgi.FieldStorage()

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

# Version requested.
311
if output_type == 'v':
312
    unbufprint('Spot version %s\n' % spot.version())
313
    finish()
314
315
316
317
318
319
320
321
322
323
324
325
326
327

spot.unblock_signal(signal.SIGALRM)
spot.unblock_signal(signal.SIGTERM)
os.setpgrp()
signal.signal(signal.SIGALRM, alarm_handler)
reset_alarm()

formula = form.getfirst('f', '')

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

if pel:
328
    unbufprint('<div class="parse-error">')
329
    err = spot.format_parse_errors(spot.get_cout(), formula, pel)
330
331
332
333
334
    unbufprint('</div>')

# Do not continue if we could not parse anything sensible.
if not f:
    finish()
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353

# Formula simplifications
opt = spot.Reduce_None
for r in form.getlist('r'):
    if r == 'br':
        opt = opt + spot.Reduce_Basics
    elif r == 'si':
        opt = opt + spot.Reduce_Syntactic_Implications
    elif r == 'eu':
        opt = opt + spot.Reduce_Eventuality_And_Universality
    elif r == 'lc':
        opt = opt + spot.Reduce_Containment_Checks_Stronger
if opt != spot.Reduce_None:
    f2 = spot.reduce(f, opt)
    f.destroy()
    f = f2

# Formula manipulation only.
if output_type == 'f':
354
    formula_format = form.getfirst('ff', 'o')
355
356
    # o = Spot, i = Spin, g = GraphViz
    if formula_format == 'o':
357
        unbufprint('<div class="formula spot-format">%s</div>' % f)
358
    elif formula_format == 'i':
359
360
        unbufprint('<div class="formula spin-format">'
                   + spot.to_spin_string(f) + '</div>')
361
    elif formula_format == 'g':
362
        render_formula(f)
363
    finish()
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384

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

dict = spot.bdd_dict()

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,
385
                                    exprop, symb_merge,
386
387
388
389
390
391
392
393
394
395
396
                                    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)

397
398
399
# Should it be displayed as a SBA?
issba = False

400
401
402
403
# Monitor output
if output_type == 'm':
    automaton = spot.scc_filter(automaton)
    automaton = spot.minimize_monitor(automaton)
404
    unbufprint('<div class="automata-stats">')
405
    dont_run_dot = print_stats(automaton)
406
    unbufprint('</div>')
407
    render_automaton(automaton, dont_run_dot, issba)
408
    automaton = 0
409
    finish()
410
411
412
413

# Automaton simplifications
prune_scc = False
wdba_minimize = False
414
simul_minimize = False
415
416
417
418
419
for s in form.getlist('as'):
    if s == 'ps':
        prune_scc = True
    elif s == 'wd':
        wdba_minimize = True
420
421
    elif s == 'rs':
        simul_minimize = True
422
423
424
425
426
427

if output_type == 'a':
    buchi_type = form.getfirst('af', 't')
elif output_type == 'r':
    buchi_type = form.getfirst('ra', 't')
else:
428
    unbufprint("Unkown output type 'o=%s'.\n" % output_type)
429
    automaton = 0
430
    finish()
431
432
433
434
435
436
437
438
439
440
441
442
443

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
    # degeneralization is requested: keeping those that lead to
    # accepting states usually helps.
444
    automaton = spot.scc_filter(automaton, not degen)
445
446
447
448
449
450
451

if wdba_minimize:
    minimized = spot.minimize_obligation_new(automaton, f)
    if minimized:
        automaton = minimized
        minimized = 0
        degen = False # No need to degeneralize anymore
452
        issba = True
453
454
455
456
        simul_minimize = False # No need to simulate anymore

if simul_minimize:
    automaton = spot.simulation(automaton)
457
458
459

if degen or neverclaim:
    degen = spot.tgba_sba_proxy(automaton)
460
    issba = True
461
462
463
464
465
466
467
468
else:
    degen = automaton

# Buchi Automaton Output
if output_type == 'a':
    if buchi_type == 'i':
        s = spot.ostringstream()
        spot.never_claim_reachable(s, degen, f)
469
        unbufprint('<div class="neverclaim">%s</div>' % cgi.escape(s.str()))
470
471
472
        del s
    else: # 't' or 's'
        dont_run_dot = print_stats(degen)
473
        render_automaton(degen, dont_run_dot, issba)
474
475
    degen = 0
    automaton = 0
476
    finish()
477
478
479
480
481
482
483
484
485
486
487

# 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
488
489


490
    err = ""
491
    opt = (form.getfirst('ec', 'Cou99') + "(" +
492
493
494
495
           form.getfirst('eo', '') + ")")
    eci, err = spot.emptiness_check_instantiator.construct(opt)

    if not eci:
496
497
        unbufprint('<div class="parse-error">Cannot parse "' + opt
                         + '" near "' + err + '".</div>')
498
        ec = 0
499
500
501
502
    else:
        ec_a = 0
        n_acc = degen.number_of_acceptance_conditions()
        n_max = eci.max_acceptance_conditions()
503
        n_min = eci.min_acceptance_conditions()
504
        if (n_acc <= n_max):
505
506
507
508
509
510
511
512
            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>')
513
        else:
514
515
516
517
518
            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>')
519
520
521
522
523
524
525
526
        if ec_a:
            ec = eci.instantiate(ec_a)
        else:
            ec = 0

    if ec:
        ec_res = ec.check()
        if not ec_res:
527
            unbufprint('<div class="ec">No accepting run found.</div>')
528
529
        else:
            ec_run = ec_res.accepting_run()
530
            unbufprint('<div class="ec">An accepting run was found.<br/>')
531
532
533
534
            if ec_run:
                if print_acc_run:
                    s = spot.ostringstream()
                    spot.print_tgba_run(s, ec_a, ec_run)
535
536
                    unbufprint('<div class="accrun">%s</div>' %
                               cgi.escape(s.str()))
537
538
539
540
541
                    del s

                if draw_acc_run:
                    deco = spot.tgba_run_dotty_decorator(ec_run)
                    dont_run_dot = print_stats(ec_a)
542
                    render_automaton(ec_a, dont_run_dot, issba, deco)
543
544
545
                    del deco
                del ec_run
            del ec_res
546
            unbufprint('</div>')
547
        del ec
548
        del ec_a
549
550
    degen = 0
    automaton = 0
551
    finish()