From 324802c04f01d2c160e507f0265dd188864aa829 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 27 Apr 2012 17:26:59 +0200
Subject: [PATCH] Change the simulation option from -RSD to -RDS and document
 it.

* src/tgbatest/ltl2tgba.cc: Here.
* src/tgbatest/spotlbtt.test: Adjust.
---
 src/tgbatest/ltl2tgba.cc   | 14 ++++++++------
 src/tgbatest/spotlbtt.test |  8 ++++----
 2 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 2e4b3e7c9..be3729264 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -201,7 +201,9 @@ syntax(char* prog)
 	    << "          "
 	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
 	    << std::endl
-            << "  -Rm   attempt to minimize the automata" << std::endl
+	    << "  -RDS  minimize the automaton with direct simulation"
+	    << std::endl
+            << "  -Rm   attempt to WDBA-minimize the automata" << std::endl
 	    << std::endl
 
             << "Automaton conversion:" << std::endl
@@ -614,7 +616,7 @@ main(int argc, char** argv)
 	       || !strcmp(argv[formula_index], "-R2t"))
 	{
 	  // For backward compatibility, make all these options
-	  // equal to -RSD.
+	  // equal to -RDS.
 	  reduction_dir_sim = true;
 	}
       else if (!strcmp(argv[formula_index], "-R3"))
@@ -634,14 +636,14 @@ main(int argc, char** argv)
 	{
 	  display_reduce_form = true;
 	}
+      else if (!strcmp(argv[formula_index], "-RDS"))
+        {
+          reduction_dir_sim = true;
+        }
       else if (!strcmp(argv[formula_index], "-Rm"))
         {
           opt_minimize = true;
         }
-      else if (!strcmp(argv[formula_index], "-RSD"))
-        {
-          reduction_dir_sim = true;
-        }
       else if (!strcmp(argv[formula_index], "-M"))
         {
           opt_monitor = true;
diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test
index 7157e87ec..8b1cb8afb 100755
--- a/src/tgbatest/spotlbtt.test
+++ b/src/tgbatest/spotlbtt.test
@@ -195,7 +195,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), simulated"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot '../ltl2tgba -F -f -t -RSD  -r4 -R3'"
+   Parameters = "--spot '../ltl2tgba -F -f -t -RDS  -r4 -R3'"
    Enabled = yes
 }
 
@@ -203,7 +203,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- LaCim), simulated"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot '../ltl2tgba -F -f -l -t -RSD  -r4 -R3'"
+   Parameters = "--spot '../ltl2tgba -F -f -l -t -RDS  -r4 -R3'"
    Enabled = yes
 }
 
@@ -211,7 +211,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- TAA), simulated"
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot '../ltl2tgba -F -f -l -taa -t -RSD  -r4 -R3'"
+   Parameters = "--spot '../ltl2tgba -F -f -l -taa -t -RDS  -r4 -R3'"
    Enabled = yes
 }
 
@@ -219,7 +219,7 @@ Algorithm
 {
    Name = "Spot (Couvreur -- FM), simulated and degeneralized on states."
    Path = "${LBTT_TRANSLATE}"
-   Parameters = "--spot '../ltl2tgba -F -f -t -RSD -DS'"
+   Parameters = "--spot '../ltl2tgba -F -f -t -RDS -DS'"
    Enabled = yes
 }