Commit 34f49a86 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Preliminary implementation of an ajax-based ltl2tgba translator.

* configure.ac: Output wrap/python/ajax/Makefile.
* wrap/python/Makefile.am (SUBDIRS): Add ajax.
* wrap/python/ajax/Makefile.am, wrap/python/ajax/README,
wrap/python/ajax/ltl2tgba.html, wrap/python/ajax/spot.in: New files.
* wrap/python/ajax/css/, wrap/python/ajax/js,
wrap/python/ajax/logos: New directories.
* README: Document wrap/python/ajax/.
parent dc2a89f8
This diff is collapsed.
/*
* TipTip
* Copyright 2010 Drew Wilson
* www.drewwilson.com
* code.drewwilson.com/entry/tiptip-jquery-plugin
*
* Version 1.3 - Updated: Mar. 23, 2010
*
* This Plug-In will create a custom tooltip to replace the default
* browser tooltip. It is extremely lightweight and very smart in
* that it detects the edges of the browser window and will make sure
* the tooltip stays within the current window size. As a result the
* tooltip will adjust itself to be displayed above, below, to the left
* or to the right depending on what is necessary to stay within the
* browser window. It is completely customizable as well via CSS.
*
* This TipTip jQuery plug-in is dual licensed under the MIT and GPL licenses:
* http://www.opensource.org/licenses/mit-license.php
* http://www.gnu.org/licenses/gpl.html
*/
(function($){$.fn.tipTip=function(options){var defaults={activation:"hover",keepAlive:false,maxWidth:"200px",edgeOffset:3,defaultPosition:"bottom",delay:400,fadeIn:200,fadeOut:200,attribute:"title",content:false,enter:function(){},exit:function(){}};var opts=$.extend(defaults,options);if($("#tiptip_holder").length<=0){var tiptip_holder=$('<div id="tiptip_holder" style="max-width:'+opts.maxWidth+';"></div>');var tiptip_content=$('<div id="tiptip_content"></div>');var tiptip_arrow=$('<div id="tiptip_arrow"></div>');$("body").append(tiptip_holder.html(tiptip_content).prepend(tiptip_arrow.html('<div id="tiptip_arrow_inner"></div>')))}else{var tiptip_holder=$("#tiptip_holder");var tiptip_content=$("#tiptip_content");var tiptip_arrow=$("#tiptip_arrow")}return this.each(function(){var org_elem=$(this);if(opts.content){var org_title=opts.content}else{var org_title=org_elem.attr(opts.attribute)}if(org_title!=""){if(!opts.content){org_elem.removeAttr(opts.attribute)}var timeout=false;if(opts.activation=="hover"){org_elem.hover(function(){active_tiptip()},function(){if(!opts.keepAlive){deactive_tiptip()}});if(opts.keepAlive){tiptip_holder.hover(function(){},function(){deactive_tiptip()})}}else if(opts.activation=="focus"){org_elem.focus(function(){active_tiptip()}).blur(function(){deactive_tiptip()})}else if(opts.activation=="click"){org_elem.click(function(){active_tiptip();return false}).hover(function(){},function(){if(!opts.keepAlive){deactive_tiptip()}});if(opts.keepAlive){tiptip_holder.hover(function(){},function(){deactive_tiptip()})}}function active_tiptip(){opts.enter.call(this);tiptip_content.html(org_title);tiptip_holder.hide().removeAttr("class").css("margin","0");tiptip_arrow.removeAttr("style");var top=parseInt(org_elem.offset()['top']);var left=parseInt(org_elem.offset()['left']);var org_width=parseInt(org_elem.outerWidth());var org_height=parseInt(org_elem.outerHeight());var tip_w=tiptip_holder.outerWidth();var tip_h=tiptip_holder.outerHeight();var w_compare=Math.round((org_width-tip_w)/2);var h_compare=Math.round((org_height-tip_h)/2);var marg_left=Math.round(left+w_compare);var marg_top=Math.round(top+org_height+opts.edgeOffset);var t_class="";var arrow_top="";var arrow_left=Math.round(tip_w-12)/2;if(opts.defaultPosition=="bottom"){t_class="_bottom"}else if(opts.defaultPosition=="top"){t_class="_top"}else if(opts.defaultPosition=="left"){t_class="_left"}else if(opts.defaultPosition=="right"){t_class="_right"}var right_compare=(w_compare+left)<parseInt($(window).scrollLeft());var left_compare=(tip_w+left)>parseInt($(window).width());if((right_compare&&w_compare<0)||(t_class=="_right"&&!left_compare)||(t_class=="_left"&&left<(tip_w+opts.edgeOffset+5))){t_class="_right";arrow_top=Math.round(tip_h-13)/2;arrow_left=-12;marg_left=Math.round(left+org_width+opts.edgeOffset);marg_top=Math.round(top+h_compare)}else if((left_compare&&w_compare<0)||(t_class=="_left"&&!right_compare)){t_class="_left";arrow_top=Math.round(tip_h-13)/2;arrow_left=Math.round(tip_w);marg_left=Math.round(left-(tip_w+opts.edgeOffset+5));marg_top=Math.round(top+h_compare)}var top_compare=(top+org_height+opts.edgeOffset+tip_h+8)>parseInt($(window).height()+$(window).scrollTop());var bottom_compare=((top+org_height)-(opts.edgeOffset+tip_h+8))<0;if(top_compare||(t_class=="_bottom"&&top_compare)||(t_class=="_top"&&!bottom_compare)){if(t_class=="_top"||t_class=="_bottom"){t_class="_top"}else{t_class=t_class+"_top"}arrow_top=tip_h;marg_top=Math.round(top-(tip_h+5+opts.edgeOffset))}else if(bottom_compare|(t_class=="_top"&&bottom_compare)||(t_class=="_bottom"&&!top_compare)){if(t_class=="_top"||t_class=="_bottom"){t_class="_bottom"}else{t_class=t_class+"_bottom"}arrow_top=-12;marg_top=Math.round(top+org_height+opts.edgeOffset)}if(t_class=="_right_top"||t_class=="_left_top"){marg_top=marg_top+5}else if(t_class=="_right_bottom"||t_class=="_left_bottom"){marg_top=marg_top-5}if(t_class=="_left_top"||t_class=="_left_bottom"){marg_left=marg_left+5}tiptip_arrow.css({"margin-left":arrow_left+"px","margin-top":arrow_top+"px"});tiptip_holder.css({"margin-left":marg_left+"px","margin-top":marg_top+"px"}).attr("class","tip"+t_class);if(timeout){clearTimeout(timeout)}timeout=setTimeout(function(){tiptip_holder.stop(true,true).fadeIn(opts.fadeIn)},opts.delay)}function deactive_tiptip(){opts.exit.call(this);if(timeout){clearTimeout(timeout)}tiptip_holder.fadeOut(opts.fadeOut)}}})}})(jQuery);
\ No newline at end of file
This diff is collapsed.
#!@PYTHON@
# -*- mode: python; coding: iso-8859-1 -*-
# Copyright (C) 2011 Laboratoire de Recherche et Dveloppement de
# l'Epita (LRDE).
#
# 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
# Directory for temporary files (images and other auxiliary files).
imgdir = 'spotimg'
# 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
# to get the correct size and transparent
# background in Chrome.
from CGIHTTPServer import CGIHTTPRequestHandler
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
if not os.environ.has_key('SCRIPT_NAME'):
# If this is not run as a cgi script, let's start an HTTP server.
from BaseHTTPServer import HTTPServer
server_address=('',8000)
if not os.access(imgdir, os.F_OK):
os.mkdir(imgdir, 0755)
print "Directory spotimg/ created."
httpd = HTTPServer(server_address, MyHandler)
print "Point your browser to http://localhost:8000/ltl2tgba.html"
httpd.serve_forever()
import sys
import cgi
import cgitb; cgitb.enable()
import signal
import uuid
print "Content-Type: text/html"
print
# Redirect stderr to stdout.
os.close(sys.stderr.fileno())
os.dup2(sys.stdout.fileno(), sys.stderr.fileno())
# Assume Spot is installed
sys.path.insert(0, '@pythondir@')
if (os.environ.has_key('SERVER_SOFTWARE') and
os.environ['SERVER_SOFTWARE'].startswith(MyHandler.server_version)):
# 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:
execfile('ltl2tgba.opt')
except IOError:
pass
import spot
import buddy
def alarm_handler(signum, frame):
print """<p><font color="red">The script was aborted because
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
better to install Spot on your own computer.</p>"""
sys.stdout.flush()
os.kill(0, signal.SIGTERM)
def reset_alarm():
signal.alarm(30)
def render_dot(basename):
print '<div class="dot">'
if svg_output:
ext = 'svg'
else:
ext = 'png'
os.spawnlp(os.P_WAIT, dot, dot, dot_bgcolor, '-T' + ext,
'-Gsize=8.2,8.2', '-o', basename + '.' + ext, basename + '.txt')
reset_alarm()
b = cgi.escape(basename)
if svg_output:
print ('<object type="image/svg+xml" data="' + b + '.svg">'
+ 'Your browser does not support SVG.</object>')
else:
print ('<img src="' + b + '.png"><br>(<a href="' + b
+ '.txt">dot source</a>)')
print '</div>'
sys.stdout.flush()
def render_automaton(basename, automata, dont_run_dot, deco = False):
outfile = spot.ofstream(basename + '.txt')
if not deco:
spot.dotty_reachable(outfile, automata)
else:
spot.dotty_reachable(outfile, automata, deco)
del outfile
if dont_run_dot:
print ('<p>' + dont_run_dot + ''' to be rendered on-line. However
you may download the <a href="''' + cgi.escape(basename)
+ '.txt">source in dot format</a> and render it yourself.')
else:
render_dot(basename)
def print_stats(automaton):
stats = spot.stats_reachable(automaton)
print "<p>", stats.states,
if stats.states <= 1:
print " state,",
else:
print " states,",
print stats.transitions,
if stats.transitions <= 1:
print " transition,",
else:
print " transitions,",
# compute the number of acceptance conditions
count = automaton.number_of_acceptance_conditions()
if count > 0:
print count,
if count <= 1:
print "acceptance condition:",
else:
print "acceptance conditions:",
sys.stdout.flush()
acc = automaton.all_acceptance_conditions()
spot.bdd_print_accset(spot.get_cout(), automaton.get_dict(), acc)
else:
print "no acceptance condition (all cycles are accepting)"
print "</p>"
sys.stdout.flush()
# Decide whether we will render the automaton or not.
# (A webserver is not a calcul center...)
if stats.states > 64:
return "Automaton has too much states"
if float(stats.transitions)/stats.states > 10:
return "Automaton has too much transitions per states"
return False
form = cgi.FieldStorage()
uid = str(uuid.uuid1())
imgprefix = imgdir + '/' + uid
output_type = form.getfirst('o', 'v');
# Version requested.
if output_type == 'v':
print 'Spot version ' + spot.version()
exit(0)
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:
print '<div class="parse-error">'
err = spot.format_parse_errors(spot.get_cout(), formula, pel)
print '</div>'
# 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':
formula_format = form.getfirst('ff', 'o')
# o = Spot, i = Spin, g = GraphViz
if formula_format == 'o':
print '<div class="formula spot-format">%s</div>' % f
elif formula_format == 'i':
print ('<div class="formula spin-format">'
+ spot.to_spin_string(f) + '</div>')
elif formula_format == 'g':
outfile = spot.ofstream(imgprefix + '-f.txt')
spot.dotty(outfile, f)
del outfile
render_dot(imgprefix + '-f')
exit(0)
# 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,
exprop, symb_merge,
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)
# Monitor output
if output_type == 'm':
automaton = spot.scc_filter(automaton)
automaton = spot.minimize_monitor(automaton)
print '<div class="automata-stats">'
dont_run_dot = print_stats(automaton)
print '</div>'
render_automaton(imgprefix + '-a', automaton, dont_run_dot)
automaton = 0
exit(0)
# 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:
print "Unkown output type 'o=%s'." % output_type
automaton = 0
exit(0)
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.
automaton = spot.scc_filter(automaton, degen)
if wdba_minimize:
minimized = spot.minimize_obligation_new(automaton, f)
if minimized:
automaton = minimized
minimized = 0
degen = False # No need to degeneralize anymore
if degen or neverclaim:
degen = spot.tgba_sba_proxy(automaton)
else:
degen = automaton
# Buchi Automaton Output
if output_type == 'a':
if buchi_type == 'i':
s = spot.ostringstream()
spot.never_claim_reachable(s, degen, f)
print '<div class="neverclaim">%s</div>' % cgi.escape(s.str())
del s
else: # 't' or 's'
dont_run_dot = print_stats(degen)
render_automaton(imgprefix + '-a', degen, dont_run_dot)
degen = 0
automaton = 0
exit(0)
# 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
err = ""
opt = (form.getfirst('ec', 'Cou99') + "(" +
form.getfirst('eo', '') + ")")
eci, err = spot.emptiness_check_instantiator.construct(opt)
if not eci:
print ('<div class="parse-error">Cannot parse "' + opt + '" near "'
+ err + '".</div>')
else:
ec_a = 0
n_acc = degen.number_of_acceptance_conditions()
n_max = eci.max_acceptance_conditions()
if (n_acc <= n_max):
ec_a = automaton
else:
print ('<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>')
if ec_a:
ec = eci.instantiate(ec_a)
else:
ec = 0
if ec:
ec_res = ec.check()
if not ec_res:
print '<div class="ec">No accepting run found.</div>'
else:
ec_run = ec_res.accepting_run()
print '<div class="ec">An accepting run was found.<br/>'
if ec_run:
if print_acc_run:
s = spot.ostringstream()
spot.print_tgba_run(s, ec_a, ec_run)
print '<div class="accrun">%s</div>' % cgi.escape(s.str())
del s
if draw_acc_run:
deco = spot.tgba_run_dotty_decorator(ec_run)
dont_run_dot = print_stats(ec_a)
render_automaton(imgprefix + '-e', ec_a, dont_run_dot, deco)
del deco
del ec_run
del ec_res
print '</div>'
del ec
del ec_a
degen = 0
automaton = 0
exit(0)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment