From d9d9837e55350cfb9adec59e01caa2cd182091fd Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 21 Aug 2014 15:04:12 +0200
Subject: [PATCH] * wrap/python/ajax/ltl2tgba.html: Update tooltips.

---
 wrap/python/ajax/ltl2tgba.html | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index 211f768e8..949cfad06 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -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">