From 2697fcddbf65f8c2aa8ec197f011f957a2378708 Mon Sep 17 00:00:00 2001
From: Maximilien Colange <colange@lrde.epita.fr>
Date: Mon, 25 Sep 2017 14:12:12 +0200
Subject: [PATCH] Fix a bug in scc_info, and clarify documentation

* spot/twaalgos/sccinfo.hh, spot/twaalgos/sccinfo.cc: Implement it
* tests/python/sccinfo.py: Test it
* NEWS: Document the fix
---
 NEWS                     |  5 +++++
 spot/twaalgos/sccinfo.cc | 44 +++++++++++++++++++++++-----------------
 spot/twaalgos/sccinfo.hh | 13 +++++++++---
 tests/python/sccinfo.py  | 33 ++++++++++++++++++++++++++++--
 4 files changed, 71 insertions(+), 24 deletions(-)

diff --git a/NEWS b/NEWS
index 137e11256..892f5fbcc 100644
--- a/NEWS
+++ b/NEWS
@@ -70,6 +70,11 @@ New in spot 2.4.0.dev (not yet released)
     will work either on f or its negation.
     (see https://spot.lrde.epita.fr/hierarchy.html for details).
 
+  Bugs fixed:
+
+  - spot::scc_info::determine_unknown_acceptance() incorrectly
+    considered some rejecting SCC as accepting.
+
   Deprecation notices:
 
   (These functions still work but compilers emit warnings.)
diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc
index 67768fa96..1323956eb 100644
--- a/spot/twaalgos/sccinfo.cc
+++ b/spot/twaalgos/sccinfo.cc
@@ -368,26 +368,32 @@ namespace spot
   void scc_info::determine_unknown_acceptance()
   {
     std::vector<bool> k;
-    unsigned n = scc_count();
+    unsigned s = scc_count();
     bool changed = false;
-    for (unsigned s = 0; s < n; ++s)
-      if (!is_rejecting_scc(s) && !is_accepting_scc(s))
-        {
-          if (!aut_->is_existential())
-            throw std::runtime_error("scc_info::determine_unknown_acceptance() "
-                                     "does not support alternating automata");
-          auto& node = node_[s];
-          if (k.empty())
-            k.resize(aut_->num_states());
-          for (auto i: node.states_)
-            k[i] = true;
-          if (mask_keep_accessible_states(aut_, k, node.states_.front())
-              ->is_empty())
-            node.rejecting_ = true;
-          else
-            node.accepting_ = true;
-          changed = true;
-        }
+    // iterate over SCCs in topological order
+    do
+      {
+        --s;
+        if (!is_rejecting_scc(s) && !is_accepting_scc(s))
+          {
+            if (!aut_->is_existential())
+              throw std::runtime_error(
+                  "scc_info::determine_unknown_acceptance() "
+                  "does not support alternating automata");
+            auto& node = node_[s];
+            if (k.empty())
+              k.resize(aut_->num_states());
+            for (auto i: node.states_)
+              k[i] = true;
+            if (mask_keep_accessible_states(aut_, k, node.states_.front())
+                ->is_empty())
+              node.rejecting_ = true;
+            else
+              node.accepting_ = true;
+            changed = true;
+          }
+      }
+    while (s);
     if (changed)
       determine_usefulness();
   }
diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh
index cccf31f8c..92a4b61dd 100644
--- a/spot/twaalgos/sccinfo.hh
+++ b/spot/twaalgos/sccinfo.hh
@@ -246,19 +246,21 @@ namespace spot
       return trivial_;
     }
 
-    /// \brief True if we are sure that the SCC is accepting
+    /// \brief True if we know that the SCC has an accepting cycle
     ///
     /// Note that both is_accepting() and is_rejecting() may return
     /// false if an SCC interesects a mix of Fin and Inf sets.
+    /// Call determine_unknown_acceptance() to decide.
     bool is_accepting() const
     {
       return accepting_;
     }
 
-    // True if we are sure that the SCC is rejecting
+    /// \brief True if we know that all cycles in the SCC are rejecting
     ///
     /// Note that both is_accepting() and is_rejecting() may return
     /// false if an SCC interesects a mix of Fin and Inf sets.
+    /// Call determine_unknown_acceptance() to decide.
     bool is_rejecting() const
     {
       return rejecting_;
@@ -295,9 +297,14 @@ namespace spot
   ///
   /// This takes twa_graph as input and compute its SCCs.  This
   /// class maps all input states to their SCCs, and vice-versa.
-  /// It allows iterating over all SCCs of the automaton, and check
+  /// It allows iterating over all SCCs of the automaton, and checks
   /// their acceptance or non-acceptance.
   ///
+  /// SCC are numbered in reverse topological order, i.e. the SCC of the
+  /// initial state has the highest number, and if s1 is reachable from
+  /// s2, then s1 < s2. Many algorithms depend on this property to
+  /// determine in what order to iterate the SCCs.
+  ///
   /// Additionally this class can be used on alternating automata, but
   /// in this case, universal transitions are handled like existential
   /// transitions.  It still make sense to check which states belong
diff --git a/tests/python/sccinfo.py b/tests/python/sccinfo.py
index 16267fdf4..264a308f7 100644
--- a/tests/python/sccinfo.py
+++ b/tests/python/sccinfo.py
@@ -52,8 +52,6 @@ l3 = si.states_of(3)
 l = sorted(list(l0) + list(l1) + list(l2) + list(l3))
 assert l == [0, 1, 2, 3, 4]
 
-
-
 i = si.initial()
 todo = {i}
 seen = {i}
@@ -77,3 +75,34 @@ assert transi == [(0, 0, 1), (0, 3, 4), (3, 0, 7),
                   (3, 3, 9), (1, 1, 5), (2, 2, 6), (4, 4, 12)]
 
 assert not spot.is_weak_automaton(a, si)
+
+
+a = spot.automaton("""
+HOA: v1
+States: 4
+Start: 0
+AP: 1 "a"
+Acceptance: 2 Inf(0)&Fin(1)
+--BODY--
+State: 0
+[t] 0 {1}
+[t] 1 {0}
+State: 1
+[t] 1 {1}
+[t] 0 {1}
+[t] 2
+State: 2
+[t] 2 {1}
+[t] 3 {0}
+State: 3
+[t] 3 {1}
+[t] 2
+--END--
+""")
+si = spot.scc_info(a)
+si.determine_unknown_acceptance()
+assert si.scc_count() == 2
+assert si.is_accepting_scc(0)
+assert not si.is_rejecting_scc(0)
+assert si.is_rejecting_scc(1)
+assert not si.is_accepting_scc(1)