diff --git a/ChangeLog b/ChangeLog
index 90292f788..598effd73 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,13 @@
+2012-03-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
+
+	ltl2tgba.html: save state in URL to preserve history
+
+	* wrap/python/ajax/js/jquery.ba-bbq.min.js: New file.
+	* wrap/python/ajax/Makefile.am: Distribute it.
+	* wrap/python/ajax/ltl2tgba.html: Include it, and
+	Adjust the code to update the URL's hash fragment,
+	and to read it.
+
 2012-03-04  Alexandre Duret-Lutz  <adl@lrde.epita.fr>
 
 	python: fix return value of emptiness_check_instantiator
diff --git a/NEWS b/NEWS
index a64832ec5..572241abf 100644
--- a/NEWS
+++ b/NEWS
@@ -2,6 +2,8 @@ New in spot 0.8.2a:
 
   * Support for both Python 2.x and Python 3.x.
     (Previous versions would only work with Python 2.x.)
+  * The online ltl2tgba.html now stores its state in the URL so that
+    history is preserved, and links to particular setups can be sent.
   * Bug fixes:
     - Fix a segfault in the compression code used by the -Z
       option of dve2check.
diff --git a/wrap/python/ajax/Makefile.am b/wrap/python/ajax/Makefile.am
index bd360e9de..c176b16be 100644
--- a/wrap/python/ajax/Makefile.am
+++ b/wrap/python/ajax/Makefile.am
@@ -1,6 +1,7 @@
-## Copyright (C) 2011  Laboratoire d'Informatique de Paris 6 (LIP6),
-## département Systèmes Répartis Coopératifs (SRC), Université Pierre
-## et Marie Curie.
+## -*- encoding: utf-8 -*-
+## Copyright (C) 2011, 2012 Laboratoire d'Informatique de Paris 6
+## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
+## Pierre et Marie Curie.
 ##
 ## This file is part of Spot, a model checking library.
 ##
@@ -21,9 +22,9 @@
 
 nodist_noinst_SCRIPTS = spot.py
 EXTRA_DIST = $(srcdir)/spot.in README ltl2tgba.html css/ltl2tgba.css	\
-  css/tipTip.css js/jquery.tipTip.minified.js logos/lip6sys64.png	\
-  logos/lrde64.png logos/spot64s.png logos/mail.png			\
-  css/ui-lightness/jquery-ui-1.8.13.custom.css				\
+  css/tipTip.css js/jquery.tipTip.minified.js js/jquery.ba-bbq.min.js	\
+  logos/lip6sys64.png logos/lrde64.png logos/spot64s.png		\
+  logos/mail.png css/ui-lightness/jquery-ui-1.8.13.custom.css		\
   css/ui-lightness/images/ui-icons_222222_256x240.png			\
   css/ui-lightness/images/ui-bg_glass_100_f6f6f6_1x400.png		\
   css/ui-lightness/images/ui-bg_glass_100_fdf5ce_1x400.png		\
@@ -37,7 +38,7 @@ EXTRA_DIST = $(srcdir)/spot.in README ltl2tgba.html css/ltl2tgba.css	\
   css/ui-lightness/images/ui-bg_gloss-wave_35_f6a828_500x100.png	\
   css/ui-lightness/images/ui-bg_glass_65_ffffff_1x400.png		\
   css/ui-lightness/images/ui-bg_diagonals-thick_20_666666_40x40.png	\
-  css/ui-lightness/images/ui-bg_highlight-soft_75_ffe45c_1x100.png      \
+  css/ui-lightness/images/ui-bg_highlight-soft_75_ffe45c_1x100.png	\
   protocol.txt
 
 CLEANFILES = $(nodist_noinst_SCRIPTS)
