From 7ba4ab7931e75163bd68f3a5a5ab63a05cc94c08 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 27 Apr 2012 15:51:20 +0200
Subject: [PATCH] slights documentation changes around direct simulation

* src/tgbaalgos/simulation.hh: Mention the fact that this is
a "direct" simulation.
* wrap/python/ajax/ltl2tgba.html: Likewise, and change the key
to "ds".
* wrap/python/ajax/protocol.txt, wrap/python/ajax/spot.in: Adjust.
---
 src/tgbaalgos/simulation.hh    | 15 +++++++--------
 wrap/python/ajax/ltl2tgba.html |  4 ++--
 wrap/python/ajax/protocol.txt  |  2 +-
 wrap/python/ajax/spot.in       | 10 +++++-----
 4 files changed, 15 insertions(+), 16 deletions(-)

diff --git a/src/tgbaalgos/simulation.hh b/src/tgbaalgos/simulation.hh
index 06efccd91..40301845d 100644
--- a/src/tgbaalgos/simulation.hh
+++ b/src/tgbaalgos/simulation.hh
@@ -30,20 +30,19 @@ namespace spot
   /// \addtogroup tgba_reduction
   /// @{
 
-  /// \brief Tries to reduce the automaton by merging states whose
-  /// recognizes similar language.
+  /// \brief Attempt to reduce the automaton by direct simulation
   ///
   /// When the language recognized by one state is included in the
   /// language recognized by an another one, the first one is merged
-  /// with the second. The algorithm is based on the following
-  /// paper:
+  /// with the second.  The algorithm is based on the following
+  /// paper, but generalized to handled TGBA directly.
   ///
   /// \verbatim
-  ///     @InProceedings{ etessami.00.concur,
+  /// @InProceedings{ etessami.00.concur,
   ///   author        = {Kousha Etessami and Gerard J. Holzmann},
   ///   title         = {Optimizing {B\"u}chi Automata},
   ///   booktitle     = {Proceedings of the 11th International Conference on
-  ///     	      Concurrency Theory (Concur'00)},
+  ///	  	      Concurrency Theory (Concur'00)},
   ///   pages         = {153--167},
   ///   year          = {2000},
   ///   editor        = {C. Palamidessi},
@@ -54,9 +53,9 @@ namespace spot
   /// }
   /// \endverbatim
   ///
-  /// \param automaton The automaton to simulate.
+  /// \param automaton the automaton to simulate.
   /// \return a new automaton which is at worst a copy of the received
-  /// one.
+  /// one
   tgba* simulation(const tgba* automaton);
 
   /// @}
diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index 81a0c00dc..49efa0ce5 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -445,8 +445,8 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 		<INPUT type="checkbox" name="as" value="wd">
 		minimize obligation properties
               </label><br>
-	      <label class="rtip" title="<b>Direct Simulation</b> tries to reduce the automaton with simulation reduction.">
-		<INPUT type="checkbox" name="as" value="rs">
+	      <label class="rtip" title="Attempt to reduce the automaton by using <b>direct simulation</b>.  This might also improve the determinism as a side effect.">
+		<INPUT type="checkbox" name="as" value="ds">
 		direct simulation
               </label><br>
 
diff --git a/wrap/python/ajax/protocol.txt b/wrap/python/ajax/protocol.txt
index fd8b74162..94c2d80e2 100644
--- a/wrap/python/ajax/protocol.txt
+++ b/wrap/python/ajax/protocol.txt
@@ -71,4 +71,4 @@ Automaton simplifications (pick many)
 
   as=ps   Prune SCC
   as=wd   WDBA minimiztion
-  as=rs   Simulation reduction
+  as=ds   Direct Simulation reduction
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 692664cd5..22259cd2a 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -411,14 +411,14 @@ if output_type == 'm':
 # Automaton simplifications
 prune_scc = False
 wdba_minimize = False
-simul_minimize = False
+direct_simul = False
 for s in form.getlist('as'):
     if s == 'ps':
         prune_scc = True
     elif s == 'wd':
         wdba_minimize = True
-    elif s == 'rs':
-        simul_minimize = True
+    elif s == 'ds':
+        direct_simul = True
 
 if output_type == 'a':
     buchi_type = form.getfirst('af', 't')
@@ -450,9 +450,9 @@ if wdba_minimize:
         minimized = 0
         degen = False # No need to degeneralize anymore
         issba = True
-        simul_minimize = False # No need to simulate anymore
+        direct_simul = False # No need to simulate anymore
 
-if simul_minimize:
+if direct_simul:
     automaton = spot.simulation(automaton)
 
 if degen or neverclaim: