From 294566802116248f58a9c8a7931e6e655b455e10 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 9 May 2012 13:15:46 +0200
Subject: [PATCH] Update the help text for the Couvreur/FM algorithm.

* wrap/python/ajax/ltl2tgba.html: Mention PSL.
---
 wrap/python/ajax/ltl2tgba.html | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index ff09002b5..f6b5f49af 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -466,7 +466,7 @@ 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.)">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.  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-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 class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>