From c016f561fa4ad1c49600950d8d992dfc8ef9c230 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 2 Oct 2023 11:54:34 +0200
Subject: [PATCH] sccinfo: implement PROCESS_UNREACHABLE_STATES

This is actually used by next patch.

* spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh: Here.
* tests/python/sccinfo.py: Add a small test case.
* NEWS: Mention it.
---
 NEWS                     |  3 +++
 spot/twaalgos/sccinfo.cc | 24 ++++++++++++++++--------
 spot/twaalgos/sccinfo.hh |  9 ++++++++-
 tests/python/sccinfo.py  | 39 ++++++++++++++++++++++++++++++++++++++-
 4 files changed, 65 insertions(+), 10 deletions(-)

diff --git a/NEWS b/NEWS
index b6ad95362..1da2a9cde 100644
--- a/NEWS
+++ b/NEWS
@@ -85,6 +85,9 @@ New in spot 2.11.6.dev  (not yet released)
 
     The above also impacts autfilt --included-in option.
 
+  - spot::scc_info has a new option PROCESS_UNREACHABLE_STATES that
+    causes it to enumerated even unreachable SCCs.
+
   Bugs fixed:
 
   - tgba_determinize()'s use_simulation option would cause it to
diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc
index 7d82c6b81..3abc6fcbd 100644
--- a/spot/twaalgos/sccinfo.cc
+++ b/spot/twaalgos/sccinfo.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2023 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -206,13 +206,21 @@ namespace spot
           }
       };
 
-    // Setup depth-first search from the initial state.  But we may
-    // have a conjunction of initial state in alternating automata.
-    if (initial_state_ == -1U)
-      initial_state_ = aut->get_init_state_number();
-    for (unsigned init: aut->univ_dests(initial_state_))
-      push_init(init);
-
+    if (!!(options & scc_info_options::PROCESS_UNREACHABLE_STATES))
+      {
+        unsigned e = aut->num_states();
+        for (unsigned i = 0; i < e; ++i)
+          push_init(i);
+      }
+    else
+      {
+        // Setup depth-first search from the initial state.  But we may
+        // have a conjunction of initial state in alternating automata.
+        if (initial_state_ == -1U)
+          initial_state_ = aut->get_init_state_number();
+        for (unsigned init: aut->univ_dests(initial_state_))
+          push_init(init);
+      }
     while (!init_states.empty())
       {
         unsigned init = init_states.front();
diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh
index 2de9a1cb8..dc275c517 100644
--- a/spot/twaalgos/sccinfo.hh
+++ b/spot/twaalgos/sccinfo.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement
+// Copyright (C) 2014-2021, 2023 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -393,6 +393,13 @@ namespace spot
     /// Conditionally track states if the acceptance conditions uses Fin.
     /// This is sufficiant for determine_unknown_acceptance().
     TRACK_STATES_IF_FIN_USED = 8,
+    /// Also compute SCCs for the unreachable states.  When this is
+    /// used, SCCs are first enumerated from state 0, and then from
+    /// the next unvisited states.  In other words the initial state
+    /// does not play any role.  If STOP_ON_ACC is used with
+    /// PROCESS_UNREACHABLE_STATES, the enumeration will stop as soon
+    /// as an SCC is found, but that SCC might not be reachable.
+    PROCESS_UNREACHABLE_STATES = 16,
     /// Default behavior: explore everything and track states and succs.
     ALL = TRACK_STATES | TRACK_SUCCS,
   };
diff --git a/tests/python/sccinfo.py b/tests/python/sccinfo.py
index f8ade7e4b..197dd7254 100644
--- a/tests/python/sccinfo.py
+++ b/tests/python/sccinfo.py
@@ -1,6 +1,6 @@
 #!/usr/bin/python3
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2021, 2022 Laboratoire de Recherche et
+# Copyright (C) 2017, 2021, 2022, 2023 Laboratoire de Recherche et
 # Développement de l'EPITA.
 #
 # This file is part of Spot, a model checking library.
@@ -114,3 +114,40 @@ tc.assertTrue(si.is_accepting_scc(0))
 tc.assertFalse(si.is_rejecting_scc(0))
 tc.assertTrue(si.is_rejecting_scc(1))
 tc.assertFalse(si.is_accepting_scc(1))
+
+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}
+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()
+tc.assertEqual(si.scc_count(), 1)
+tc.assertFalse(si.is_accepting_scc(0))
+tc.assertTrue(si.is_rejecting_scc(0))
+si = spot.scc_info_with_options \
+    (a,
+     spot.scc_info_options_PROCESS_UNREACHABLE_STATES |
+     spot.scc_info_options_TRACK_STATES)
+si.determine_unknown_acceptance()
+tc.assertEqual(si.scc_count(), 2)
+tc.assertTrue(si.is_accepting_scc(1))
+tc.assertFalse(si.is_rejecting_scc(1))
+tc.assertTrue(si.is_rejecting_scc(0))
+tc.assertFalse(si.is_accepting_scc(0))