From 15c6fd9562499a574daaddd6be7a88000ddf373d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sun, 12 Feb 2017 01:37:52 +0100
Subject: [PATCH] alternation: fix detection of non-weak automata

Fixes #218.

* spot/twaalgos/alternation.cc: Adjust check.
* tests/core/alternating.test: Add test case from #218.
* NEWS: Mention the bug.
---
 NEWS                         |  3 ++
 spot/twaalgos/alternation.cc | 62 +++++++++++++++++-------------------
 tests/core/alternating.test  | 22 ++++++++++++-
 3 files changed, 54 insertions(+), 33 deletions(-)

diff --git a/NEWS b/NEWS
index 02e580028..fb61a5afb 100644
--- a/NEWS
+++ b/NEWS
@@ -27,6 +27,9 @@ New in spot 2.3.0.dev (not yet released)
     spot::acc_word::op and spot::acc_word::type had to be renamed as
     spot::acc_word::sub.op and spot::acc_word::sub.type.
 
+  - alternation_removal() was not always reporting the unsupported
+    non-weak automata.
+
 New in spot 2.3 (2017-01-19)
 
   Build:
diff --git a/spot/twaalgos/alternation.cc b/spot/twaalgos/alternation.cc
index ad2cd7dad..9af21b332 100644
--- a/spot/twaalgos/alternation.cc
+++ b/spot/twaalgos/alternation.cc
@@ -104,33 +104,34 @@ namespace spot
       unsigned reject_1_count_ = 0;
       std::set<unsigned> true_states_;
 
-      bool ensure_weak_state(unsigned src, unsigned scc)
+      bool ensure_weak_scc(unsigned scc)
       {
         bool first = true;
         bool reject_cycle = false;
         acc_cond::mark_t m = 0U;
-        for (auto& t: aut_->out(src))
-          for (unsigned d: aut_->univ_dests(t.dst))
-            if (si_.scc_of(d) == scc)
-              {
-                if (first)
-                  {
-                    first = false;
-                    m = t.acc;
-                    reject_cycle = !aut_->acc().accepting(m);
-                  }
-                else if (m != t.acc)
-                  {
-                    throw std::runtime_error
-                      ("alternation_removal() only work with weak "
-                       "alternating automata");
-                  }
-                // In case of a universal edge we only
-                // need to check the first destination
-                // inside the SCC, because the other
-                // have the same t.acc.
-                break;
-              }
+        for (unsigned src: si_.states_of(scc))
+          for (auto& t: aut_->out(src))
+            for (unsigned d: aut_->univ_dests(t.dst))
+              if (si_.scc_of(d) == scc)
+                {
+                  if (first)
+                    {
+                      first = false;
+                      m = t.acc;
+                      reject_cycle = !aut_->acc().accepting(m);
+                    }
+                  else if (m != t.acc)
+                    {
+                      throw std::runtime_error
+                        ("alternation_removal() only work with weak "
+                         "alternating automata");
+                    }
+                  // In case of a universal edge we only
+                  // need to check the first destination
+                  // inside the SCC, because the other
+                  // have the same t.acc.
+                  break;
+                }
         return reject_cycle;
       }
 
@@ -155,10 +156,11 @@ namespace spot
                     // decide rejecting/accepting.
                     assert(si_.is_accepting_scc(n));
 
-                    unsigned s = si_.states_of(n).front();
-                    bool rej = ensure_weak_state(s, n);
+                    // Catch unsupported types of automata
+                    bool rej = ensure_weak_scc(n);
                     assert(rej == false);
                     // Detect if it is a "true state"
+                    unsigned s = si_.states_of(n).front();
                     auto& ss = g.state_storage(s);
                     if (ss.succ == ss.succ_tail)
                       {
@@ -168,14 +170,10 @@ namespace spot
                       }
                   }
               }
-            else
+            else if (ensure_weak_scc(n))
               {
-                for (auto src: si_.states_of(n))
-                  if (ensure_weak_state(src, n))
-                    {
-                      class_of_[n] = reject_more;
-                      has_reject_more_ = true;
-                    }
+                class_of_[n] = reject_more;
+                has_reject_more_ = true;
               }
           }
       }
diff --git a/tests/core/alternating.test b/tests/core/alternating.test
index 1fcfb7dc6..86069a866 100644
--- a/tests/core/alternating.test
+++ b/tests/core/alternating.test
@@ -374,5 +374,25 @@ State: 2 "t"
 [t] 2
 --END--
 EOF
-autfilt --tgba in >out 2>&1 && exit 1
+autfilt --tgba in 2>out && exit 1
+grep 'autfilt.*weak.*alternating' out
+
+cat >in <<EOF
+HOA: v1
+States: 4
+AP: 2 "a" "b"
+Start: 0&1
+Acceptance: 1 Inf(0)
+--BODY--
+State: 0 {0}
+[0] 2
+State: 2 /*{0}*/
+[0] 0
+State: 1 {0}
+[1] 3
+State: 3 /*{0}*/
+[1] 1
+--END--
+EOF
+autfilt --tgba in 2>out && exit 1
 grep 'autfilt.*weak.*alternating' out