From 4bb4aeb3727febc1b61aeff00db74c9ff301cd52 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 7 Apr 2019 15:26:15 +0200
Subject: [PATCH] simulation: fix commit 8959eabad

* spot/twaalgos/simulation.cc: Restrict common_in marks to current SCC
when pushing them, otherwise weak automata might become inherently
weak.
* tests/core/sim3.test: Add test case.
---
 spot/twaalgos/simulation.cc | 89 ++++++++++++++++++++++---------------
 tests/core/sim3.test        | 73 ++++++++++++++++++++++++++++++
 2 files changed, 126 insertions(+), 36 deletions(-)

diff --git a/spot/twaalgos/simulation.cc b/spot/twaalgos/simulation.cc
index a36fdf0ae..afbae6420 100644
--- a/spot/twaalgos/simulation.cc
+++ b/spot/twaalgos/simulation.cc
@@ -233,29 +233,26 @@ namespace spot
                 // common_out[i] is the set of acceptance set numbers common to
                 // all outgoing edges of state i.
                 std::vector<acc_cond::mark_t> common_out(ns);
-                scc_info si(a_, scc_info_options::NONE);
                 for (unsigned s = 0; s < ns; ++s)
                   {
                     bool first = true;
                     for (auto& e : a_->out(s))
-                      {
-                        if (first)
-                          {
-                            common_out[s] = e.acc;
-                            first = false;
-                          }
-                        else if (common_out[s] != e.acc)
-                          {
-                            // If the automaton does not have
-                            // state-based acceptance, do not change
-                            // pull the marks.  Mark the input as
-                            // "not-state-acc" so that we remember
-                            // that.
-                            std::const_pointer_cast<twa_graph>(in)
-                              ->prop_state_acc(false);
-                            goto donotpull;
-                          }
-                      }
+                      if (first)
+                        {
+                          common_out[s] = e.acc;
+                          first = false;
+                        }
+                      else if (common_out[s] != e.acc)
+                        {
+                          // If the automaton does not have
+                          // state-based acceptance, do not change
+                          // pull the marks.  Mark the input as
+                          // "not-state-acc" so that we remember
+                          // that.
+                          std::const_pointer_cast<twa_graph>(in)
+                            ->prop_state_acc(false);
+                          goto donotpull;
+                        }
                   }
                 // Pull the common outgoing sets to the incoming
                 // edges.  Doing so seems to favor cases where states
@@ -654,23 +651,6 @@ namespace spot
                   t.acc = acc;
               }
           }
-        if (!Sba && !Cosimulation && original_->prop_state_acc()
-            && !record_implications_)
-          {
-            // common_in[i] is the set of acceptance set numbers
-            // common to all incoming edges of state i.
-            std::vector<acc_cond::mark_t>
-              common_in(res->num_states(), res->acc().all_sets());
-            for (auto& e : res->edges())
-              common_in[e.dst] &= e.acc;
-            // Push the common incoming sets to the outgoing edges.
-            // Doing so cancels the preprocessing we did in the other
-            // direction, to prevent marks from moving around the
-            // automaton if we apply simulation several times, and to
-            // favor state-based acceptance.
-            for (auto& e : res->edges())
-              e.acc = (e.acc - common_in[e.dst]) | common_in[e.src];
-          }
 
         // If we recorded implications for the determinization
         // procedure, we should not remove unreachable states, as that
@@ -680,6 +660,43 @@ namespace spot
         if (!record_implications_)
           res->purge_unreachable_states();
 
+        // Push the common incoming sets to the outgoing edges.
+        // Doing so cancels the preprocessing we did in the other
+        // direction, to prevent marks from moving around the
+        // automaton if we apply simulation several times, and to
+        // favor state-based acceptance.
+        if (!Sba && !Cosimulation && !record_implications_
+            && original_->prop_state_acc())
+          {
+            // common_in[i] is the set of acceptance set numbers
+            // common to all incoming edges of state i.  Only edges
+            // inside one SCC matter.
+            unsigned ns = res->num_states();
+            std::vector<acc_cond::mark_t> common_in(ns);
+            scc_info si(res, scc_info_options::NONE);
+            for (unsigned s = 0; s < ns; ++s)
+              {
+                unsigned s_scc = si.scc_of(s);
+                bool first = true;
+                for (auto& e: res->out(s))
+                  {
+                    if (si.scc_of(e.dst) != s_scc)
+                      continue;
+                    if (first)
+                      {
+                        common_in[s] = e.acc;
+                        first = false;
+                      }
+                    else
+                      {
+                        common_in[s] &= e.acc;
+                      }
+                  }
+              }
+            for (auto& e : res->edges())
+              e.acc = (e.acc - common_in[e.dst]) | common_in[e.src];
+          }
+
         delete gb;
         res->prop_copy(original_,
                        { false, // state-based acc forced below
diff --git a/tests/core/sim3.test b/tests/core/sim3.test
index f7385db92..8a5a398b4 100755
--- a/tests/core/sim3.test
+++ b/tests/core/sim3.test
@@ -86,3 +86,76 @@ State: 4 {0}
 --END--
 EOF
 diff out expected
+
+# This is a case where the "pull-mark in simulation" optimization
+# introduced by 8959eabad caused the output automaton to be declared
+# weak although it was only inherently weak.
+cat >input <<EOF
+HOA: v1
+States: 8
+Start: 0
+AP: 2 "p0" "p1"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc weak
+--BODY--
+State: 0
+[0&1] 1
+State: 1
+[1] 2
+[!0&1] 3
+State: 2
+[!0&1] 5
+[0&1] 7
+State: 3
+[0&1] 4
+[1] 5
+State: 4 {0}
+[0&1] 4
+[1] 5
+[!0&!1] 6
+State: 5 {0}
+[0&1] 4
+[1] 5
+State: 6 {0}
+[!0&!1] 6
+State: 7
+[!0&1] 5
+[!0&!1] 6
+[0&1] 7
+--END--
+EOF
+cat >expect <<EOF
+HOA: v1
+States: 7
+Start: 0
+AP: 2 "p0" "p1"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc deterministic weak
+--BODY--
+State: 0
+[0&1] 1
+State: 1
+[0&1] 2
+[!0&1] 3
+State: 2
+[!0&1] 3
+[0&1] 6
+State: 3 {0}
+[!0&1] 3
+[0&1] 4
+State: 4 {0}
+[!0&1] 3
+[0&1] 4
+[!0&!1] 5
+State: 5 {0}
+[!0&!1] 5
+State: 6
+[!0&1] 3
+[!0&!1] 5
+[0&1] 6
+--END--
+EOF
+autfilt --small --low input > output
+diff expect output