diff --git a/wrap/python/ajax/README b/wrap/python/ajax/README index bff90f76e..af7a6dfb1 100644 --- a/wrap/python/ajax/README +++ b/wrap/python/ajax/README @@ -21,6 +21,7 @@ to http://localhost:8000/ltl2tgba.html and you should be OK. After you have killed the server process (e.g. with Control-C), you may want to erase the spotimg/ directory. + Installing on a real web server =============================== @@ -50,7 +51,7 @@ Installing on a real web server 3) In the directory where you have installed spot.py, create a subdirectory called spotimg/. This is where - the script will output its images and other temporary + the script will cache its images and other temporary files. (If you want to change this name, see the imgdir variable at the top of the script.) @@ -58,9 +59,21 @@ Installing on a real web server will run the script when the HTTP server processes the request. - spot.py purges old files (>15min) from this directory - each time it runs. + spot.py purges old files at most once every hour. 4) Copy the directories css/, js/, and logos/ along with ltl2tgba.html to there destination. You may have to adjust a few paths at the top of the html page. + + +Debugging +========= + +The hash string displayed in the web browser is the query string sent +to the CGI script, so you can simulate the call from the command line +with a command like this: + + % export QUERY_STRING="f=a+U+b&r=br&r=lf&r=si&r=eu&o=a&ff=o&mf=d&af=t&ra=t&rf=p&t=fm&fm=od&fm=sm&la=sp&ta=lc&as=ps&ec=Cou99&eo=" + % export SCRIPT_NAME=spot.py + % export SERVER_SOFTWARE=SimpleHTTP + % ./spot.py diff --git a/wrap/python/ajax/css/ltl2tgba.css b/wrap/python/ajax/css/ltl2tgba.css index 9937c9514..a985369d3 100644 --- a/wrap/python/ajax/css/ltl2tgba.css +++ b/wrap/python/ajax/css/ltl2tgba.css @@ -84,6 +84,10 @@ table.ltltable text-transform: capitalize; } +.floatright { + float: right; +} + .ltl2tgba .head .ui-icon { float: right; margin: 1px 0px; diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html index 43c771c2a..71ab39b27 100644 --- a/wrap/python/ajax/ltl2tgba.html +++ b/wrap/python/ajax/ltl2tgba.html @@ -382,7 +382,11 @@ an identifier: aUb is an atomic proposition, unlike
+ +
diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt index 7e5bd7cd9..0b4e649e9 100644 --- a/wrap/python/ajax/protocol.txt +++ b/wrap/python/ajax/protocol.txt @@ -74,3 +74,7 @@ Automaton simplifications (pick many) as=ps Prune SCC as=wd WDBA minimiztion as=ds Direct Simulation reduction + +Global options + + g=8 Enable UTF-8 output. diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 2fed10fcb..084427a7d 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -135,8 +135,10 @@ os.dup2(fd, sys.stdout.fileno()) # allowed to send strings to sys.stdout. Always use the following # method instead. def unbufprint(s): - sys.stdout.write(s.encode("utf-8")) - + if sys.getdefaultencoding() != 'ascii': + sys.stdout.write(s.encode("utf-8")) + else: + sys.stdout.write(s) def finish(kill = False): # Output the result and exit. @@ -262,6 +264,8 @@ def render_dot_maybe(dotsrc, dont_run_dot): # This way we can cache two different requests that generate # the same automaton (e.g., when changing a simplification # option that has no influence). + if sys.getdefaultencoding() != 'ascii': + dotsrc = dotsrc.encode('utf-8') autprefix = (imgdir + '/' + hashlib.sha1(dotsrc).hexdigest()) dotname = autprefix + '.txt' if not os.access(dotname, os.F_OK): @@ -279,13 +283,10 @@ However you may download the %s' % (kind, s, kind) + form = cgi.FieldStorage() output_type = form.getfirst('o', 'v'); @@ -333,6 +341,13 @@ os.setpgrp() signal.signal(signal.SIGALRM, alarm_handler) reset_alarm() +# Global options +utf8 = False +for g in form.getlist('g'): + if g == '8': + utf8 = True + spot.enable_utf8() + formula = form.getfirst('f', '') env = spot.default_environment.instance() @@ -376,14 +391,18 @@ if output_type == 'f': formula_format = form.getfirst('ff', 'o') # o = Spot, i = Spin, g = GraphViz, p = properties if formula_format == 'o': - unbufprint('
%s
' % f) + unbufprint(format_formula(f)) elif formula_format == 'i': unbufprint('
' + spot.to_spin_string(f) + '
') elif formula_format == 'g': render_formula(f) elif formula_format == 'p': - unbufprint('Properties for %s