alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltl2tgba.html: Detect ltl3ba's presence and version.

Browse source 
* wrap/python/ajax/ltl2tgba.html: Display the ltl3ba version, and
disable its tab when unavailable.
* wrap/python/ajax/protocol.txt: Add option for ltl3ba's version.
* wrap/python/ajax/spot.in: Implement this option, and catch
errors when ltl3ba is not installed.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-23 19:47:17 +02:00
parent 04cc63cac2
commit 689f56f480
3 changed files with 39 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

17
wrap/python/ajax/ltl2tgba.html
View file

@ -8,7 +8,7 @@
<link rel="stylesheet" href="css/ui-lightness/jquery-ui-1.8.13.custom.css">
<link rel="stylesheet" href="css/tipTip.css">
<link rel="stylesheet" href="css/ltl2tgba.css">
<script type="text/javascript" src="http://ajax.googleapis.com/ajax/libs/jquery/1.6.1/jquery.min.js"></script>
<script type="text/javascript" src="http://ajax.googleapis.com/ajax/libs/jquery/1.7.2/jquery.min.js"></script>
<script type="text/javascript" src="http://ajax.googleapis.com/ajax/libs/jqueryui/1.8.13/jquery-ui.min.js"></script>
<script type="text/javascript" src="js/jquery.tipTip.minified.js"></script>
<script type="text/javascript" src="js/jquery.ba-bbq.min.js"></script>
@ -20,7 +20,6 @@
$(".tabs").tabs();
$("#send").button();
$("#results").hide();
$(".tabs a").click(function() {return false;});
$(".rtip").tipTip({maxWidth: "300px", delay: 1000,
edgeOffset: 10,
defaultPosition: "right"});
@ -139,6 +138,18 @@
defaultPosition: "right"});
});
$.get("/cgi-bin/spot.py", "o=v3", function(data) {
if (data != 'not available') {
$("#ltl3ba-link").attr("title", data)
.tipTip({maxWidth: "400px", delay: 1000,
edgeOffset: 10,
defaultPosition: "right"});
} else {
var index = $('#translator-tabs a[href="#tabs-tl3"]').parent().index();
$("#translator-tabs").tabs("option", "disabled", [index - 1]);
}
});
function fold(ui, callback) {
var icon = ui.children(".ui-icon");
icon.removeClass("ui-icon-circle-arrow-n")
@ -516,7 +527,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
</label><br>
</div>
<div id="tabs-tl3">
Use <a href="http://sourceforge.net/projects/ltl3ba/">LTL3BA</a> to build:
Use <a href="http://sourceforge.net/projects/ltl3ba/" id="ltl3ba-link">LTL3BA</a> to build:
<label class="rtip" title="Stop LTL3BA once it has built a Transition-based Generalized Büchi Automaton. Spot will take it from here and optionally apply more optimizations.">
<INPUT id="ltl3ba-T" type="radio" name="lo" value="T" checked>
a TGBA

1
wrap/python/ajax/protocol.txt
View file

@ -20,6 +20,7 @@ Choosing the desired output (pick one)
o=m output monitor
o=a output automaton
o=r output run
o=v3 output LTL3BA's version (no other argument needed)
Type of formula output if o=f (pick one)

30
wrap/python/ajax/spot.in
View file

@ -337,6 +337,21 @@ if output_type == 'v':
unbufprint('Spot version %s\n' % spot.version())
finish()
# ltl3ba's version
if output_type == 'v3':
import subprocess
try:
l3proc = subprocess.Popen(['@LTL3BA@', '-V'], stdout=subprocess.PIPE)
(ver, err) = l3proc.communicate()
err = l3proc.returncode
except:
err = 1
if err != 0:
unbufprint('not available')
else:
unbufprint(ver.replace("\n", "<br>"))
finish()
spot.unblock_signal(signal.SIGALRM)
spot.unblock_signal(signal.SIGTERM)
os.setpgrp()
@ -515,13 +530,16 @@ elif translator == 'l3':
import subprocess
l3file = tmpdir + "/aut"
l3aut = open(l3file, "w+")
l3proc = subprocess.Popen(args, stdout=l3aut)
l3aut.close()
ret = l3proc.wait()
if ret != 0:
unbufprint('''<div class="error">ltl3ba exited with error %s</div>'''
% ret)
try:
l3proc = subprocess.Popen(args, stdout=l3aut)
ret = l3proc.wait()
except:
unbufprint('<div class="error">Failed to run ltl3ba. Is it installed?</div>')
finish()
if ret != 0:
unbufprint('<div class="error">ltl3ba exited with error %s</div>' % ret)
finish()
l3aut.close()
tpel = spot.empty_tgba_parse_error_list()
automaton = spot.tgba_parse(l3file, tpel, dict, env)
if tpel: