From 3bd95c32e777047c158d4af18e4bdbae80513eb7 Mon Sep 17 00:00:00 2001
From: Alexandre Lewkowicz <lewkow_a@epita.fr>
Date: Tue, 22 Sep 2015 14:06:39 +0200
Subject: [PATCH] safra: Remove paths when leaving an SCC

* src/tests/safra.cc:  Add option.
* src/twaalgos/safra.cc, src/twaalgos/safra.hh:  When a node leaves an
SCC, all the subpaths of that node are removed.
---
 src/tests/safra.cc    | 13 ++++++++++---
 src/twaalgos/safra.cc | 20 ++++++++++++++------
 src/twaalgos/safra.hh |  8 ++++++--
 3 files changed, 30 insertions(+), 11 deletions(-)

diff --git a/src/tests/safra.cc b/src/tests/safra.cc
index 34c1d566f..cde9ce178 100644
--- a/src/tests/safra.cc
+++ b/src/tests/safra.cc
@@ -45,6 +45,7 @@ int help()
 int main(int argc, char* argv[])
 {
   bool emit_scc = false;
+  bool track_scc = false;
   bool sim = false;
   bool in_hoa = false;
   bool in_ltl = false;
@@ -80,8 +81,12 @@ int main(int argc, char* argv[])
         pretty_print = true;
       else if (!strncmp(argv[i], "-b", 2))
         sim = true;
-      else if (!strncmp(argv[i], "--emit_scc", 2))
+      else if (!strncmp(argv[i], "--emit_scc", 10))
         emit_scc = true;
+      else if (!strncmp(argv[i], "--track_scc", 11))
+        track_scc = true;
+      else
+        std::cerr << "Warning: " << argv[i] << " not used\n";
     }
 
   if (!input)
@@ -99,7 +104,8 @@ int main(int argc, char* argv[])
       spot::translator trans(dict);
       trans.set_pref(spot::postprocessor::Deterministic);
       auto tmp = trans.run(f);
-      res = spot::tgba_determinisation(tmp, sim, pretty_print, emit_scc);
+      res = spot::tgba_determinisation(tmp, sim, pretty_print, emit_scc,
+                                       track_scc);
       f->destroy();
     }
   else if (in_hoa)
@@ -108,7 +114,8 @@ int main(int argc, char* argv[])
       auto aut = spot::parse_aut(input, pel, dict);
       if (spot::format_parse_aut_errors(std::cerr, input, pel))
         return 2;
-      res = tgba_determinisation(aut->aut, sim, pretty_print, emit_scc);
+      res = tgba_determinisation(aut->aut, sim, pretty_print, emit_scc,
+                                 track_scc);
     }
   res->merge_edges();
 
diff --git a/src/twaalgos/safra.cc b/src/twaalgos/safra.cc
index 6bdf5e833..4592736f3 100644
--- a/src/twaalgos/safra.cc
+++ b/src/twaalgos/safra.cc
@@ -24,7 +24,6 @@
 
 #include "safra.hh"
 #include "twaalgos/degen.hh"
-#include "twaalgos/sccinfo.hh"
 #include "twaalgos/simulation.hh"
 
 namespace spot
@@ -174,7 +173,9 @@ namespace spot
                              std::unordered_map<bdd,
                                              std::pair<unsigned, unsigned>,
                                              bdd_hash>& deltas,
-                              succs_t& res) const
+                              succs_t& res,
+                              const scc_info& scc,
+                              bool track_scc) const
   {
     // Given a bdd returns index of associated safra_state in res
     std::map<unsigned, unsigned> bdd2num;
@@ -200,7 +201,14 @@ namespace spot
                                      bddnums[j]);
                   }
                 safra_state& ss = res[idx].first;
-                ss.update_succ(node.second, t.dst, t.acc);
+                (void) scc;
+                ss.update_succ(std::vector<node_helper::brace_t>(1, 0), t.dst, t.acc);
+                // Check if we are leaving the SCC, if so we delete all the
+                // braces as no cycles can be found with that node
+                if (track_scc && scc.scc_of(node.first) != scc.scc_of(t.dst))
+                  ss.update_succ({ 0 }, t.dst, t.acc);
+                else
+                  ss.update_succ(node.second, t.dst, t.acc);
                 assert(ss.nb_braces_.size() == ss.is_green_.size());
               }
           }
@@ -364,7 +372,7 @@ namespace spot
         unsigned nb_braces = val;
         // One brace set
         is_green_.assign(nb_braces, true);
-        // First brace has init_state hence one state inside the first braces.
+        // Newly created states are the empty mocrstate
         nb_braces_.assign(nb_braces, 0);
       }
   }
@@ -394,7 +402,7 @@ namespace spot
 
   twa_graph_ptr
   tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation,
-                       bool pretty_print, bool emit_scc)
+                       bool pretty_print, bool emit_scc, bool track_scc)
   {
     // Degeneralize
     twa_graph_ptr aut = spot::degeneralize_tba(a);
@@ -468,7 +476,7 @@ namespace spot
         safra_state curr = todo.front();
         unsigned src_num = seen.find(curr)->second;
         todo.pop_front();
-        curr.compute_succs(aut, bddnums, deltas, succs);
+        curr.compute_succs(aut, bddnums, deltas, succs, scc, track_scc);
         for (auto s: succs)
           {
             auto i = seen.find(s.first);
diff --git a/src/twaalgos/safra.hh b/src/twaalgos/safra.hh
index 8b9bb9514..70e4a9934 100644
--- a/src/twaalgos/safra.hh
+++ b/src/twaalgos/safra.hh
@@ -24,6 +24,7 @@
 
 #include "misc/bddlt.hh"
 #include "twa/twagraph.hh"
+#include "twaalgos/sccinfo.hh"
 
 namespace spot
 {
@@ -52,7 +53,9 @@ namespace spot
                           std::unordered_map<bdd,
                                              std::pair<unsigned, unsigned>,
                                              bdd_hash>& deltas,
-                           succs_t& res) const;
+                           succs_t& res,
+                           const scc_info& scc,
+                           bool track_scc = false) const;
     // The outermost brace of each node cannot be green
     void ungreenify_last_brace();
     // Used when creating the list of successors
@@ -78,5 +81,6 @@ namespace spot
   tgba_determinisation(const const_twa_graph_ptr& aut,
                        bool bisimulation = false,
                        bool pretty_print = false,
-                       bool emit_scc = false);
+                       bool emit_scc = false,
+                       bool track_scc = false);
 }