Add an option to use WDBA only if it reduces the size of the automaton.

* src/tgba/tgbaexplicit.hh (num_states): New method.
* src/tgbaalgos/minimize.hh, src/tgbaalgos/minimize.cc
(minimize_obligation): Add a reject_bigger option.
* src/tgbatest/ltl2tgba.cc (-RM): New option.
* src/tgbatest/spotlbtt.test: Test -RM.
* bench/ltl2tgba/algorithms: Include -RM in addition to -Rm, and
replace -RDS by -RIS.
* NEWS: Mention this.

NEWS

@@ -31,6 +31,10 @@ New in spot 0.9.2a:
     iterated_simulations() will alternate direct and reverse
     simulations in a loop as long as it diminishes the size of the
     automaton.
+  * minimize_obligation() has a new option to disable WDBA
+    minimization it cases it would produce a deterministic automaton
+    that is bigger than the original TGBA.  So this effectively
+    gives the choice between less states or more determinism.
 
 New in spot 0.9.2 (2012-07-02):
 

bench/ltl2tgba/algorithms

@@ -98,7 +98,7 @@ Algorithm
 {
    Name = "Spot FM Sim (degen)"
    Path = "$LBTT_TRANSLATE"
-   Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -x -RDS -F'"
+   Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -x -RIS -F'"
    Enabled = yes
 }
 
@@ -114,7 +114,7 @@ Algorithm
 {
    Name = "Spot FM WDBA+Sim (degen)"
    Path = "$LBTT_TRANSLATE"
-   Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -x -Rm -RDS -F'"
+   Parameters = "--spin '$LTL2TGBA -f -N -R3 -r7 -x -Rm -RIS -F'"
    Enabled = yes
 }
 
@@ -138,7 +138,7 @@ Algorithm
 {
    Name = "Spot FM Sim (TGBA)"
    Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -RDS -F'"
+   Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -RIS -F'"
    Enabled = yes
 }
 
@@ -152,9 +152,25 @@ Algorithm
 
 Algorithm
 {
-   Name = "Spot FM WDBA+Sim (TGBA)"
+   Name = "Spot FM WDBA* (TGBA)"
    Path = "$LBTT_TRANSLATE"
-   Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -Rm -RDS -F'"
+   Parameters = "--spot '$LTL2TGBA -f -t -R3f -r7 -x -RM -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot FM WDBA+ISim (TGBA)"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -Rm -RIS -F'"
+   Enabled = yes
+}
+
+Algorithm
+{
+   Name = "Spot FM WDBA*+ISim (TGBA)"
+   Path = "$LBTT_TRANSLATE"
+   Parameters = "--spot '$LTL2TGBA -f -t -R3 -r7 -x -RM -RIS -F'"
    Enabled = yes
 }
 EOF

src/tgba/tgbaexplicit.hh

@@ -283,6 +283,12 @@ namespace spot
       return add_state(State::default_val);
     }
 
+    size_t num_states() const
+    {
+      // Do not use ls_.size() because it may contain aliases.
+      return sl_.size();
+    }
+
     transition*
     create_transition(State* source, const State* dest)
     {
@@ -508,7 +514,6 @@ namespace spot
       return to_string_func_(i->second);
     }
 
-    /// old implementation in tgba_explicit_string
     /// Create an alias for a state.  Any reference to \a alias_name
     /// will act as a reference to \a real_name.
     void add_state_alias(const label_t& alias, const label_t& real)

src/tgbaalgos/minimize.cc

@@ -47,6 +47,7 @@
 #include "tgbaalgos/scc.hh"
 #include "tgbaalgos/ltl2tgba_fm.hh"
 #include "tgbaalgos/bfssteps.hh"
