From 26a62c8b685128a17f97c10892d5715830820769 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 22 Mar 2024 16:08:32 +0100
Subject: [PATCH] minimize: t acceptance is compatible with wdba-minimization

* spot/twaalgos/minimize.cc (minimize_obligation_garanteed_to_work):
Skip some tests when the acceptance is "t".
* tests/core/det.test: Adjust.
---
 spot/twaalgos/minimize.cc | 24 +++++++++++++++++++-----
 tests/core/det.test       |  6 +++---
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index 40e176d2e..399cc2541 100644
--- a/spot/twaalgos/minimize.cc
+++ b/spot/twaalgos/minimize.cc
@@ -611,11 +611,25 @@ namespace spot
                                              formula f)
   {
     // WDBA-minimization necessarily work for obligations
-    return ((f && f.is_syntactic_obligation())
-            // Weak deterministic automata are obligations
-            || (aut_f->prop_weak().is_true() && is_deterministic(aut_f))
-            // Guarantee automata are obligations as well.
-            || is_terminal_automaton(aut_f));
+    if (f && f.is_syntactic_obligation())
+      return true;
+    // we can minimize automata with t acceptance
+    if (aut_f->acc().is_t())
+      return true;
+    if (aut_f->prop_weak().is_false())
+      return false;
+    // Weak deterministic automata are obligations
+    if (aut_f->prop_weak().is_true() && is_deterministic(aut_f))
+      return true;
+    scc_info si(aut_f);
+    check_strength(std::const_pointer_cast<twa_graph>(aut_f), &si);
+    // Check again, now that the strength is known
+    if (aut_f->prop_weak().is_true() && is_deterministic(aut_f))
+      return true;
+    // Guarantee automata are obligations as well.
+    if (is_terminal_automaton(aut_f, &si))
+      return true;
+    return false;
   }
 
   twa_graph_ptr
diff --git a/tests/core/det.test b/tests/core/det.test
index 76125ae7e..37b834f42 100755
--- a/tests/core/det.test
+++ b/tests/core/det.test
@@ -149,7 +149,7 @@ AP: 1 "a"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc !complete
-properties: !deterministic exist-branch
+properties: !deterministic exist-branch very-weak
 spot.highlight.states: 0 1
 spot.highlight.edges: 1 2 2 2
 --BODY--
@@ -174,7 +174,7 @@ AP: 1 "a"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc !complete
-properties: !deterministic exist-branch
+properties: !deterministic exist-branch very-weak
 spot.highlight.states: 1 1
 --BODY--
 State: 0 {0}
@@ -198,7 +198,7 @@ AP: 1 "a"
 acc-name: Buchi
 Acceptance: 1 Inf(0)
 properties: trans-labels explicit-labels state-acc !complete
-properties: !deterministic exist-branch
+properties: !deterministic exist-branch very-weak
 spot.highlight.states: 1 5
 spot.highlight.edges: 2 5 3 5
 --BODY--