30e0541268
* wrap/python/ajax/ltl2tgba.html: Do not display testing automaton options when generating monitors.
716 lines
38 KiB
HTML
716 lines
38 KiB
HTML
<!doctype HTML public "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
<html lang="en">
|
|
<head>
|
|
<title>Spot's online LTL-to-TGBA translator</title>
|
|
<meta http-equiv="Content-type" content="text/html;charset=UTF-8">
|
|
<meta name="keywords" content="Spot,LTL,automata,Büchi,translation,TGBA">
|
|
<meta name="description" content="Translate LTL or PSL formulas into Büchi automata online using the Spot model-checking library">
|
|
<link rev=Made href="mailto:spot@lrde.epita.fr" title="Spot's discussion list">
|
|
<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">
|
|
<link rel="icon" href="http://spot.lip6.fr/img/favicon.ico" type="image/x-icon">
|
|
<link rel="shortcut icon" href="http://spot.lip6.fr/img/favicon.ico" type="image/x-icon">
|
|
<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>
|
|
<script type="text/javascript" src="js/jquery.ba-dotimeout.min.js"></script>
|
|
<script type="text/javascript">
|
|
jQuery(document).ready(function(){
|
|
$.spotvars = { autoupdate: false,
|
|
scrolldown: true,
|
|
internalchange: false};
|
|
$(".tabs").tabs();
|
|
$("#send").button();
|
|
$("#results").hide();
|
|
$("abbr").tipTip({maxWidth: "300px", delay: 1000,
|
|
edgeOffset: 3,
|
|
defaultPosition: "below"});
|
|
$(".rtip").tipTip({maxWidth: "300px", delay: 1000,
|
|
edgeOffset: 10,
|
|
defaultPosition: "right"});
|
|
$(".btip").tipTip({maxWidth: "300px", delay: 1000,
|
|
edgeOffset: 10,
|
|
defaultPosition: "bottom"});
|
|
$(".ftip").tipTip({maxWidth: "300px", delay: 1000,
|
|
edgeOffset: 4,
|
|
defaultPosition: "left",
|
|
content: "<b>Click<\/b> to fold/unfold.<br><b>Ctrl+Click<\/b> to remove (any option set will remain set)."
|
|
});
|
|
$(".restip").tipTip({maxWidth: "300px", delay: 1000,
|
|
edgeOffset: 4,
|
|
defaultPosition: "left",
|
|
content: "<b>Click<\/b> to fold/unfold.<br><b>Ctrl+Click<\/b> to remove."
|
|
});
|
|
$(".ltltip").tipTip({maxWidth: "300px", delay: 1000,
|
|
edgeOffset: 4,
|
|
defaultPosition: "left",
|
|
content: "<b>Click<\/b> to fold/unfold."
|
|
});
|
|
$("#brcheckbox").change(function() {
|
|
if (!$(this).is(':checked')) {
|
|
$("#lfcheckbox").removeAttr('checked');
|
|
}
|
|
})
|
|
|
|
$("#lfcheckbox").change(function() {
|
|
if ($(this).is(':checked')) {
|
|
$("#brcheckbox").attr('checked', true);
|
|
}
|
|
})
|
|
|
|
$("#ltl3ba-T").change(function() {
|
|
if ($(this).is(':checked')) {
|
|
$("#ltl3ba-S").removeAttr('checked');
|
|
}
|
|
})
|
|
$("#ltl3ba-S").change(function() {
|
|
if ($(this).is(':checked')) {
|
|
$("#ltl3ba-U").attr('checked', true);
|
|
}
|
|
})
|
|
$("#to-s").change(function() {
|
|
if ($(this).is(':checked')) {
|
|
$("#to-l").removeAttr('checked');
|
|
}
|
|
})
|
|
$("#to-l").change(function() {
|
|
if ($(this).is(':checked')) {
|
|
$("#to-s").removeAttr('checked');
|
|
}
|
|
})
|
|
$("#tf-t,#tf-g").change(function() {
|
|
if ($(this).is(':checked')) {
|
|
$("#to-l,#to-s").removeAttr('disabled');
|
|
}
|
|
})
|
|
$("#tf-a").change(function() {
|
|
if ($(this).is(':checked')) {
|
|
$("#to-l,#to-s").attr('disabled', true);
|
|
}
|
|
})
|
|
$("#as-ds,#as-rs").change(function() {
|
|
if ($(this).is(':checked')) {
|
|
$("#as-is").removeAttr('checked');
|
|
}
|
|
})
|
|
$("#as-is").change(function() {
|
|
if ($(this).is(':checked')) {
|
|
$("#as-ds,#as-rs").removeAttr('checked');
|
|
}
|
|
})
|
|
|
|
function hideOrShowPanels(output, duration) {
|
|
switch (output)
|
|
{
|
|
case 'f':
|
|
$('#translator-tabs,#autsimp-tabs,#run-tabs,#tester-tabs').hide(duration);
|
|
break;
|
|
case 'm':
|
|
$('#autsimp-tabs,#run-tabs,#tester-tabs').hide(duration);
|
|
$('#translator-tabs').not('.killed').show(duration);
|
|
break;
|
|
case 'a':
|
|
$('#translator-tabs,#autsimp-tabs').not('.killed').show(duration);
|
|
$('#run-tabs,#tester-tabs').hide(duration);
|
|
break;
|
|
case 't':
|
|
$('#translator-tabs,#autsimp-tabs,#tester-tabs').not('.killed').show(duration);
|
|
$('#run-tabs').hide(duration);
|
|
break;
|
|
case 'r':
|
|
$('#translator-tabs,#autsimp-tabs,#run-tabs').not('.killed').show(duration);
|
|
$('#tester-tabs').hide(duration);
|
|
break;
|
|
}
|
|
}
|
|
|
|
function updateFormFromHash(duration) {
|
|
var hashparam = jQuery.deparam.fragment();
|
|
if (jQuery.isEmptyObject(hashparam))
|
|
return;
|
|
if (!$.spotvars.internalchange)
|
|
$("input,select", "#trform").each(function() {
|
|
var name = this.name;
|
|
var value = [];
|
|
if (name && hashparam[name] != undefined) {
|
|
value = hashparam[name];
|
|
if (value.constructor != Array)
|
|
value = [value];
|
|
}
|
|
switch(this.type || this.tagName.toLowerCase()) {
|
|
case "radio":
|
|
case "checkbox":
|
|
this.checked = false;
|
|
for(var i = 0; i < value.length; i++) {
|
|
this.checked |= (value[i] == this.value);
|
|
}
|
|
break;
|
|
case "select":
|
|
for(var opt = 0; opt < this.options.length; opt++) {
|
|
var option = this.options[opt];
|
|
option.selected = false;
|
|
for (var i = 0; i < value.length; i++) {
|
|
option.selected |= (value[i] == option.value);
|
|
}
|
|
}
|
|
break;
|
|
default:
|
|
this.value=value.join(',');
|
|
}
|
|
});
|
|
$("#brcheckbox,#tf-a").change();
|
|
$.spotvars.autoupdate = true;
|
|
$.spotvars.internalchange = false;
|
|
var o = $('input[name="o"]').val();
|
|
hideOrShowPanels(o, duration);
|
|
$("#output-tabs").tabs("select", "#tabs-o" + o);
|
|
var t = $('input[name="t"]').val();
|
|
$("#translator-tabs").tabs('select', '#tabs-t' + t);
|
|
updateResults();
|
|
}
|
|
|
|
$(window).bind('hashchange', function(e) { updateFormFromHash('fast') });
|
|
|
|
$.get("/cgi-bin/spot.py", "o=v", function(data) {
|
|
$("#spottip").attr("title", "This page uses <b>" + data + "<\/b> to process LTL formulas and automata. Please download the <b>Spot<\/b> library and install it on your computer if you want to do the same from the command line, or from another program.")
|
|
.tipTip({maxWidth: "400px", delay: 1000,
|
|
edgeOffset: 10,
|
|
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")
|
|
.addClass("ui-icon-circle-arrow-s");
|
|
ui.siblings('[class!="dontcollapse"]').hide('fast', callback);
|
|
}
|
|
function unfold(ui, noshowsiblings) {
|
|
var icon = ui.children(".ui-icon");
|
|
icon.removeClass("ui-icon-circle-arrow-s")
|
|
.addClass("ui-icon-circle-arrow-n");
|
|
if (!noshowsiblings) {
|
|
ui.siblings('[class!="dontcollapse"]').show('fast');
|
|
}
|
|
}
|
|
|
|
function foldToggle(ui) {
|
|
var icon = ui.children(".ui-icon");
|
|
if (icon.hasClass("ui-icon-circle-arrow-n")) {
|
|
icon.removeClass("ui-icon-circle-arrow-n")
|
|
.addClass("ui-icon-circle-arrow-s");
|
|
ui.siblings('[class!="dontcollapse"]').hide('fast');
|
|
} else {
|
|
icon.removeClass("ui-icon-circle-arrow-s")
|
|
.addClass("ui-icon-circle-arrow-n");
|
|
ui.siblings('[class!="dontcollapse"]').show('fast');
|
|
}
|
|
}
|
|
|
|
function updateHash() {
|
|
var str = $("#trform").serialize();
|
|
// This will trigger updateResults.
|
|
window.location.hash = "#" + str;
|
|
$.spotvars.internalchange = true;
|
|
// updateResults();
|
|
}
|
|
|
|
function updateResults() {
|
|
// If the answer takes more that 200ms to arrive,
|
|
// display a busy indicator.
|
|
$.doTimeout('res-update', 200, function(){
|
|
$("#results-body").hide();
|
|
$("#results-loading").show();
|
|
$("#results").show();
|
|
unfold($("#results-head"), true);
|
|
})
|
|
// don't read window.location.hash, because
|
|
// it has been %-decoded by firefox, which
|
|
// cause problems when formulae include '&'.
|
|
var fragment = location.href.replace(/^[^#]*#?(.*)$/, '$1');
|
|
$("#results-body")
|
|
.load("/cgi-bin/spot.py",
|
|
fragment,
|
|
function(response, status, xhr) {
|
|
$.doTimeout('res-update');
|
|
if (status == "error") {
|
|
var msg = "Sorry but there was an error: ";
|
|
$("#results-body").html(msg + xhr.status + " "
|
|
+ xhr.statusText);
|
|
}
|
|
$("#results-loading").hide();
|
|
$("#results-body").show();
|
|
$("#results").show();
|
|
unfold($("#results-head"), true);
|
|
fold($("#ltl-head"), function() {
|
|
if ($.spotvars.scrolldown)
|
|
$('html,body').animate({scrollTop: $("#results-head").offset().top}, 'slow');
|
|
$.spotvars.scrolldown = false;
|
|
});
|
|
return true;
|
|
});
|
|
}
|
|
|
|
function autoUpdate() {
|
|
if ($.spotvars.autoupdate)
|
|
updateHash();
|
|
return $.spotvars.autoupdate;
|
|
}
|
|
|
|
$("#send").click(updateHash);
|
|
$("input,select").change(autoUpdate);
|
|
$('input[name="f"]').attr('spellcheck', false).focus()
|
|
.keydown(function(e){
|
|
if (e.keyCode == 13) {
|
|
$.spotvars.scrolldown = true;
|
|
updateHash();
|
|
}
|
|
});
|
|
$('.collapsible .head').click(function(e) {
|
|
if (e.ctrlKey) {
|
|
if ($(this).attr('id') != 'ltl-head')
|
|
$(this).parent().hide('fast').addClass("killed");
|
|
} else {
|
|
foldToggle($(this));
|
|
}
|
|
return false;
|
|
});
|
|
$("#output-tabs").bind("tabsselect", function(event, ui) {
|
|
var v = ui.panel.id[6]; // 'tabs-om' => 'm'.
|
|
$('input[name="o"]').val(v)
|
|
if (!autoUpdate())
|
|
hideOrShowPanels(v, 'fast')
|
|
return true;
|
|
});
|
|
$('#output-tabs').tabs('select', '#tabs-oa');
|
|
$('#translator-tabs').bind("tabsselect", function(event, ui) {
|
|
$('input[name="t"]').val(ui.panel.id.substring(6));
|
|
autoUpdate();
|
|
return true;
|
|
});
|
|
|
|
// Update the form from the hash value
|
|
updateFormFromHash(0);
|
|
});
|
|
</script>
|
|
</head>
|
|
<body>
|
|
<div id="spotlogo">
|
|
<a href="http://spot.lip6.fr/"><img border=0 src="logos/spot64s.png" alt="Spot Logo" class="rtip" id="spottip" title="This page uses the <b>Spot</b> library to process LTL formulas and automata. Please download <b>Spot</b> and install it on your computer if you want to do the same from the command line, or from another program."></a></div>
|
|
<div id="mailicon">
|
|
<a href="mailto:spot@lrde.epita.fr"><img border=0 src="logos/mail.png" alt="Spot Logo" class="rtip" title="A bug? A question? Please e-mail us at <b>spot@lrde.epita.fr</b>."></a></div>
|
|
<div id="lrdelogo">
|
|
<a href="http://www.lrde.epita.fr/"><img border=0 src="logos/lrde64.png" alt="LRDE Logo"></a></div>
|
|
<div id="lip6logo">
|
|
<a href="http://www.lip6.fr/"><img border=0 src="logos/lip6sys64.png" alt="LIP6 Logo"></a></div>
|
|
<div class="ltl2tgba">
|
|
<!-- The action below will not be used. -->
|
|
<FORM id="trform" action="#"><P>
|
|
<div class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
<h3 id="ltl-head" class="ui-widget-header ui-corner-all head">LTL (or PSL) Formula to translate<span class="ui-icon ui-icon-circle-arrow-n ltltip">Fold</span></h3>
|
|
<div class="dontcollapse">
|
|
<INPUT class="formula" type="text" name="f" value=""><span id="send" class="btip" title="Submit the formula and all options. You may simply hit <b>enter</b> after typing the formula. After the first submission the form will auto-update itself anytime you change an option.">Send</span></div>
|
|
<div id="ltl-help">
|
|
<p>Use alphanumeric identifiers or double-quoted strings for atomic
|
|
propositions, and parentheses for grouping.<BR>Identifiers cannot
|
|
start with the letter of a prefix operator (<span class="formula">F</span>,
|
|
<span class="formula">G</span>, or <span class="formula">X</span>): for instance <span class="formula">GFa</span>
|
|
means <span class="formula">G(F(a))</span>. Use <span class="formula">"GFa"</span> if you really want
|
|
to refer to <span class="formula">GFa</span> as a proposition.<br>Conversely, infix
|
|
letter operators are not assumed to be operators if they are part of
|
|
an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
|
|
<span class="formula">a U b</span> and <span class="formula">(a)U(b)</span>.</p>
|
|
<table border="0" width="100%" rules="groups" frame="void" cellpadding="3" cellspacing="0" class="ltltable">
|
|
<colgroup>
|
|
<colgroup span=2>
|
|
<colgroup span=2>
|
|
<colgroup span=2>
|
|
<colgroup span=2>
|
|
<thead>
|
|
<tr>
|
|
<th></th>
|
|
<th colspan=2>Constants</th>
|
|
<th colspan=2>Unary operators (prefix)</th>
|
|
<th colspan=4>Binary operators (infix)</th>
|
|
</tr>
|
|
</thead>
|
|
<tbody>
|
|
<tr>
|
|
<td class="ltldocrow" rowspan=3>Boolean</td>
|
|
<td class="ltldoc">false:</td><td><span class="formula">0</span> <span class="formula">false</span></td>
|
|
<td class="ltldoc">not:</td><td><span class="formula">!</span> <span class="formula">~</span></td>
|
|
<td class="ltldoc">and:</td><td><span class="formula">&</span> <span class="formula">&&</span>
|
|
<span class="formula">/\</span></td>
|
|
<td class="ltldoc">implies:</td><td><span class="formula">-></span>
|
|
<span class="formula">--></span>
|
|
<span class="formula">=></span></td>
|
|
</tr>
|
|
<tr>
|
|
<td class="ltldoc">true:</td><td><span class="formula">1</span> <span class="formula">true</span></td>
|
|
<td></td><td></td>
|
|
<td class="ltldoc">or:</td><td><span class="formula">|</span> <span class="formula">||</span>
|
|
<span class="formula">+</span> <span class="formula">\/</span></td>
|
|
<td class="ltldoc">equivalent:</td><td><span class="formula"><-></span>
|
|
<span class="formula"><--></span>
|
|
<span class="formula"><=></span></td>
|
|
</tr>
|
|
<tr>
|
|
<td></td><td></td>
|
|
<td></td><td></td>
|
|
<td class="ltldoc">xor:</td><td><span class="formula">xor</span> <span class="formula">^</span></td>
|
|
<td></td><td></td>
|
|
</tr>
|
|
</tbody>
|
|
<tbody>
|
|
<tr>
|
|
<td class="ltldocrow" rowspan=3><ABBR title="Linear-time Temporal Logic">LTL</ABBR></td>
|
|
<td></td><td></td>
|
|
<td class="ltldoc">eventually:</td><td><span class="formula">F</span>
|
|
<span class="formula"><></span></td>
|
|
<td class="ltldoc">(strong) until:</td><td><span class="formula">U</span></td>
|
|
<td class="ltldoc">weak until:</td><td><span class="formula">W</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td></td><td></td>
|
|
<td class="ltldoc">always:</td><td><span class="formula">G</span>
|
|
<span class="formula">[]</span></td>
|
|
<td class="ltldoc">(weak) release:</td><td><span class="formula">R</span>
|
|
<span class="formula">V</span></td>
|
|
<td class="ltldoc">strong release:</td><td><span class="formula">M</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td></td><td></td>
|
|
<td class="ltldoc">next:</td><td><span class="formula">X</span> <span class="formula">()</span></td>
|
|
<td></td><td></td>
|
|
<td></td><td></td>
|
|
</tr>
|
|
</tbody>
|
|
<tbody>
|
|
<tr>
|
|
<td class="ltldocrow" rowspan=3><ABBR title="Sequential Extended Regular
|
|
Expression">SERE</ABBR></td>
|
|
<td class="ltldoc">ε:</td><td><span class="formula">[*0]</span></td>
|
|
<td class="ltldoc">Kleene star:</td><td><span class="formula">[*]</span> <span class="formula">[*</span><i>i..j</i><span class="formula">]</span></td>
|
|
<td class="ltldoc">concatenation:</td><td><span class="formula">;</span></td>
|
|
<td class="ltldoc">fusion:</td><td><span class="formula">:</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td></td><td></td>
|
|
<td class="ltldoc">goto:</td><td><span class="formula">[-></span><i>i..j</i><span class="formula">]</span></td>
|
|
<td class="ltldoc">intersection:</td><td><span class="formula">&&</span> <span class="formula">/\</span></td>
|
|
<td class="ltldoc"><ABBR title="Non-Length-Matching">NLM</ABBR> and:</td><td><span class="formula">&</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td></td><td></td>
|
|
<td class="ltldoc">nonconsec. rep.:</td><td><span class="formula">[=</span><i>i..j</i><span class="formula">]</span></td>
|
|
<td class="ltldoc">union:</td><td><span class="formula">|</span> <span class="formula">||</span> <span class="formula">+</span> <span class="formula">\/</span></td>
|
|
<td></td><td></td>
|
|
</tr>
|
|
</tbody>
|
|
<tbody>
|
|
<tr>
|
|
<td class="ltldocrow" rowspan=2><ABBR title="Property Specification Language">PSL</ABBR></td>
|
|
<td></td><td></td>
|
|
<td class="ltldoc">weak closure:</td><td><span class="formula">{</span><i>s</i><span class="formula">}</span></td>
|
|
<td class="ltldoc">∀-suffix impl.:</td><td><span class="formula">{</span><i>s</i><span class="formula">}[]-></span><i>p</i><br><span class="formula">{</span><i>s</i><span class="formula">}|-></span><i>p</i><br><span class="formula">{</span><i>s</i><span class="formula">}(</span><i>p</i><span class="formula">)</span></td>
|
|
<td class="ltldoc"><ABBR title="Non-Overlapping">NO</ABBR> ∀-suffix impl.:</td><td><span class="formula">{</span><i>s</i><span class="formula">}[]=></span><i>p</i><br><span class="formula">{</span><i>s</i><span class="formula">}|=></span><i>p</i></td>
|
|
</tr>
|
|
<tr>
|
|
<td></td><td></td>
|
|
<td class="ltldoc">strong closure:</td><td><span class="formula">{</span><i>s</i><span class="formula">}!</span></td>
|
|
<td class="ltldoc">∃-suffix impl.:</td><td><span class="formula">{</span><i>s</i><span class="formula">}<>-></span><i>p</i></td>
|
|
<td class="ltldoc"><ABBR title="Non-Overlapping">NO</ABBR> ∃-suffix impl.:</td><td><span class="formula">{</span><i>s</i><span class="formula">}<>=></span><i>p</i></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
</div>
|
|
<div class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
<h3 class="ui-widget-header ui-corner-all head">Formula Simplifications<span class="ui-icon ui-icon-circle-arrow-n ftip">Fold</span></h3>
|
|
<div>
|
|
<label class="rtip" title="Apply simple, unconditional rewriting rules to simplify formula. For instance <span class='formula'>F(a)|F(b)</span> is rewritten as <span class='formula'>F(a|b)</span>.">
|
|
<INPUT id="brcheckbox" type="checkbox" name="r" value="br" checked>
|
|
basic rewritings
|
|
</label>
|
|
<label class="rtip" title="Enable basic rewriting rules that may produce bigger formulas.">
|
|
<INPUT id="lfcheckbox" type="checkbox" name="r" value="lf" checked>
|
|
allow larger formulas
|
|
</label><br>
|
|
<label class="rtip" title="Use rewriting rules based on implications between subformulas, when these implications can be proved syntactically. For instance <span class='formula'>a U Fa</span> can be reduced to <span class='formula'>Fa</span> because the latter is obviously implied by <span class='formula'>a</span>.">
|
|
<INPUT type="checkbox" name="r" value="si" checked>
|
|
syntactic implication
|
|
</label><br>
|
|
<label class="rtip" title="Apply simplification rules when subformulas are <b>pure eventuality</b> or <b>purely universal</b>. For instance <span class='formula'>FGFa</span> can be rewritten to <span class='formula'>GFa</span> because the latter is a pure eventuality.">
|
|
<INPUT type="checkbox" name="r" value="eu" checked>
|
|
eventuality and universality
|
|
</label><br>
|
|
<label class="rtip" title="Try to reduce the formula by testing inclusion between automata built for various subformulas. This can be rather slow on large formulas.">
|
|
<INPUT type="checkbox" name="r" value="lc">
|
|
language containment
|
|
</label>
|
|
<label class="rtip floatright" title="Encode all formulas using UTF-8 characters.">
|
|
<INPUT type="checkbox" name="g" value="8">
|
|
UTF-8 output
|
|
</label>
|
|
</div>
|
|
</div>
|
|
<div id="output-tabs" class="tabs collapsible shadow">
|
|
<ul class="head">
|
|
<li>Desired Output:</li>
|
|
<li><a href="#tabs-of" class="btip" title="Simplify the formula, but do not convert it as an automaton.">Formula</a></li>
|
|
<li><a href="#tabs-om" class="btip" title="Create a monitor accepting all finite prefixes compatible with the formula.">Monitor</a></li>
|
|
<li><a href="#tabs-oa" class="btip" title="Translate the LTL formula into Büchi automaton.">Büchi Automaton</a></li>
|
|
<li><a href="#tabs-or" class="btip" title="Translate the LTL formula into Büchi automaton, and exhibit an accepting run.">Büchi Run</a></li>
|
|
<li><a href="#tabs-ot" class="btip" title="Translate the LTL formula into a Testing Automaton, or some variant.">Testing Automaton</a></li>
|
|
<li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
|
|
</ul>
|
|
<input type="hidden" name="o">
|
|
<div>
|
|
<div id="tabs-of">
|
|
Output the (simplified) formula as:<br>
|
|
<label class="rtip" title="Use letter operators (such as <span class='formula'>G</span> or <span class='formula'>F</span>) when possible, and unless UTF-8 output is activated.">
|
|
<INPUT type="radio" name="ff" value="o" checked>
|
|
text in Spot's syntax
|
|
</label><br>
|
|
<label class="rtip" title="This output can be given to Spin or any other tool using a similar syntax. Spot can also read it back. Operators such as such as <span class='formula'>M</span> and <span class='formula'>W</span>, which are not supported by Spin are rewritten away.">
|
|
<INPUT type="radio" name="ff" value="i">
|
|
text in Spin's syntax
|
|
</label><br>
|
|
<label class="rtip" title="A graphical representation of Spot's internal representation. Actually this is not a tree but an acyclic graph, because equal subformulas are shared.">
|
|
<INPUT type="radio" name="ff" value="g">
|
|
a syntactic tree
|
|
</label><br>
|
|
<label class="rtip" title="Various properties of the formula.">
|
|
<INPUT type="radio" name="ff" value="p">
|
|
property information
|
|
</label><br>
|
|
</div>
|
|
<div id="tabs-om">
|
|
Translate the (simplified) formula as:<br>
|
|
<label class="rtip" title="A deterministic monitor is a DFA that accepts all the prefixes of the executions that satisfy the formula.">
|
|
<INPUT type="radio" name="mf" value="d" checked>
|
|
a deterministic monitor
|
|
</label><br>
|
|
</div>
|
|
<div id="tabs-oa">
|
|
Translate the (simplified) formula as:<br>
|
|
<label class="rtip" title="A Transition-based Generalized Büchi Automaton (TGBA) is the main kind of automaton used by Spot. It is what all the translation algorithm below will output.">
|
|
<INPUT type="radio" name="af" value="t" checked>
|
|
a transition-based generalized Büchi automaton
|
|
</label><br>
|
|
<label class="rtip" title="Degeneralize the TGBA to obtain a Büchi automaton with a single set of accepting states.">
|
|
<INPUT type="radio" name="af" value="s">
|
|
a state-based degeneralized Büchi automaton
|
|
</label><br>
|
|
<label class="rtip" title="Degeneralize the TGBA to obtain a Büchi automaton with a single set of accepting states (as with previous option), then output the automaton as a neverclaim that can be fed to Spin.">
|
|
<INPUT type="radio" name="af" value="i">
|
|
a Spin neverclaim
|
|
</label><br>
|
|
</div>
|
|
<div id="tabs-or">
|
|
Translate the (simplified) formula as:<br>
|
|
<label class="rtip" title="A Transition-based Generalized Büchi Automaton (TGBA) is the main kind of automaton used by Spot. It is what all the translation algorithm below will output.">
|
|
<INPUT type="radio" name="ra" value="t" checked>
|
|
a transition-based generalized Büchi automaton
|
|
</label><br>
|
|
<label class="rtip" title="Degeneralize the TGBA to obtain a Büchi automaton with a single set of accepting states.">
|
|
<INPUT type="radio" name="ra" value="s">
|
|
a state-based degeneralized Büchi automaton
|
|
</label><br>
|
|
then<br>
|
|
<label class="rtip" title="Produce a textual description of run accepted by the automaton.">
|
|
<INPUT type="radio" name="rf" value="p">
|
|
print an accepting run
|
|
</label><br>
|
|
<label class="rtip" title="Use color to show an accepting run in the automaton.">
|
|
<INPUT type="radio" name="rf" value="d" checked>
|
|
draw an accepting run on top of the automaton
|
|
</label><br>
|
|
</div>
|
|
<div id="tabs-ot">
|
|
Translate the (simplified) formula into a Büchi automaton, and then convert it into:<br>
|
|
<label class="rtip" title="Instead of reading valuations of all atomic propositions testing automata only watch the changes to these valuation. A transitions labeled by <span class='formula'>a</span> may be crossed only if these atomic proposition change in the system. Additionally, testing automata have two acceptance conditions: states can be Büchi accepting or livelock accepting (or both, or none).">
|
|
<INPUT id="tf-t" type="radio" name="tf" value="t">
|
|
a Testing Automaton (TA)
|
|
</label><br>
|
|
<label class="rtip" title="GTA are testing automata extended with multiple Büchi acceptance conditions.">
|
|
<INPUT id="tf-g" type="radio" name="tf" value="g">
|
|
a Generalized Testing Automaton (GTA)
|
|
</label><br>
|
|
<label class="rtip" title="TGTA are similar to TGBA except instead of reading valuations of all atomic propositions testing automata only watch the changes to these valuation. They have multiple Büchi acceptance conditions on transitions, but no livelock acceptance.">
|
|
<INPUT id="tf-a" type="radio" name="tf" value="a" checked>
|
|
a Transition-based Generalized Testing Automaton (TGTA)
|
|
</label><br>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
<div id="translator-tabs" class="tabs collapsible shadow">
|
|
<ul class="head">
|
|
<li>Translator Algorithm:</li>
|
|
<li><a href="#tabs-tfm" class="btip" title="A tableau construction that uses BDDs to symbolically represent each state of the automaton. This is the best algorithm of the three, and the only one that has been extended to support PSL operators.">Couvreur/FM</a></li>
|
|
<li><a href="#tabs-tla" class="btip" title="Builds a purely symbolic automaton, using BDDs to encode the transition relation. The translation itself is fast (it uses a number of BDD operations that is linear in the size of the formula), but the resulting symbolic encoding is better used symbolically. If you develop it explicitly (e.g. to draw it, as on this page) the result can easily have an exponential number of states.">Couvreur/LaCIM</a></li>
|
|
<li><a href="#tabs-tta" class="btip" title="An implementation of Heikki Tauriainen's Ph.D. thesis algorithm to translate LTL formulas via very weak alternating automata with transition-based generalized acceptance conditions.">Tauriainen/TAA</a></li>
|
|
<li><a href="#tabs-tl3" class="btip" title="An improved version of LTL2BA, overhauled by Tomáš Babiak during his Ph.D., and described at TACAS'12.<br>LTL3BA is not part of Spot. Options in this tab correspond to options offered by LTL3BA, and have some overlap with the options offered by Spot upstream and downstream.">LTL3BA</a></li>
|
|
<li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
|
|
</ul>
|
|
<input type="hidden" name="t" value="fm">
|
|
<div>
|
|
<div id="tabs-tfm">
|
|
<label class="rtip" title="Try to optimize the automaton for determinism when building it. Warning: this option can be expensive if the formula uses a lot of different atomic propositions because the algorithm has to consider all possible valuations.">
|
|
<INPUT type="checkbox" name="fm" value="od" checked>
|
|
optimize determinism
|
|
</label><br>
|
|
<label class="rtip" title="All states that share the same set of outgoing transitions will be merged. This optimization comes for free in the implementation, so there is no point in disabling it unless you want to study its effect.">
|
|
<INPUT type="checkbox" name="fm" value="sm" checked>
|
|
merge states with same symbolic successor representation
|
|
</label><br>
|
|
<label class="rtip" title="Attempt to delay non-deterministic branching. It sometimes helps to reduce the indeterminism (look at the effect on <span class='formula'>X(a) R b</span>), but it may also produce bigger automata.">
|
|
<INPUT type="checkbox" name="fm" value="bp">
|
|
branching postponement
|
|
</label><br>
|
|
<label class="rtip" title="Try to syntactically detect if a state can be part of a fair loop, and if so, do not use acceptance conditions for that state. This optimization seems to have more negative effects than positive effects...">
|
|
<INPUT type="checkbox" name="fm" value="fl">
|
|
fair-loop approximations
|
|
</label><br>
|
|
</div>
|
|
<div id="tabs-tla">
|
|
<label class="rtip" title="The automaton built by Couvreur/LaCIM is represented symbolically using BDDs. Useless SCCs can be removed using a series of fix-point operations. You may want to disable the <b>prune unaccepting SCCs</b> automaton simplification.">
|
|
<INPUT type="checkbox" name="la" value="sp" checked>
|
|
symbolically prune unaccepting SCCs
|
|
</label><br>
|
|
</div>
|
|
<div id="tabs-tta">
|
|
<label class="rtip" title="Enable a refined set of translation rules, based on language inclusion between subformulas. Because language inclusion between formula is tested using automata operations on translations for subformulas, this option can be slow.">
|
|
<INPUT type="checkbox" name="ta" value="lc" checked>
|
|
language containment
|
|
</label><br>
|
|
</div>
|
|
<div id="tabs-tl3">
|
|
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
|
|
</label> or <label class="rtip" title="Run LTL3BA until it produces its final Büchi Automaton. Spot will consider this BA has a TGBA if further optimizations have been requested below.">
|
|
<INPUT id="ltl3ba-U" type="radio" name="lo" value="U">
|
|
a BA
|
|
</label><br>
|
|
<div class="colleft">
|
|
<label class="rtip" title="LTL simplifications performed in LTL3BA are independent of those Spot may have performed upstream.">
|
|
<INPUT type="checkbox" name="l3" value="l" checked>
|
|
LTL simplifications
|
|
</label><br>
|
|
<label class="rtip" title="See next tooltip for an explanation of suspension. LTL3BA supports suspension also in the construction of an intermediate alternating automaton, where it is only used for one step.">
|
|
<INPUT type="checkbox" name="l3" value="A" checked>
|
|
suspension in alternating automaton
|
|
</label><br>
|
|
<label class="rtip" title="Suspension is a technique to postpone the verification of some subformulae. An easy way to picture it is to look at the formula <span class='formula'>F(a)&GF(b)</span>: the <span class='formula'>GF(b)</span> part does not need to be checked before some <span class='formula'>a</span> has been seen. On this example, suspension amounts to translating <span class='formula'>F(a&GF(b))</span> but the technique is more general than such LTL rewritings.">
|
|
<INPUT type="checkbox" name="l3" value="P" checked>
|
|
suspension in TGBA
|
|
</label><br>
|
|
<label class="rtip" title="During the construction, each newly created transition or state is immediately compared to existing transitions or states and merged if possible.">
|
|
<INPUT type="checkbox" name="l3" value="o" checked>
|
|
on-the-fly simplifications
|
|
</label><br>
|
|
</div>
|
|
<label class="rtip" title="Perform the same simplifications as the on-the-fly simplification but on the final automaton, plus some SCC simplifications.">
|
|
<INPUT type="checkbox" name="l3" value="p" checked>
|
|
a-posteriori simplifications
|
|
</label><br>
|
|
<label class="rtip" title="Compute Strongly Connected Components to simplify the automaton.">
|
|
<INPUT type="checkbox" name="l3" value="C" checked>
|
|
SCC simplifications
|
|
</label><br>
|
|
<label class="rtip" title="Try to improve the automaton's determinism when building it. This may produce larger automata.">
|
|
<INPUT type="checkbox" name="l3" value="M">
|
|
more deterministic output
|
|
</label><br>
|
|
<label class="rtip" title="Compute a direct (a.k.a. strong fair) simulation relation to reduce the size of the Büchi automaton.">
|
|
<INPUT id="ltl3ba-S" type="checkbox" name="l3" value="S">
|
|
direct simulation on BA
|
|
</label><br>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
<div id="autsimp-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
<h3 class="ui-widget-header ui-corner-all head">Automaton Simplifications<span class="ui-icon ui-icon-circle-arrow-n ftip">Fold</span></h3>
|
|
<div>
|
|
<label class="rtip" title="Compute the SCCs of the automaton. Eliminate all the useless SCCs (i.e. those that cannot be part of an accepting run). Also attempt to remove redundant acceptance conditions.">
|
|
<INPUT type="checkbox" name="as" value="ps" checked>
|
|
prune unaccepting SCCs
|
|
</label><br>
|
|
<label class="rtip" title="<b>Obligation properties</b> are properties that can be represented by a Weak Deterministic Büchi Automaton (WDBA). Any WDBA has a minimal form that can be constructed in a way that is similar to DFA minimization.<br>Using this option, any automaton (WDBA or not) will be tentatively determinized and minimized; the result will be used only if it is equivalent to the original automaton (i.e., if the property was indeed an obligation property).">
|
|
<INPUT type="checkbox" name="as" value="wd">
|
|
determinize and minimize obligation properties
|
|
</label><br>
|
|
<label class="rtip" title="Attempt to reduce the automaton by using <b>direct simulation</b> on the TGBA. Basically a state <b>A</b> can be merged into a state <b>B</b> if the <b>suffixes</b> reachable from <b>A</b> are included into those reachable from <b>B</b>. This algorithm may also improve determinism as a side effect.">
|
|
<INPUT id="as-ds" type="checkbox" name="as" value="ds">
|
|
direct simulation
|
|
</label>
|
|
<label class="rtip" title="Attempt to reduce the automaton by using <b>reverse simulation</b> on the TGBA. Basically a state <b>A</b> can be merged into a state <b>B</b> if the <b>prefixes</b> reachable from <b>A</b> are included into those reachable from <b>B</b> This can also improve codeterminism as a side effect.">
|
|
<INPUT id="as-rs" type="checkbox" name="as" value="rs">
|
|
reverse simulation
|
|
</label>
|
|
<label class="rtip" title="Apply <b>direct</b> and <b>reverse simulation</b> alternatively until the automaton is not reduced further.">
|
|
<INPUT id="as-is" type="checkbox" name="as" value="is">
|
|
iterated simulations
|
|
</label><br>
|
|
</div>
|
|
</div>
|
|
<div id="run-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
<h3 class="ui-widget-header ui-corner-all
|
|
head">Emptiness-check Algorithm<span class="ui-icon ui-icon-circle-arrow-n ftip">Fold</span></h3>
|
|
<div>
|
|
Search accepting run using algorithm:
|
|
<select name="ec">
|
|
<option value="Cou99" selected>Cou99</option>
|
|
<option value="CVWY90">CVWY90</option>
|
|
<option value="GV04">GV04</option>
|
|
<option value="SE05">SE05</option>
|
|
<option value="Tau03">Tau03</option>
|
|
<option value="Tau03_opt">Tau03_opt</option>
|
|
</select> with these
|
|
<a href="http://spot.lip6.fr/wiki/EmptinessCheckOptions">options</a>:
|
|
<INPUT type="text" maxlength="40" name="eo" value="">
|
|
</div>
|
|
</div>
|
|
<div id="tester-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
<h3 class="ui-widget-header ui-corner-all head">Testing Automaton Options<span class="ui-icon ui-icon-circle-arrow-n ftip">Fold</span></h3>
|
|
<div>
|
|
<label class="rtip" title="Divert all livelock accepting paths to a single livelock acceptance state.">
|
|
<INPUT id="to-l" type="checkbox" name="to" value="l">
|
|
use a catch-all livelock state
|
|
</label><br>
|
|
<label class="rtip" title="Ensure that all livelock accepting states are also Büchi-accepting, so that the testing automaton can be tested for emptiness in a single pass.">
|
|
<INPUT id="to-s" type="checkbox" name="to" value="s" checked>
|
|
produce a single-pass testing automaton
|
|
</label><br>
|
|
<label class="rtip" title="Merge bisimilar states in the final testing automaton.">
|
|
<INPUT type="checkbox" name="to" value="m" checked>
|
|
merge bisimilar states
|
|
</label><br>
|
|
</div>
|
|
</div>
|
|
</FORM>
|
|
<div id="results" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
|
|
<h3 id="results-head" class="ui-widget-header ui-corner-all head">Results<span class="ui-icon ui-icon-circle-arrow-n restip">Fold</span></h3>
|
|
<div id="results-loading" class="dontcollapse"><img src="css/loading.gif" class="loading" border=0 alt="loading..."></div>
|
|
<div id="results-body">
|
|
Loading...
|
|
</div>
|
|
</div>
|
|
</div>
|
|
</body>
|
|
</html>
|