From 030ebed367020dab3876fa42def2237cdcdf9d35 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 21 Jun 2019 22:36:33 +0200
Subject: [PATCH] scc_has_rejecting_cycle: rewrite without copy

* spot/twaalgos/genem.hh, spot/twaalgos/genem.cc
(generic_emptiness_check_for_scc): Add a version that takes an acc.
* spot/twaalgos/isweakscc.cc (scc_has_rejecting_cycle): Use
generic_emptiness_check_for_scc.
---
 spot/twaalgos/genem.cc     | 15 ++++++++++++---
 spot/twaalgos/genem.hh     |  9 +++++++++
 spot/twaalgos/isweakscc.cc | 18 ++++--------------
 3 files changed, 25 insertions(+), 17 deletions(-)

diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc
index 9b53b2a90..c4e541f72 100644
--- a/spot/twaalgos/genem.cc
+++ b/spot/twaalgos/genem.cc
@@ -75,6 +75,8 @@ namespace spot
         else
           {
             int fo = acc.fin_one();
+            if (fo < 0)
+              std::cerr << autacc << acc << '\n';
             assert(fo >= 0);
             // Try to accept when Fin(fo) == true
             acc_cond::mark_t fo_m = {(unsigned) fo};
@@ -160,9 +162,16 @@ namespace spot
   bool generic_emptiness_check_for_scc(const scc_info& si,
                                        unsigned scc)
   {
-    if (SPOT_UNLIKELY(!si.get_aut()->is_existential()))
-      throw std::runtime_error("generic_emptiness_check_for_scc() "
-                               "does not support alternating automata");
     return is_scc_empty(si, scc, si.get_aut()->acc(), nullptr);
   }
+
+  bool
+  generic_emptiness_check_for_scc(const scc_info& si, unsigned scc,
+                                  const acc_cond& forced_acc)
+  {
+    if (si.is_trivial(scc))
+      return true;
+    return scc_split_check(si, scc, forced_acc, nullptr, {});
+  }
+
 }
diff --git a/spot/twaalgos/genem.hh b/spot/twaalgos/genem.hh
index 525f73b09..e35b3290d 100644
--- a/spot/twaalgos/genem.hh
+++ b/spot/twaalgos/genem.hh
@@ -40,4 +40,13 @@ namespace spot
   /// \brief Emptiness check of one SCC, for any acceptance condition.
   SPOT_API bool
   generic_emptiness_check_for_scc(const scc_info& si, unsigned scc);
+
+  /// \ingroup emptiness_check_algorithms
+  /// \brief Emptiness check of one SCC, for any acceptance condition.
+  ///
+  /// This version makes it possible to ignore the acceptance
+  /// condition of the automaton, and use \a forced_acc.
+  SPOT_API bool
+  generic_emptiness_check_for_scc(const scc_info& si, unsigned scc,
+                                  const acc_cond& forced_acc);
 }
diff --git a/spot/twaalgos/isweakscc.cc b/spot/twaalgos/isweakscc.cc
index 04a9f07db..ff2254302 100644
--- a/spot/twaalgos/isweakscc.cc
+++ b/spot/twaalgos/isweakscc.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2012-2019 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -20,7 +20,7 @@
 #include "config.h"
 #include <spot/tl/formula.hh>
 #include <spot/twaalgos/isweakscc.hh>
-#include <spot/twaalgos/mask.hh>
+#include <spot/twaalgos/genem.hh>
 
 namespace spot
 {
@@ -38,18 +38,8 @@ namespace spot
   {
     if (SPOT_UNLIKELY(scc >= map.scc_count()))
       invalid_scc_number("scc_has_rejecting_cycle");
-    auto aut = map.get_aut();
-    // We check that by cloning the SCC and complementing its
-    // acceptance condition.
-    std::vector<bool> keep(aut->num_states(), false);
-    auto& states = map.states_of(scc);
-    for (auto s: states)
-      keep[s] = true;
-    auto sccaut = mask_keep_accessible_states(aut, keep, states.front(),
-                                              /* drop_univ_branch = */ true);
-    sccaut->set_acceptance(sccaut->acc().num_sets(),
-                           sccaut->get_acceptance().complement());
-    return !sccaut->is_empty();
+    acc_cond neg_acc = map.get_aut()->get_acceptance().complement();
+    return !generic_emptiness_check_for_scc(map, scc, neg_acc);
   }
 
   bool