From c8cf86b081da7416211c9f6949e67fc6cb133f8d Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Tue, 7 Jul 2015 21:04:10 +0200
Subject: [PATCH] sccinfo: stop keeping track of conditions between SCCs

They are unused.

* src/twaalgos/sccinfo.cc, src/twaalgos/sccinfo.hh: Do
not keep track of conditions between two SCCs.
* src/twaalgos/minimize.cc, src/twaalgos/ltl2tgba_fm.cc:
Adjust.
---
 src/twaalgos/ltl2tgba_fm.cc |  4 ++--
 src/twaalgos/minimize.cc    |  6 +++---
 src/twaalgos/sccinfo.cc     | 29 ++++++++---------------------
 src/twaalgos/sccinfo.hh     | 12 +-----------
 4 files changed, 14 insertions(+), 37 deletions(-)

diff --git a/src/twaalgos/ltl2tgba_fm.cc b/src/twaalgos/ltl2tgba_fm.cc
index 77806ff24..8c13b2787 100644
--- a/src/twaalgos/ltl2tgba_fm.cc
+++ b/src/twaalgos/ltl2tgba_fm.cc
@@ -1198,8 +1198,8 @@ namespace spot
 	  if (!coacc)
 	    {
 	      // ... or if any of its successors is coaccessible.
-	      for (auto& i: sm->succ(n))
-		if (coaccessible[i.dst])
+	      for (unsigned i: sm->succ(n))
+		if (coaccessible[i])
 		  {
 		    coacc = true;
 		    break;
diff --git a/src/twaalgos/minimize.cc b/src/twaalgos/minimize.cc
index 7127f1b39..9eeea160b 100644
--- a/src/twaalgos/minimize.cc
+++ b/src/twaalgos/minimize.cc
@@ -545,10 +545,10 @@ namespace spot
 	  // Also SCCs are useless if all their successor are
 	  // useless.
 	  unsigned l = k;
-	  for (auto& j: succ)
+	  for (unsigned j: succ)
 	    {
-	      is_useless &= useless[j.dst];
-	      unsigned dj = d[j.dst];
+	      is_useless &= useless[j];
+	      unsigned dj = d[j];
 	      if (dj < l)
 		l = dj;
 	    }
diff --git a/src/twaalgos/sccinfo.cc b/src/twaalgos/sccinfo.cc
index 80d3805ee..6b19b63a4 100644
--- a/src/twaalgos/sccinfo.cc
+++ b/src/twaalgos/sccinfo.cc
@@ -127,7 +127,7 @@ namespace spot
 		// Record the transition between the SCC being popped
 		// and the previous SCC.
 		if (!root_.empty())
-		  root_.front().node.succ_.emplace_back(cond, num);
+		  root_.front().node.succ_.emplace_back(num);
 	      }
 	    continue;
 	  }
@@ -162,15 +162,10 @@ namespace spot
 	    // Record that there is a transition from this SCC to the
 	    // dest SCC labelled with cond.
 	    auto& succ = root_.front().node.succ_;
-	    scc_succs::iterator i = std::find_if(succ.begin(), succ.end(),
-						 [spi](const scc_trans& x) {
-						   return (x.dst ==
-							   (unsigned) spi);
-						 });
+	    scc_succs::iterator i =
+	      std::find(succ.begin(), succ.end(), (unsigned) spi);
 	    if (i == succ.end())
-	      succ.emplace_back(cond, spi);
-	    else
-	      i->cond |= cond;
+	      succ.emplace_back(spi);
 	    continue;
 	  }
 
@@ -243,8 +238,8 @@ namespace spot
 	    continue;
 	  }
 	node_[i].useful_ = false;
-	for (auto j: node_[i].succ())
-	  if (node_[j.dst].is_useful())
+	for (unsigned j: node_[i].succ())
+	  if (node_[j].is_useful())
 	    {
 	      node_[i].useful_ = true;
 	      break;
@@ -358,19 +353,11 @@ namespace spot
 	}
 	out << "\"]\n";
 
-	for (auto& i: m->succ(state))
+	for (unsigned dest: m->succ(state))
 	  {
-	    int dest = i.dst;
-	    bdd label = i.cond;
-
-	    out << "  " << state << " -> " << dest
-		<< " [label=\"";
-	    escape_str(out, bdd_format_formula(aut->get_dict(), label));
-	    out << "\"]\n";
-
+	    out << "  " << state << " -> " << dest << '\n';
 	    if (seen[dest])
 	      continue;
-
 	    seen[dest] = true;
 	    q.push(dest);
 	  }
diff --git a/src/twaalgos/sccinfo.hh b/src/twaalgos/sccinfo.hh
index 25a2051a0..04471ab03 100644
--- a/src/twaalgos/sccinfo.hh
+++ b/src/twaalgos/sccinfo.hh
@@ -27,17 +27,7 @@ namespace spot
   class SPOT_API scc_info
   {
   public:
-    struct scc_trans
-    {
-      scc_trans(bdd cond, unsigned dst)
-	: cond(cond), dst(dst)
-      {
-      }
-      bdd cond;
-      unsigned dst;
-    };
-
-    typedef std::vector<scc_trans> scc_succs;
+    typedef std::vector<unsigned> scc_succs;
 
     class scc_node
     {