+#include "tgbaalgos/stats.hh"
 
 namespace spot
 {
@@ -621,10 +622,22 @@ namespace spot
 
   tgba*
   minimize_obligation(const tgba* aut_f,
-		      const ltl::formula* f, const tgba* aut_neg_f)
+		      const ltl::formula* f, const tgba* aut_neg_f,
+		      bool reject_bigger)
   {
     tgba_explicit_number* min_aut_f = minimize_wdba(aut_f);
 
+    if (reject_bigger)
+      {
+	// Abort if min_aut_f has more states than aut_f.
+	tgba_statistics orig_size = stats_reachable(aut_f);
+	if (orig_size.states < min_aut_f->num_states())
+	  {
+	    delete min_aut_f;
+	    return const_cast<tgba*>(aut_f);
+	  }
+      }
+
     // if f is a syntactic obligation formula, the WDBA minimization
     // must be correct.
     if (f && f->is_syntactic_obligation())

src/tgbaalgos/minimize.hh

@@ -63,9 +63,11 @@ namespace spot
 
   /// \brief Minimize a Büchi automaton in the WDBA class.
   ///
-  /// This takes a TGBA whose language is representable by
+  /// This takes a TGBA whose language is representable by a Weak
-  /// a Weak Deterministic Büchi Automaton, and construct
+  /// Deterministic Büchi Automaton, and construct a minimal WDBA for
-  /// a minimal WDBA for this language.
+  /// this language.  This essentially chains three algorithms:
+  /// determinization, acceptance adjustment (Löding's coloring
+  /// algorithm), and minimization (using a Moore-like approache).
   ///
   /// If the input automaton does not represent a WDBA language,
   /// the resulting automaton is still a WDBA, but it will not
@@ -141,9 +143,17 @@ namespace spot
   /// product(aut_neg_f,minize(aut))</code> are both empty.  If they
   /// are, the the minimization was sound.  (See the paper for full
   /// details.)
+  ///
+  /// If \a reject_bigger is set, this function will return the input
+  /// automaton \a aut_f when the minimized WDBA has more states than
+  /// the input automaton.  (More states are possible because of
+  /// determinization step during minimize_wdba().)  Note that
+  /// checking the size of the minimized WDBA occurs before ensuring
+  /// that the minimized WDBA is correct.
   tgba* minimize_obligation(const tgba* aut_f,
 			    const ltl::formula* f = 0,
-			    const tgba* aut_neg_f = 0);
+			    const tgba* aut_neg_f = 0,
+			    bool reject_bigger = false);
 
   /// @}
 }

src/tgbatest/ltl2tgba.cc

@@ -210,6 +210,9 @@ syntax(char* prog)
 	    << std::endl
             << "  -Rm   attempt to WDBA-minimize the automaton" << std::endl
 	    << std::endl
+            << "  -RM   attempt to WDBA-minimize the automaton unless the "
+	    << "result is bigger" << std::endl
+	    << std::endl
 
             << "Automaton conversion:" << std::endl
             << "  -M    convert into a deterministic minimal monitor "
@@ -341,6 +344,7 @@ main(int argc, char** argv)
   bool graph_run_tgba_opt = false;
   bool opt_reduce = false;
   bool opt_minimize = false;
+  bool reject_bigger = false;
   bool opt_bisim_ta = false;
   bool opt_monitor = false;
   bool containment = false;
@@ -682,6 +686,11 @@ main(int argc, char** argv)
         {
           opt_minimize = true;
         }
+      else if (!strcmp(argv[formula_index], "-RM"))
+        {
+          opt_minimize = true;
+	  reject_bigger = true;
+        }
       else if (!strcmp(argv[formula_index], "-RT"))
         {
           opt_bisim_ta = true;
@@ -1025,7 +1034,7 @@ main(int argc, char** argv)
       if (opt_minimize)
 	{
 	  tm.start("obligation minimization");
-	  minimized = minimize_obligation(a, f);
+	  minimized = minimize_obligation(a, f, 0, reject_bigger);
 	  tm.stop("obligation minimization");
 
 	  if (minimized == 0)

src/tgbatest/spotlbtt.test

@@ -167,6 +167,14 @@ Algorithm
    Enabled = yes
 }
 
+Algorithm
+{
+   Name = "Spot (Couvreur -- FM), +pre +WDBA(rejbig)"
+   Path = "${LBTT_TRANSLATE}"
+   Parameters = "--spot '../ltl2tgba -r4 -R3 -RM -F -f -t'"
+   Enabled = yes
+}
+
 Algorithm
 {
    Name = "Spot (Couvreur -- LaCIM), +pre +WDBA"