alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/wrap/python/ajax/ltl2tgba.html
Alexandre Duret-Lutz 49701ca3bc dotty: get rid of the decorated version 
* src/tgbaalgos/dottydec.cc, src/tgbaalgos/dottydec.hh,
src/tgbaalgos/rundotdec.cc, src/tgbaalgos/rundotdec.hh: Delete.
* src/tgbaalgos/Makefile.am, wrap/python/spot.i: Adjust.
* src/tgbaalgos/dotty.cc, src/tgbaalgos/dotty.hh: Remove the
decorated version, and the related arguments.
* src/bin/common_aoutput.cc, src/bin/dstar2tgba.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/complementation.cc,
src/tgbatest/emptchk.cc: Adjust calls.
* wrap/python/ajax/spot.in: Draw the accepting run as an
automaton instead of painting it.
* wrap/python/ajax/ltl2tgba.html: Update help text.
2015-01-24 12:22:31 +01:00

749 lines
41 KiB
HTML
Raw Blame History

<!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&uuml;chi,translation,TGBA">
<meta name="description" content="Translate LTL or PSL formulas into B&uuml;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&nbsp;U&nbsp;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</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">&amp;</span> <span class="formula">&amp;&amp;</span>
<span class="formula">/\</span></td>
<td class="ltldoc">implies:</td><td><span class="formula">-&gt;</span>
<span class="formula">--&gt;</span>
<span class="formula">=&gt;</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">&lt;-&gt;</span>
<span class="formula">&lt;--&gt;</span>
<span class="formula">&lt;=&gt;</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">&lt;&gt;</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=4><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> <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">&amp;&amp;</span> <span class="formula">/\</span></td>
<td class="ltldoc"><ABBR title="Non-Length-Matching">NLM</ABBR> and:</td><td><span class="formula">&amp;</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>
<tr>
<td></td><td></td>
<td class="ltldoc"><abbr title="The operator <span class='formula'>[:+]</span> corresponds to the <span class='formula'>⊕</span> operator introduced by Dax et al. (<i>Specification Languages for Stutter-Invariant Regular Properties</i>, ATVA'09). The other two are generalizations to different bounds.">iterated fusion</abbr>:</td><td><span class="formula">[:*] </span><span class="formula">[:+]</span> <span class="formula">[:*</span><i>i..j</i><span class="formula">]</span></td>
<td></td><td></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">triggers:</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">Non-Ov.</ABBR> trigger:</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">seq:</td><td><span class="formula">{</span><i>s</i><span class="formula">}&lt;&gt;-></span><i>p</i></td>
<td class="ltldoc"><ABBR title="Non-Overlapping">Non-Ov.</ABBR> seq:</td><td><span class="formula">{</span><i>s</i><span class="formula">}&lt;&gt;=></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&uuml;chi automaton.">B&uuml;chi Automaton</a></li>
<li><a href="#tabs-or" class="btip" title="Translate the LTL formula into B&uuml;chi automaton, and exhibit an accepting run.">B&uuml;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="This output can be given to LBT, LBTT, ltl2dstar, scheck, or any other tool using a similar syntax. Spot can also read it back. The original syntax only support atomic propositions named <span class='formula'>p0</span>, <span class='formula'>p1</span>, etc. As an extension, also supported by ltl2dstar, other atomic proposition are enclosed in double quotes. PSL formulas are not supported.">
<INPUT type="radio" name="ff" value="l">
text in LBT'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>
<label class="rtip" title="A nondeterministic monitor is an NFA that accepts all the prefixes of the executions that satisfy the formula.">
<INPUT type="radio" name="mf" value="n" checked>
a nondeterministic monitor
</label><br>
</div>
<div id="tabs-oa">
Translate the (simplified) formula as:<br>
<label class="rtip" title="A Transition-based Generalized B&uuml;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&uuml;chi automaton
</label><br>
<label class="rtip" title="Degeneralize the TGBA to obtain a B&uuml;chi automaton with a single set of accepting states.">
<INPUT type="radio" name="af" value="s">
a state-based degeneralized B&uuml;chi automaton
</label><br>
<label class="rtip" title="Degeneralize the TGBA to obtain a B&uuml;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&uuml;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&uuml;chi automaton
</label><br>
<label class="rtip" title="Degeneralize the TGBA to obtain a B&uuml;chi automaton with a single set of accepting states.">
<INPUT type="radio" name="ra" value="s">
a state-based degeneralized B&uuml;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 as a lasso-shaped 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 produces better results than Tauriainen/TAA, and is the only algorithm that has been extended to support PSL operators.">Couvreur/FM</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-tcs" class="btip" title="Compositional suspension.<br>A technique presented at Spin'13. Suspendable formulas are formulas such as <span class='formula'>GFa</span> or <span class='formula'>FGb</span> whose verification can always be postponed by a finite number of step. In this approach, we extract all suspendable subformulas, translate them separately from the main, skeleton automaton, only to merge them back in the accepting SCC. This translation uses Couvreur/FM for the intermediate parts.">Comp.Susp.</a></li>
<li id="ltl3ba-tab"><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 that are still applied before (LTL simplifications) and after (automata simplifications) LTL3BA is called.">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-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)&amp;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&amp;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" checked>
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 id="tabs-tcs">
<label class="rtip" title="Apply WDBA minimization on skeleton automaton when possible.">
<INPUT type="checkbox" name="cs" value="w">
WDBA minimization of intermediate automaton
</label><br>
<label class="rtip" title="Apply direct simulation on skeleton automaton. This is only done when the WDBA minimization could not work.">
<INPUT type="checkbox" name="cs" value="s" checked>
direct simulation on intermediate automaton
</label><br>
<label class="rtip" title="Start suspension on transitions that enter accepting SCCs instead of waiting to be in the SCC. (Not discussed in the Spin'13 paper.)">
<INPUT type="checkbox" name="cs" value="e">
early start of suspended automata
</label><br>
<label class="rtip" title="Output the skeleton automaton, with suspension labels showing where suspended formulae should be attached.
Unlike in our Spin'13 paper, we consider negated suspension labels and missing suspension labels
equivalently: the important data is the place of the positive suspension labels.">
<INPUT type="checkbox" name="cs" value="c">
do not compose suspended formulas (for debugging)
</label><br>
<!--
<label class="rtip" title="Consider obligation subformulas as atomic propositions initially, and compose their WDBA-minimized translation.">
<INPUT type="checkbox" name="cs" value="o">
compose WDBA-minimized obligation sub-formulas
</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&uuml;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>
Reference in a new issue View git blame Copy permalink