From 18b45667627adfc06a8257a586f5f1c71c492be9 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 15 Nov 2017 15:06:13 +0100
Subject: [PATCH] wdba_minimization: make the reverse check first

* spot/twaalgos/minimize.cc (minimize_obligation): When
needed (i.e. in the non-deterministic case), make the reverse check
before the forward check, because it does not require translating the
negated formula.
---
 spot/twaalgos/minimize.cc | 33 +++++++++++++++++----------------
 1 file changed, 17 insertions(+), 16 deletions(-)

diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index a78cbc876..33186597a 100644
--- a/spot/twaalgos/minimize.cc
+++ b/spot/twaalgos/minimize.cc
@@ -603,7 +603,7 @@ namespace spot
 
     // If the input automaton was already weak and deterministic, the
     // output is necessary correct.
-    if (aut_f->prop_weak() && aut_f->prop_universal())
+    if (aut_f->prop_weak() && is_deterministic(aut_f))
       return min_aut_f;
 
     // if f is a syntactic obligation formula, the WDBA minimization
@@ -616,6 +616,17 @@ namespace spot
     if (is_terminal_automaton(aut_f))
       return min_aut_f;
 
+    // If the input was deterministic, then by construction
+    // min_aut_f accepts at least all the words of aut_f, so we do
+    // not need the reverse check.  Otherwise, complement the
+    // minimized WDBA to test the reverse inclusion.
+    // (remove_fin() has a special handling of weak automata, and
+    // dualize also has a special handling of deterministic
+    // automata, so all these steps are quite efficient.)
+    if (!is_deterministic(aut_f)
+        && !product(aut_f, remove_fin(dualize(min_aut_f)))->is_empty())
+      return std::const_pointer_cast<twa_graph>(aut_f);
+
     // Build negation automaton if not supplied.
     if (!aut_neg_f)
       {
@@ -645,26 +656,16 @@ namespace spot
     if (is_terminal_automaton(aut_neg_f))
       return min_aut_f;
 
-    bool ok = false;
-
     // Make sure the minimized WDBA does not accept more words than
     // the input.
     if (product(min_aut_f, aut_neg_f)->is_empty())
       {
         assert((bool)min_aut_f->prop_weak());
-        // If the input was deterministic, then by construction
-        // min_aut_f accepts at least all the words of aut_f, so we do
-        // not need the reverse check.  Otherwise, complement the
-        // minimized WDBA to test the reverse inclusion.
-        // (remove_fin() has a special handling of weak automata, and
-        // dualize also has a special handling of deterministic
-        // automata, so all these steps are quite efficient.)
-        ok = is_deterministic(aut_f)
-          || product(aut_f, remove_fin(dualize(min_aut_f)))->is_empty();
+        return min_aut_f;
+      }
+    else
+      {
+        return std::const_pointer_cast<twa_graph>(aut_f);
       }
-
-    if (ok)
-      return min_aut_f;
-    return std::const_pointer_cast<twa_graph>(aut_f);
   }
 }