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

* wrap/python/ajax/ltl2tgba.html: Update tooltips.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2014-08-21 15:04:12 +02:00
parent 829012fe43
commit d9d9837e55
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -564,11 +564,11 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<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-tfm" class="btip" title="A tableau construction that uses BDDs to symbolically represent each state of the automaton. Among the tree algorithms in Spot (Couvreur/FM, Couvreur/LACIM, Tauriainen/TAA) this is the best one, 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><a href="#tabs-tcs" class="btip" title="Compositionnal suspension.<br>To be 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.">Comp.Susp.</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 that are still applied before (LTL simplifications) and after (automata simplifications) LTL3BA is called.">LTL3BA</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 class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
</ul>
<input type="hidden" name="t" value="fm">