From 2d6c7ac045d17acd50861e0e8fbe2f48ff88cb8e Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 8 Dec 2020 20:02:33 +0100
Subject: [PATCH] minimize_wdba: improve handling of terminal automata

Part of #444.

* spot/twaalgos/minimize.cc (minimize_wdba): Terminal automata do not
need a product to decide which states are accepting in the DBA.  This
is faster, and also determinize more formulas of #443.
* tests/core/ltl2tgba2.test: Adjust the expected iteration where
determinization will be aborted.
---
 spot/twaalgos/minimize.cc | 40 +++++++++++++++++++++++++++------------
 tests/core/ltl2tgba2.test |  8 ++++----
 2 files changed, 32 insertions(+), 16 deletions(-)

diff --git a/spot/twaalgos/minimize.cc b/spot/twaalgos/minimize.cc
index bbae0ad0c..4fd6847b3 100644
--- a/spot/twaalgos/minimize.cc
+++ b/spot/twaalgos/minimize.cc
@@ -384,7 +384,7 @@ namespace spot
     hash_set* non_final;
 
     twa_graph_ptr det_a;
-
+    bool has_sinks = false;
     {
       bool input_is_det = is_deterministic(a);
       if (input_is_det)
@@ -396,21 +396,30 @@ namespace spot
           // Find any accepting sink state, to speed up the
           // determinization by merging all states containing a sink
           // state.
-          //
-          // We only as consider as "accepting sink" any state
-          // that have an accepting self-loop labeled by true.
           std::vector<unsigned> acc_sinks;
           unsigned ns = a->num_states();
-          for (unsigned n = 0; n < ns; ++n)
+          if (!a->prop_terminal().is_true())
             {
-              for (auto& e: a->out(n))
-                if (e.dst == n && e.cond == bddtrue
-                    && a->acc().accepting(e.acc))
-                  {
-                    acc_sinks.push_back(n);
-                    break;
-                  }
+              // We only consider as "accepting sink" any state
+              // that has an accepting self-loop labeled by true.
+              for (unsigned n = 0; n < ns; ++n)
+                for (auto& e: a->out(n))
+                  if (e.dst == n && e.cond == bddtrue
+                      && a->acc().accepting(e.acc))
+                    {
+                      acc_sinks.push_back(n);
+                      break;
+                    }
             }
+          else
+            {
+              // All accepting SCCs are terminal.
+              scc_info si(a, scc_info_options::NONE);
+              for (unsigned n = 0; n < ns; ++n)
+                if (si.is_accepting_scc(si.scc_of(n)))
+                  acc_sinks.push_back(n);
+            }
+          has_sinks = !acc_sinks.empty();
           det_a = tgba_powerset(a, aborter, &acc_sinks);
           if (!det_a)
             return nullptr;
@@ -441,6 +450,13 @@ namespace spot
           for (unsigned m = 0; m < scc_count; ++m)
             is_accepting_scc[m] = sm.is_accepting_scc(m);
         }
+      else if (a->prop_terminal())
+        {
+          // tgba_powerset has gathered all terminal states on
+          // powerstate 0.
+          if (has_sinks)
+            is_accepting_scc[sm.scc_of(0)] = true;
+        }
       else
         {
           twa_graph_ptr prod = spot::product(a, det_a, aborter);
diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test
index 3c087de35..f090c2aa2 100755
--- a/tests/core/ltl2tgba2.test
+++ b/tests/core/ltl2tgba2.test
@@ -481,7 +481,7 @@ test 34,0 = `ltl2tgba -B --stats=%s,%d "$f"`
 # Issue #444.  Because WDBA-minimization disables itself for large
 # automata, the output is only deterministic up to a certain point,
 # and the goal is to raise that point.
-f='(!(G({(a)} |=> {(b)[*9]})))'
-test 11,1 = `ltl2tgba -B --stats=%s,%d "$f"`
-f='(!(G({(a)} |=> {(b)[*10]})))'
-test 12,0 = `ltl2tgba -B --stats=%s,%d "$f"`
+f='(!(G({(a)} |=> {(b)[*12]})))'
+test 14,1 = `ltl2tgba -B --stats=%s,%d "$f"`
+f='(!(G({(a)} |=> {(b)[*13]})))'
+test 15,0 = `ltl2tgba -B --stats=%s,%d "$f"`