From 66c77f587b925c3bc9c2eff708178032bfed7884 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 28 Apr 2013 12:36:35 +0200
Subject: [PATCH] cgi: improve documentation

* wrap/python/ajax/ltl2tgba.html: Augment and update tooltips to match
vocabulary in the Spin'13 paper.  Hide the compose obligation option
since it's a work in progress.
---
 wrap/python/ajax/ltl2tgba.html | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index 9d76a7eab..211f768e8 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -568,7 +568,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 	      <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>Work in progress.">Comp.Susp.</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 class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
 	    </ul>
 	    <input type="hidden" name="t" value="fm">
@@ -648,26 +648,29 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 		</label><br>
 	      </div>
 	      <div id="tabs-tcs">
-		<label class="rtip" title="Apply WDBA minimization on intermediate automaton.  We can only do it if the input formula is an obligation (in this case there is nothing to suspend and the automaton we process is already the final one) or if the intermediate automaton has the shape of a guarantee property.">
-		  <INPUT type="checkbox" name="cs" value="w" checked>
+		<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 intermediate automaton.  This is only done when the WDBA minimization could not work.">
+		<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.">
+		<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 intermediate automaton with labels showing where suspended formulae should be attached.">
+		<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>
+		</label><br> -->
 	      </div>
 	    </div>
 	  </div>