From c4c42a37c635e7663caa6098f303e88a192d1f4a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 4 Jun 2012 20:42:03 +0200
Subject: [PATCH] =?UTF-8?q?ltl2tgba.html:=20Update=20tooltips=20with=20Tom?=
 =?UTF-8?q?=C3=A1=C5=A1=20Babiak's=20comments.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* wrap/python/ajax/ltl2tgba.html: Update tooltips for LTL3BA.
---
 wrap/python/ajax/ltl2tgba.html | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index fb9b12289..32ba67421 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -555,24 +555,24 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 		  <INPUT type="checkbox" name="l3" value="l" checked>
 		  LTL simplifications
 		</label><br>
-		<label class="rtip" title="See previous tooltip for an explanation of suspension.  This version disables suspension in the intermediate alternating automaton, where it is only used for one step.">
+		<label class="rtip" title="See next tooltip for an explanation of suspension.  This version disables suspension in the 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 some subformulae.  Any 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 need not 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.">
+		<label class="rtip" title="Suspension is a technique to postpone the verification of some subformulae.  Any 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="<font color='red'><b>FIXME</b></font>: missing description">
+		<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="<font color='red'><b>FIXME</b></font>: missing description">
+		<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">
+		<label class="rtip" title="Compute Strongly Connected Components to simplify the automaton.">
 		  <INPUT type="checkbox" name="l3" value="C" checked>
 		  SCC simplifications
 		</label><br>