f3bae53e5b
* wrap/python/ajax/ltl2tgba.html: Adjust to use
jQuery 1.6.1 and jQuery-UI 1.8.13. Remove a useless check
of $("#autoupdate").attr("checked") since this checkbox no longer
exists.
* wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.8.custom.css:
Replace by ...
* wrap/python/ajax/css/ui-lightness/jquery-ui-1.8.13.custom.css: This.
* wrap/python/ajax/Makefile.am (EXTRA_DIST): Adjust.
416 lines
23 KiB
HTML
416 lines
23 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 on-line 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">
|
|
<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">
|
|
<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/jqueryui/1.8.13/jquery-ui.min.js"></script>
|
|
<script type="text/javascript" src="js/jquery.tipTip.minified.js"></script>
|
|
<script type="text/javascript">
|
|
jQuery(document).ready(function(){
|
|
$.spotvars = {
|
|
autoupdate: 0
|
|
}
|
|
$(".tabs").tabs();
|
|
$("#send").button();
|
|
$("#results").hide();
|
|
$(".tabs a").click(function() {return false;});
|
|
$(".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."
|
|
});
|
|
|
|
$.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"});
|
|
});
|
|
|
|
function fold(ui) {
|
|
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');
|
|
}
|
|
function unfold(ui) {
|
|
var icon = ui.children(".ui-icon");
|
|
icon.removeClass("ui-icon-circle-arrow-s")
|
|
.addClass("ui-icon-circle-arrow-n");
|
|
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 updateResults() {
|
|
var str = $("#trform").serialize();
|
|
$("#results-body").load("/cgi-bin/spot.py",
|
|
str,
|
|
function(response, status, xhr)
|
|
{
|
|
$.spotvars.autoupdate = 1;
|
|
if (status == "error") {
|
|
var msg = "Sorry but there was an error: ";
|
|
$("#results-body").html(msg + xhr.status + " "
|
|
+ xhr.statusText);
|
|
}
|
|
$("#results").show();
|
|
fold($("#ltl-head"));
|
|
unfold($("#results-head"));
|
|
return true;
|
|
}
|
|
);}
|
|
|
|
function autoUpdate() {
|
|
if ($.spotvars.autoupdate)
|
|
updateResults();
|
|
return true;
|
|
}
|
|
|
|
$("#send").click(updateResults);
|
|
$("input,select").change(autoUpdate);
|
|
$('input[name="f"]').attr('spellcheck', false)
|
|
.keydown(function(e){
|
|
if (e.keyCode == 13)
|
|
updateResults();
|
|
});
|
|
$('.collapsible .head').click(function(e) {
|
|
if (e.ctrlKey)
|
|
{
|
|
if ($(this).attr('id') != 'ltl-head')
|
|
$(this).parent().hide('fast');
|
|
}
|
|
else
|
|
{
|
|
foldToggle($(this));
|
|
}
|
|
return false;
|
|
});
|
|
$("#output-tabs").bind("tabsselect", function(event, ui) {
|
|
switch (ui.panel.id)
|
|
{
|
|
case 'tabs-formula':
|
|
$('input[name="o"]').val('f');
|
|
$('#translator-tabs,#autsimp-tabs,#run-tabs').hide('fast');
|
|
break;
|
|
case 'tabs-monitor':
|
|
$('input[name="o"]').val('m');
|
|
$('#autsimp-tabs,#run-tabs').hide('fast');
|
|
$('#translator-tabs').show('fast');
|
|
break;
|
|
case 'tabs-automaton':
|
|
$('input[name="o"]').val('a');
|
|
$('#translator-tabs,#autsimp-tabs').show('fast');
|
|
$('#run-tabs').hide('fast');
|
|
break;
|
|
case 'tabs-run':
|
|
$('input[name="o"]').val('r');
|
|
$('#translator-tabs,#autsimp-tabs,#run-tabs').show('fast');
|
|
break;
|
|
}
|
|
autoUpdate();
|
|
return true;
|
|
});
|
|
$('#output-tabs').tabs('select', '#tabs-automaton');
|
|
$('#translator-tabs').bind("tabsselect", function(event, ui) {
|
|
$('input[name="t"]').val(ui.panel.id.substring(5,7));
|
|
autoUpdate();
|
|
return true;
|
|
});
|
|
});
|
|
</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">
|
|
<h3 id="ltl-head" class="ui-widget-header ui-corner-all head">LTL 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="1"><tr><td>
|
|
<table border="0" rules="groups" frame="void" cellpadding="3" cellspacing=0>
|
|
<colgroup span=2>
|
|
<colgroup span=2>
|
|
<colgroup span=2>
|
|
<colgroup span=2>
|
|
<thead>
|
|
<tr>
|
|
<th colspan=2>Unary operators<br>(prefix)</th>
|
|
<th colspan=4>Binary operators<br>(infix)</th>
|
|
<th colspan=2>Constants</th>
|
|
</tr>
|
|
</thead>
|
|
<tbody>
|
|
<tr>
|
|
<td align="right">not:</td><td><span class="formula">!</span> <span class="formula">~</span></td>
|
|
<td align="right">and:</td><td><span class="formula">&</span> <span class="formula">&&</span>
|
|
<span class="formula">.</span> <span class="formula">/\</span></td>
|
|
<td align="right">(strong) until:</td><td><span class="formula">U</span></td>
|
|
<td align="right">true:</td><td><span class="formula">1</span>
|
|
<span class="formula">true</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td align="right">eventually:</td><td><span class="formula">F</span>
|
|
<span class="formula"><></span></td>
|
|
<td align="right">or:</td><td><span class="formula">|</span> <span class="formula">||</span>
|
|
<span class="formula">+</span> <span class="formula">\/</span></td>
|
|
|
|
<td align="right">weak until:</td><td><span class="formula">W</span></td>
|
|
<td align="right">false:</td><td><span class="formula">0</span>
|
|
<span class="formula">false</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td align="right">always:</td><td><span class="formula">G</span>
|
|
<span class="formula">[]</span></td>
|
|
<td align="right">implies:</td><td><span class="formula">-></span>
|
|
<span class="formula">--></span>
|
|
<span class="formula">=></span></td>
|
|
<td align="right">(weak) release:</td><td><span class="formula">R</span>
|
|
<span class="formula">V</span></td>
|
|
<td></td><td></td>
|
|
</tr>
|
|
<tr>
|
|
<td align="right">next:</td><td><span class="formula">X</span> <span class="formula">()</span></td>
|
|
<td align="right">equivalent:</td><td><span class="formula"><-></span>
|
|
<span class="formula"><--></span>
|
|
<span class="formula"><=></span></td>
|
|
<td align="right">strong release:</td><td><span class="formula">M</span></td>
|
|
<td></td><td></td>
|
|
</tr>
|
|
<tr>
|
|
<td></td><td></td>
|
|
<td align="right">xor:</td><td><span class="formula">^</span> <span class="formula">xor</span></td>
|
|
<td></td><td></td>
|
|
<td></td><td></td>
|
|
</tr>
|
|
</tbody>
|
|
</table></td></tr></table>
|
|
</div>
|
|
</div>
|
|
<div class="ui-widget ui-widget-content ui-corner-all collapsible">
|
|
<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 type="checkbox" name="r" value="br" checked>
|
|
basic rewritings
|
|
</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><br>
|
|
</div>
|
|
</div>
|
|
<div id="output-tabs" class="tabs collapsible">
|
|
<ul class="head">
|
|
<li>Desired Output:</li>
|
|
<li><a href="#tabs-formula" class="btip" title="Simplify the formula, but do not convert it as an automaton.">Formula</a></li>
|
|
<li><a href="#tabs-monitor" class="btip" title="Create a monitor accepting all finite prefixes compatible with the formula.">Monitor</a></li>
|
|
<li><a href="#tabs-automaton" class="btip" title="Translate the LTL formula into Büchi automaton.">Büchi Automaton</a></li>
|
|
<li><a href="#tabs-run" class="btip" title="Translate the LTL formula into Büchi automaton, and exhibit an accepting run.">Büchi Run</a></li>
|
|
<li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
|
|
</ul>
|
|
<input type="hidden" name="o">
|
|
<div>
|
|
<div id="tabs-formula">
|
|
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.">
|
|
<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.">
|
|
<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>
|
|
</div>
|
|
<div id="tabs-monitor">
|
|
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-automaton">
|
|
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-run">
|
|
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" checked>
|
|
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">
|
|
draw an accepting run on top of the automaton
|
|
</label><br>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
<div id="translator-tabs" class="tabs collapsible">
|
|
<ul class="head">
|
|
<li>Translator Algorithm:</li>
|
|
<li><a href="#tabs-fm" 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.)">Couvreur/FM</a></li>
|
|
<li><a href="#tabs-lacim" 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-taa" 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 class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
|
|
</ul>
|
|
<input type="hidden" name="t" value="fm">
|
|
<div>
|
|
<div id="tabs-fm">
|
|
<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-lacim">
|
|
<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-taa">
|
|
<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>
|
|
</div>
|
|
<div id="autsimp-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible">
|
|
<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 accepts 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 minimized and 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">
|
|
minimize obligation properties
|
|
</label><br>
|
|
</div>
|
|
</div>
|
|
<div id="run-tabs" class="ui-widget ui-widget-content ui-corner-all collapsible">
|
|
<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>
|
|
</FORM>
|
|
<div id="results" class="ui-widget ui-widget-content ui-corner-all collapsible">
|
|
<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-body">
|
|
</div>
|
|
</div>
|
|
</div>
|
|
</body>
|
|
</html>
|