diff --git a/wrap/python/ajax/js/jquery.ba-bbq.min.js b/wrap/python/ajax/js/jquery.ba-bbq.min.js
new file mode 100644
index 000000000..80de36f1c
--- /dev/null
+++ b/wrap/python/ajax/js/jquery.ba-bbq.min.js
@@ -0,0 +1,18 @@
+/*
+ * jQuery BBQ: Back Button & Query Library - v1.3pre - 8/26/2010
+ * http://benalman.com/projects/jquery-bbq-plugin/
+ * 
+ * Copyright (c) 2010 "Cowboy" Ben Alman
+ * Dual licensed under the MIT and GPL licenses.
+ * http://benalman.com/about/license/
+ */
+(function($,r){var h,n=Array.prototype.slice,t=decodeURIComponent,a=$.param,j,c,m,y,b=$.bbq=$.bbq||{},s,x,k,e=$.event.special,d="hashchange",B="querystring",F="fragment",z="elemUrlAttr",l="href",w="src",p=/^.*\?|#.*$/g,u,H,g,i,C,E={};function G(I){return typeof I==="string"}function D(J){var I=n.call(arguments,1);return function(){return J.apply(this,I.concat(n.call(arguments)))}}function o(I){return I.replace(H,"$2")}function q(I){return I.replace(/(?:^[^?#]*\?([^#]*).*$)?.*/,"$1")}function f(K,P,I,L,J){var R,O,N,Q,M;if(L!==h){N=I.match(K?H:/^([^#?]*)\??([^#]*)(#?.*)/);M=N[3]||"";if(J===2&&G(L)){O=L.replace(K?u:p,"")}else{Q=m(N[2]);L=G(L)?m[K?F:B](L):L;O=J===2?L:J===1?$.extend({},L,Q):$.extend({},Q,L);O=j(O);if(K){O=O.replace(g,t)}}R=N[1]+(K?C:O||!N[1]?"?":"")+O+M}else{R=P(I!==h?I:location.href)}return R}a[B]=D(f,0,q);a[F]=c=D(f,1,o);a.sorted=j=function(J,K){var I=[],L={};$.each(a(J,K).split("&"),function(P,M){var O=M.replace(/(?:%5B|=).*$/,""),N=L[O];if(!N){N=L[O]=[];I.push(O)}N.push(M)});return $.map(I.sort(),function(M){return L[M]}).join("&")};c.noEscape=function(J){J=J||"";var I=$.map(J.split(""),encodeURIComponent);g=new RegExp(I.join("|"),"g")};c.noEscape(",/");c.ajaxCrawlable=function(I){if(I!==h){if(I){u=/^.*(?:#!|#)/;H=/^([^#]*)(?:#!|#)?(.*)$/;C="#!"}else{u=/^.*#/;H=/^([^#]*)#?(.*)$/;C="#"}i=!!I}return i};c.ajaxCrawlable(0);$.deparam=m=function(L,I){var K={},J={"true":!0,"false":!1,"null":null};$.each(L.replace(/\+/g," ").split("&"),function(O,T){var N=T.split("="),S=t(N[0]),M,R=K,P=0,U=S.split("]["),Q=U.length-1;if(/\[/.test(U[0])&&/\]$/.test(U[Q])){U[Q]=U[Q].replace(/\]$/,"");U=U.shift().split("[").concat(U);Q=U.length-1}else{Q=0}if(N.length===2){M=t(N[1]);if(I){M=M&&!isNaN(M)?+M:M==="undefined"?h:J[M]!==h?J[M]:M}if(Q){for(;P<=Q;P++){S=U[P]===""?R.length:U[P];R=R[S]=P<Q?R[S]||(U[P+1]&&isNaN(U[P+1])?{}:[]):M}}else{if($.isArray(K[S])){K[S].push(M)}else{if(K[S]!==h){K[S]=[K[S],M]}else{K[S]=M}}}}else{if(S){K[S]=I?h:""}}});return K};function A(K,I,J){if(I===h||typeof I==="boolean"){J=I;I=a[K?F:B]()}else{I=G(I)?I.replace(K?u:p,""):I}return m(I,J)}m[B]=D(A,0);m[F]=y=D(A,1);$[z]||($[z]=function(I){return $.extend(E,I)})({a:l,base:l,iframe:w,img:w,input:w,form:"action",link:l,script:w});k=$[z];function v(L,J,K,I){if(!G(K)&&typeof K!=="object"){I=K;K=J;J=h}return this.each(function(){var O=$(this),M=J||k()[(this.nodeName||"").toLowerCase()]||"",N=M&&O.attr(M)||"";O.attr(M,a[L](N,K,I))})}$.fn[B]=D(v,B);$.fn[F]=D(v,F);b.pushState=s=function(L,I){if(G(L)&&/^#/.test(L)&&I===h){I=2}var K=L!==h,J=c(location.href,K?L:{},K?I:2);location.href=J};b.getState=x=function(I,J){return I===h||typeof I==="boolean"?y(I):y(J)[I]};b.removeState=function(I){var J={};if(I!==h){J=x();$.each($.isArray(I)?I:arguments,function(L,K){delete J[K]})}s(J,2)};e[d]=$.extend(e[d],{add:function(I){var K;function J(M){var L=M[F]=c();M.getState=function(N,O){return N===h||typeof N==="boolean"?m(L,N):m(L,O)[N]};K.apply(this,arguments)}if($.isFunction(I)){K=I;return J}else{K=I.handler;I.handler=J}}})})(jQuery,this);
+/*
+ * jQuery hashchange event - v1.3 - 7/21/2010
+ * http://benalman.com/projects/jquery-hashchange-plugin/
+ * 
+ * Copyright (c) 2010 "Cowboy" Ben Alman
+ * Dual licensed under the MIT and GPL licenses.
+ * http://benalman.com/about/license/
+ */
+(function($,e,b){var c="hashchange",h=document,f,g=$.event.special,i=h.documentMode,d="on"+c in e&&(i===b||i>7);function a(j){j=j||location.href;return"#"+j.replace(/^[^#]*#?(.*)$/,"$1")}$.fn[c]=function(j){return j?this.bind(c,j):this.trigger(c)};$.fn[c].delay=50;g[c]=$.extend(g[c],{setup:function(){if(d){return false}$(f.start)},teardown:function(){if(d){return false}$(f.stop)}});f=(function(){var j={},p,m=a(),k=function(q){return q},l=k,o=k;j.start=function(){p||n()};j.stop=function(){p&&clearTimeout(p);p=b};function n(){var r=a(),q=o(m);if(r!==m){l(m=r,q);$(e).trigger(c)}else{if(q!==m){location.href=location.href.replace(/#.*/,"")+q}}p=setTimeout(n,$.fn[c].delay)}$.browser.msie&&!d&&(function(){var q,r;j.start=function(){if(!q){r=$.fn[c].src;r=r&&r+a();q=$('<iframe tabindex="-1" title="empty"/>').hide().one("load",function(){r||l(a());n()}).attr("src",r||"javascript:0").insertAfter("body")[0].contentWindow;h.onpropertychange=function(){try{if(event.propertyName==="title"){q.document.title=h.title}}catch(s){}}}};j.stop=k;o=function(){return a(q.location.href)};l=function(v,s){var u=q.document,t=$.fn[c].domain;if(v!==s){u.title=h.title;u.open();t&&u.write('<script>document.domain="'+t+'"<\/script>');u.close();q.location.hash=v}}})();return j})()})(jQuery,this);
\ No newline at end of file
diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index 7de6f15db..6a3eac25a 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -11,149 +11,202 @@
     <script type="text/javascript" src="http://ajax.googleapis.com/ajax/libs/jquery/1.6.1/jquery.min.js"></script>
     <script type="text/javascript" src="http://ajax.googleapis.com/ajax/libs/jqueryui/1.8.13/jquery-ui.min.js"></script>
     <script type="text/javascript" src="js/jquery.tipTip.minified.js"></script>
+    <script type="text/javascript" src="js/jquery.ba-bbq.min.js"></script>
     <script type="text/javascript">
-      jQuery(document).ready(function(){
-                     $.spotvars = {
-                        autoupdate: 0
-                     }
-                     $(".tabs").tabs();
-		     $("#send").button();
-		     $("#results").hide();
-                     $(".tabs a").click(function() {return false;});
-                     $(".rtip").tipTip({maxWidth: "300px", delay: 1000,
-                                        edgeOffset: 10,
-                                        defaultPosition: "right"});
-                     $(".btip").tipTip({maxWidth: "300px", delay: 1000,
-                                        edgeOffset: 10,
-                                        defaultPosition: "bottom"});
-                     $(".ftip").tipTip({maxWidth: "300px", delay: 1000,
-                                        edgeOffset: 4,
-                                        defaultPosition: "left",
-                                        content: "<b>Click<\/b> to fold/unfold.<br><b>Ctrl+Click<\/b> to remove (any option set will remain set)."
-                                       });
-                     $(".restip").tipTip({maxWidth: "300px", delay: 1000,
-                                        edgeOffset: 4,
-                                        defaultPosition: "left",
-                                        content: "<b>Click<\/b> to fold/unfold.<br><b>Ctrl+Click<\/b> to remove."
-                                       });
-                     $(".ltltip").tipTip({maxWidth: "300px", delay: 1000,
-                                        edgeOffset: 4,
-                                        defaultPosition: "left",
-                                        content: "<b>Click<\/b> to fold/unfold."
-                                       });
+    jQuery(document).ready(function(){
+        $.spotvars = { autoupdate: 0 }
+        $(".tabs").tabs();
+	$("#send").button();
+	$("#results").hide();
+        $(".tabs a").click(function() {return false;});
+        $(".rtip").tipTip({maxWidth: "300px", delay: 1000,
+                           edgeOffset: 10,
+                           defaultPosition: "right"});
+        $(".btip").tipTip({maxWidth: "300px", delay: 1000,
+                           edgeOffset: 10,
+                           defaultPosition: "bottom"});
+        $(".ftip").tipTip({maxWidth: "300px", delay: 1000,
+                           edgeOffset: 4,
+                           defaultPosition: "left",
+                           content: "<b>Click<\/b> to fold/unfold.<br><b>Ctrl+Click<\/b> to remove (any option set will remain set)."
+                          });
+        $(".restip").tipTip({maxWidth: "300px", delay: 1000,
+                             edgeOffset: 4,
+                             defaultPosition: "left",
+                             content: "<b>Click<\/b> to fold/unfold.<br><b>Ctrl+Click<\/b> to remove."
+                            });
+        $(".ltltip").tipTip({maxWidth: "300px", delay: 1000,
+                             edgeOffset: 4,
+                             defaultPosition: "left",
+                             content: "<b>Click<\/b> to fold/unfold."
+                            });
 
-		      $.get("/cgi-bin/spot.py", "o=v", function(data) {
-			  $("#spottip").attr("title", "This page uses <b>" + data + "<\/b> to process LTL formulas and automata.  Please download the <b>Spot<\/b> library and install it on your computer if you want to do the same from the command line, or from another program.")
-			       .tipTip({maxWidth: "400px", delay: 1000,
-                                        edgeOffset: 10,
-                                        defaultPosition: "right"});
-                      });
+	function hideOrShowPanels(output) {
+	    switch (output)
+	    {
+	    case 'f':
+		$('#translator-tabs,#autsimp-tabs,#run-tabs').hide('fast');
+		break;
+	    case 'm':
+		$('#autsimp-tabs,#run-tabs').hide('fast');
+		$('#translator-tabs').show('fast');
+		break;
+	    case 'a':
+		$('#translator-tabs,#autsimp-tabs').show('fast');
+		$('#run-tabs').hide('fast');
+		break;
+	    case 'r':
+		$('#translator-tabs,#autsimp-tabs,#run-tabs').show('fast');
+		break;
+	    }
+        }
 
-                function fold(ui) {
-                  var icon = ui.children(".ui-icon");
-                  icon.removeClass("ui-icon-circle-arrow-n")
-                      .addClass("ui-icon-circle-arrow-s");
-                  ui.siblings('[class!="dontcollapse"]').hide('fast');
-                }
-                function unfold(ui) {
-                  var icon = ui.children(".ui-icon");
-                  icon.removeClass("ui-icon-circle-arrow-s")
-                      .addClass("ui-icon-circle-arrow-n");
-                  ui.siblings('[class!="dontcollapse"]').show('fast');
+	function updateFormFromHash() {
+	    var hashparam = jQuery.deparam.fragment();
+	    if (jQuery.isEmptyObject(hashparam))
+		return;
+	    $("input,select", "#trform").each(function() {
+		var name = this.name;
+		var value = [];
+		if (name && hashparam[name] != undefined) {
+		    value = hashparam[name];
+		    if (value.constructor != Array)
+			value = [value];
+		} else {
+		    return;
                 }
+		switch(this.type || this.tagName.toLowerCase()) {
+		case "radio":
+		case "checkbox":
+		    this.checked = false;
+		    for(var i = 0; i < value.length; i++) {
+			this.checked |= (value[i] == this.value);
+		    }
+		    break;
+		case "select":
+		    for(var opt = 0; opt < this.options.length; opt++) {
+			var option = this.options[opt];
+			option.selected = false;
+			for (var i = 0; i < value.length; i++) {
+			    option.selected |= (value[i] == option.value);
+			}
+		    }
+		    break;
+		default:
+		    this.value=value.join(',');
+		}
+	    });
+	    updateResults();
+	    var o = $('input[name="o"]').val();
+	    $("#output-tabs").tabs("select", "#tabs-o" + o);
+	    hideOrShowPanels(o);
+            var t = $('input[name="t"]').val();
+	    $("#translator-tabs").tabs('select', '#tabs-t' + t);
+	}
 
-                function foldToggle(ui) {
-                  var icon = ui.children(".ui-icon");
-                  if (icon.hasClass("ui-icon-circle-arrow-n"))
-                    {
-                      icon.removeClass("ui-icon-circle-arrow-n")
-                          .addClass("ui-icon-circle-arrow-s");
-                      ui.siblings('[class!="dontcollapse"]').hide('fast');
-                    }
-                  else
-                    {
-                      icon.removeClass("ui-icon-circle-arrow-s")
-                          .addClass("ui-icon-circle-arrow-n");
-                      ui.siblings('[class!="dontcollapse"]').show('fast');
-                    }
-                }
+	$(window).bind('hashchange', function(e) { updateFormFromHash() });
 
-                function updateResults() {
-                    var str = $("#trform").serialize();
-                    $("#results-body").load("/cgi-bin/spot.py",
-                                       str,
-                                       function(response, status, xhr)
-                   {
-                      $.spotvars.autoupdate = 1;
-		      if (status == "error") {
-			var msg = "Sorry but there was an error: ";
-			$("#results-body").html(msg + xhr.status + " "
-                                                + xhr.statusText);
-		      }
-                      $("#results").show();
-                      fold($("#ltl-head"));
-                      unfold($("#results-head"));
-                      return true;
-                   }
-                );}
-
-                function autoUpdate() {
-                    if ($.spotvars.autoupdate)
-                       updateResults();
-                    return true;
-                }
-
-                $("#send").click(updateResults);
-                $("input,select").change(autoUpdate);
-                $('input[name="f"]').attr('spellcheck', false).focus()
-				    .keydown(function(e){
-                   if (e.keyCode == 13)
-		      updateResults();
-                });
-	      $('.collapsible .head').click(function(e) {
-                      if (e.ctrlKey)
-                        {
-                          if ($(this).attr('id') != 'ltl-head')
-                            $(this).parent().hide('fast');
-                        }
-                      else
-                        {
-                          foldToggle($(this));
-                        }
-		      return false;
-	      });
-      $("#output-tabs").bind("tabsselect", function(event, ui) {
-        switch (ui.panel.id)
-         {
-           case 'tabs-formula':
-             $('input[name="o"]').val('f');
-             $('#translator-tabs,#autsimp-tabs,#run-tabs').hide('fast');
-             break;
-           case 'tabs-monitor':
-             $('input[name="o"]').val('m');
-             $('#autsimp-tabs,#run-tabs').hide('fast');
-             $('#translator-tabs').show('fast');
-             break;
-           case 'tabs-automaton':
-             $('input[name="o"]').val('a');
-             $('#translator-tabs,#autsimp-tabs').show('fast');
-             $('#run-tabs').hide('fast');
-             break;
-           case 'tabs-run':
-             $('input[name="o"]').val('r');
-             $('#translator-tabs,#autsimp-tabs,#run-tabs').show('fast');
-             break;
-          }
-        autoUpdate();
-        return true;
+	$.get("/cgi-bin/spot.py", "o=v", function(data) {
+	    $("#spottip").attr("title", "This page uses <b>" + data + "<\/b> to process LTL formulas and automata.  Please download the <b>Spot<\/b> library and install it on your computer if you want to do the same from the command line, or from another program.")
+		.tipTip({maxWidth: "400px", delay: 1000,
+                         edgeOffset: 10,
+                         defaultPosition: "right"});
         });
-      $('#output-tabs').tabs('select', '#tabs-automaton');
-      $('#translator-tabs').bind("tabsselect", function(event, ui) {
-        $('input[name="t"]').val(ui.panel.id.substring(5,7));
-        autoUpdate();
-        return true;
+
+        function fold(ui) {
+            var icon = ui.children(".ui-icon");
+            icon.removeClass("ui-icon-circle-arrow-n")
+                .addClass("ui-icon-circle-arrow-s");
+            ui.siblings('[class!="dontcollapse"]').hide('fast');
+        }
+        function unfold(ui) {
+            var icon = ui.children(".ui-icon");
+            icon.removeClass("ui-icon-circle-arrow-s")
+                .addClass("ui-icon-circle-arrow-n");
+            ui.siblings('[class!="dontcollapse"]').show('fast');
+        }
+
+        function foldToggle(ui) {
+            var icon = ui.children(".ui-icon");
+            if (icon.hasClass("ui-icon-circle-arrow-n")) {
+                icon.removeClass("ui-icon-circle-arrow-n")
+                    .addClass("ui-icon-circle-arrow-s");
+                ui.siblings('[class!="dontcollapse"]').hide('fast');
+            } else {
+                icon.removeClass("ui-icon-circle-arrow-s")
+                    .addClass("ui-icon-circle-arrow-n");
+                ui.siblings('[class!="dontcollapse"]').show('fast');
+            }
+        }
+
+	function updateHash() {
+            var str = $("#trform").serialize();
+	    // This will trigger updateResults.
+            window.location.hash = "#" + str;
+	    // updateResults();
+        }
+
+        function updateResults() {
+	    // don't read window.location.hash, because
+	    // it has been %-decoded by firefox, which
+	    // cause problems when formulae include '&'.
+	    var fragment = location.href.replace(/^[^#]*#?(.*)$/, '$1');
+	    $.spotvars.autoupdate = 1;
+            $("#results-body")
+		.load("/cgi-bin/spot.py",
+                      fragment,
+                      function(response, status, xhr) {
+			  if (status == "error") {
+			      var msg = "Sorry but there was an error: ";
+			      $("#results-body").html(msg + xhr.status + " "
+						      + xhr.statusText);
+			  }
+			  $("#results").show();
+			  fold($("#ltl-head"));
+			  unfold($("#results-head"));
+			  return true;
+		      });
+        }
+
+        function autoUpdate() {
+            if ($.spotvars.autoupdate)
+                updateHash();
+            return $.spotvars.autoupdate;
+        }
+
+        $("#send").click(updateHash);
+        $("input,select").change(autoUpdate);
+        $('input[name="f"]').attr('spellcheck', false).focus()
+	    .keydown(function(e){
+                if (e.keyCode == 13)
+		    updateHash();
+            });
+	$('.collapsible .head').click(function(e) {
+            if (e.ctrlKey) {
+                if ($(this).attr('id') != 'ltl-head')
+                    $(this).parent().hide('fast');
+            } else {
+                foldToggle($(this));
+            }
+	    return false;
+	});
+	$("#output-tabs").bind("tabsselect", function(event, ui) {
+	    var v = ui.panel.id[6]; // 'tabs-om' => 'm'.
+            $('input[name="o"]').val(v)
+            if (!autoUpdate())
+		hideOrShowPanels(v)
+            return true;
         });
-      });
+	$('#output-tabs').tabs('select', '#tabs-oa');
+	$('#translator-tabs').bind("tabsselect", function(event, ui) {
+            $('input[name="t"]').val(ui.panel.id.substring(6));
+            autoUpdate();
+            return true;
+        });
+
+	// Update the form from the hash value
+	updateFormFromHash();
+    });
     </script>
   </head>
   <body>
@@ -266,15 +319,15 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 	  <div id="output-tabs" class="tabs collapsible shadow">
 	    <ul class="head">
 	      <li>Desired Output:</li>
-	      <li><a href="#tabs-formula" class="btip" title="Simplify the formula, but do not convert it as an automaton.">Formula</a></li>
-	      <li><a href="#tabs-monitor" class="btip" title="Create a monitor accepting all finite prefixes compatible with the formula.">Monitor</a></li>
-	      <li><a href="#tabs-automaton" class="btip" title="Translate the LTL formula into B&uuml;chi automaton.">B&uuml;chi Automaton</a></li>
-	      <li><a href="#tabs-run" class="btip" title="Translate the LTL formula into B&uuml;chi automaton, and exhibit an accepting run.">B&uuml;chi Run</a></li>
+	      <li><a href="#tabs-of" class="btip" title="Simplify the formula, but do not convert it as an automaton.">Formula</a></li>
+	      <li><a href="#tabs-om" class="btip" title="Create a monitor accepting all finite prefixes compatible with the formula.">Monitor</a></li>
+	      <li><a href="#tabs-oa" class="btip" title="Translate the LTL formula into B&uuml;chi automaton.">B&uuml;chi Automaton</a></li>
+	      <li><a href="#tabs-or" class="btip" title="Translate the LTL formula into B&uuml;chi automaton, and exhibit an accepting run.">B&uuml;chi Run</a></li>
 	      <li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
 	    </ul>
 	    <input type="hidden" name="o">
 	    <div>
-	      <div id="tabs-formula">
+	      <div id="tabs-of">
 		Output the (simplified) formula as:<br>
 		<label class="rtip" title="Use letter operators (such as <span class='formula'>G</span> or <span class='formula'>F</span>) when possible.">
 		  <INPUT type="radio" name="ff" value="o" checked>
@@ -289,14 +342,14 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 		  a syntactic tree
 		</label><br>
 	      </div>
-	      <div id="tabs-monitor">
+	      <div id="tabs-om">
 		Translate the (simplified) formula as:<br>
 		<label class="rtip" title="A deterministic monitor is a DFA that accepts all the prefixes of the executions that satisfy the formula.">
 		  <INPUT type="radio" name="mf" value="d" checked>
 		  a deterministic monitor
 		</label><br>
 	      </div>
-	      <div id="tabs-automaton">
+	      <div id="tabs-oa">
 		Translate the (simplified) formula as:<br>
 		<label class="rtip" title="A Transition-based Generalized B&uuml;chi Automaton (TGBA) is the main kind of automaton used by Spot. It is what all the translation algorithm below will output.">
 		  <INPUT type="radio" name="af" value="t" checked>
@@ -311,7 +364,7 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 		  a Spin neverclaim
 		</label><br>
 	      </div>
-	      <div id="tabs-run">
+	      <div id="tabs-or">
 		Translate the (simplified) formula as:<br>
 		<label class="rtip" title="A Transition-based Generalized B&uuml;chi Automaton (TGBA) is the main kind of automaton used by Spot. It is what all the translation algorithm below will output.">
 		  <INPUT type="radio" name="ra" value="t" checked>
@@ -336,14 +389,14 @@ 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-fm" 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-lacim" 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-taa" 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-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-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>
 	    </ul>
 	    <input type="hidden" name="t" value="fm">
 	    <div>
-	      <div id="tabs-fm">
+	      <div id="tabs-tfm">
 		<label class="rtip" title="Try to optimize the automaton for determinism when building it.  Warning: this option can be expensive if the formula uses a lot of different atomic propositions because the algorithm has to consider all possible valuations.">
 		  <INPUT type="checkbox" name="fm" value="od" checked>
 		  optimize determinism
@@ -361,13 +414,13 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 		  fair-loop approximations
 		</label><br>
 	      </div>
-	      <div id="tabs-lacim">
+	      <div id="tabs-tla">
 		<label class="rtip" title="The automaton built by Couvreur/LaCIM is represented symbolically using BDDs.  Useless SCCs can be removed using a series of fix-point operations.  You may want to disable the <b>prune unaccepting SCCs</b> automaton simplification.">
 		  <INPUT type="checkbox" name="la" value="sp" checked>
 		  symbolically prune unaccepting SCCs
 		</label><br>
 	      </div>
-	      <div id="tabs-taa">
+	      <div id="tabs-tta">
 		<label class="rtip" title="Enable a refined set of translation rules, based on language inclusion between subformulas.  Because language inclusion between formula is tested using automata operations on translations for subformulas, this option can be slow.">
 		  <INPUT type="checkbox" name="ta" value="lc" checked>
 		  language containment