From ad478bd31a34c3d5ba471e47d2cc1e120e0e065a Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 18 Oct 2016 18:12:45 +0200
Subject: [PATCH] sccinfo: improve detection of rejecting 1-self-loop SCCs

As observed in #188, the smaller.hoa automaton is made only of
1-state/1-self-loop SCCs, for which calling remove_fin is a complete
waste of time.  This patch alone (i.e., without the other changes
suggested by #188) improves the run time of

% autofilt -q --is-unambiguous smaller.hoa

from 38s to 0.05s.

* spot/twaalgos/sccinfo.cc: If a single-state SCC has undeterminate SCC
and only one self-loop, then it is necessarily rejecting.
* NEWS: Mention the change.
---
 NEWS                     |  4 ++++
 spot/twaalgos/sccinfo.cc | 26 +++++++++++++++++++++-----
 2 files changed, 25 insertions(+), 5 deletions(-)

diff --git a/NEWS b/NEWS
index 11d405955..57690f32b 100644
--- a/NEWS
+++ b/NEWS
@@ -4,6 +4,10 @@ New in spot 2.1.2.dev (not yet released)
 
   * is_unambiguous() was rewritten in a more efficient way.
 
+  * scc_info learned to determine the acceptance of simple SCCs made
+  of a single self-loop without ressorting to remove_fin() for complex
+  acceptance conditions.
+
 New in spot 2.1.2 (2016-10-14)
 
   Command-line tools:
diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc
index 6f5d01d17..ace20913b 100644
--- a/spot/twaalgos/sccinfo.cc
+++ b/spot/twaalgos/sccinfo.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
+// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement
 // de l'Epita.
 //
 // This file is part of Spot, a model checking library.
@@ -138,10 +138,26 @@ namespace spot
                     }
                 auto& succ = node_.back().succ_;
                 succ.insert(succ.end(), dests.begin(), dests.end());
-                node_.back().accepting_ =
-                  !triv && root_.back().accepting;
-                node_.back().rejecting_ =
-                  triv || !aut->acc().inf_satisfiable(acc);
+                bool accept = !triv && root_.back().accepting;
+                node_.back().accepting_ = accept;
+                bool reject = triv || !aut->acc().inf_satisfiable(acc);
+                // If the SCC acceptance is indeterminate, but has
+                // only one state and one transition, it is
+                // necessarily rejecting, otherwise we would have
+                // found it to be accepting.
+                if (!accept && !reject && nbs.size() == 1)
+                  {
+                    unsigned selfloop = 0;
+                    for (const auto& e: aut->out(nbs.front()))
+                      if (e.src == e.dst)
+                        {
+                          ++selfloop;
+                          if (selfloop > 1)
+                            break;
+                        }
+                    reject = selfloop <= 1;
+                  }
+                node_.back().rejecting_ = reject;
                 root_.pop_back();
               }
             continue;