spot.in 17.6 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 202 203
    # execfile('ltl2tgba.opt') no longuer work with Python 3.
    exec(compile(open("ltl2tgba.opt").read(), "ltl2tgba.opt", 'exec'),
         global_vars, local_vars)
204 205 206 207 208 209 210
except IOError:
    pass

import spot
import buddy

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

def reset_alarm():
    signal.alarm(30)

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

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

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

261
    if dont_run_dot:
262 263 264
        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')
265
    else:
266 267 268 269 270 271 272 273
        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)
274
    render_dot_maybe(dotsrc.str().encode('utf-8'), dont_run_dot)
275

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

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

form = cgi.FieldStorage()

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

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

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:
329
    unbufprint('<div class="parse-error">')
330
    err = spot.format_parse_errors(spot.get_cout(), formula, pel)
331 332 333 334 335
    unbufprint('</div>')

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

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

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

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

401 402 403 404
# Monitor output
if output_type == 'm':
    automaton = spot.scc_filter(automaton)
    automaton = spot.minimize_monitor(automaton)
405
    unbufprint('<div class="automata-stats">')
406
    dont_run_dot = print_stats(automaton)
407
    unbufprint('</div>')
408
    render_automaton(automaton, dont_run_dot, issba)
409
    automaton = 0
410
    finish()
411 412 413 414 415 416 417 418 419 420 421 422 423 424 425

# Automaton simplifications
prune_scc = False
wdba_minimize = False
for s in form.getlist('as'):
    if s == 'ps':
        prune_scc = True
    elif s == 'wd':
        wdba_minimize = True

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

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.
442
    automaton = spot.scc_filter(automaton, not degen)
443 444 445 446 447 448 449

if wdba_minimize:
    minimized = spot.minimize_obligation_new(automaton, f)
    if minimized:
        automaton = minimized
        minimized = 0
        degen = False # No need to degeneralize anymore
450
        issba = True
451 452 453

if degen or neverclaim:
    degen = spot.tgba_sba_proxy(automaton)
454
    issba = True
455 456 457 458 459 460 461 462
else:
    degen = automaton

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

# 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
482 483


484
    err = ""
485
    opt = (form.getfirst('ec', 'Cou99') + "(" +
486 487 488 489
           form.getfirst('eo', '') + ")")
    eci, err = spot.emptiness_check_instantiator.construct(opt)

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

    if ec:
        ec_res = ec.check()
        if not ec_res:
520
            unbufprint('<div class="ec">No accepting run found.</div>')
521 522
        else:
            ec_run = ec_res.accepting_run()
523
            unbufprint('<div class="ec">An accepting run was found.<br/>')
524 525 526 527
            if ec_run:
                if print_acc_run:
                    s = spot.ostringstream()
                    spot.print_tgba_run(s, ec_a, ec_run)
528 529
                    unbufprint('<div class="accrun">%s</div>' %
                               cgi.escape(s.str()))
530 531 532 533 534
                    del s

                if draw_acc_run:
                    deco = spot.tgba_run_dotty_decorator(ec_run)
                    dont_run_dot = print_stats(ec_a)
535
                    render_automaton(ec_a, dont_run_dot, issba, deco)
536 537 538
                    del deco
                del ec_run
            del ec_res
539
            unbufprint('</div>')
540
        del ec
541
        del ec_a
542 543
    degen = 0
    automaton = 0
544
    finish()