diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index 87e9209ac..26fdbb24e 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -540,15 +540,23 @@ 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="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)&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&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="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.">
 		  <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)&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&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">
+		  <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">
+		  <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">
 		  <INPUT type="checkbox" name="l3" value="C" checked>
 		  SCC simplifications
diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt
index 317c03e58..e17843b6b 100644
--- a/wrap/python/ajax/protocol.txt
+++ b/wrap/python/ajax/protocol.txt
@@ -84,6 +84,8 @@ LTL3BA processing options if t=l3 (pick many)
   l3=C    SCC simplifications
   l3=M    more deterministic output
   l3=S    direct simulation
+  l3=o    on-the-fly simplifications
+  l3=p    a-posteriori simplifications
 
 Automaton simplifications (pick many)
 
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 4d04da02b..3af5fe4e5 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -341,7 +341,7 @@ if output_type == 'v':
 if output_type == 'v3':
     import subprocess
     try:
-        l3proc = subprocess.Popen(['@LTL3BA@', '-V'], stdout=subprocess.PIPE)
+        l3proc = subprocess.Popen(['@LTL3BA@', '-v'], stdout=subprocess.PIPE)
         (ver, err) = l3proc.communicate()
         err = l3proc.returncode
     except:
@@ -505,7 +505,7 @@ elif translator == 'ta':
     automaton = spot.ltl_to_taa(f, dict, refined_rules)
 elif translator == 'l3':
     l3out = '-T'
-    l3opt = { '-l', '-P', '-A', '-c', '-C' }
+    l3opt = { '-l', '-P', '-A', '-c', '-C', '-o', '-p' }
     for lo in form.getfirst('lo', 'T'):
         if lo == 'U':
             l3out = '-U'
@@ -524,6 +524,10 @@ elif translator == 'l3':
             l3opt.add('-M')
         elif l3 == 'S':
             l3opt.add('-S')
+        elif l3 == 'o':
+            l3opt.remove('-o')
+        elif l3 == 'p':
+            l3opt.remove('-p')
     args = ["@LTL3BA@", l3out]
     args.extend(l3opt)
     args.extend(['-f', spot.to_spin_string(f)])