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

@@ -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,13 +636,13 @@ main(int argc, char** argv)
 	{
 	  display_reduce_form = true;
 	}
-      else if (!strcmp(argv[formula_index], "-Rm"))
+      else if (!strcmp(argv[formula_index], "-RDS"))
         {
-          opt_minimize = true;
+          reduction_dir_sim = true;
         }
-      else if (!strcmp(argv[formula_index], "-RSD"))
+      else if (!strcmp(argv[formula_index], "-Rm"))
         {
-          reduction_dir_sim = true;
+          opt_minimize = true;
         }
       else if (!strcmp(argv[formula_index], "-M"))
         {

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
 }