From abc312efee4de697c5cb3a42463181c4fe8fea1d Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 5 May 2008 21:20:10 +0000
Subject: [PATCH] Reinstated trimming to two SCC computer algs (Carlos).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@784 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/SCCComputerLockstep.java |  5 ++-
 prism/src/prism/SCCComputerSCCFind.java  | 40 ++++++++++++++++++++++--
 2 files changed, 40 insertions(+), 5 deletions(-)

diff --git a/prism/src/prism/SCCComputerLockstep.java b/prism/src/prism/SCCComputerLockstep.java
index 81a4b3a3..54c3d480 100644
--- a/prism/src/prism/SCCComputerLockstep.java
+++ b/prism/src/prism/SCCComputerLockstep.java
@@ -75,10 +75,10 @@ public class SCCComputerLockstep implements SCCComputer
 		JDD.Ref(initialNodes);
 		JDD.Ref(initialEdges);
 		tasks.push(new DecompTask(initialNodes, initialEdges));
-		JDD.Ref(initialNodes);
 		while (!tasks.isEmpty()) {
 			lockstep(tasks.pop());
 		}
+		JDD.Ref(initialNodes);
 		notInSCCs = JDD.And(initialNodes, JDD.Not(allSCCs));
 		log.print(" BSCCs: " + sccs.size());
 		log.println(" Transient states: " + JDD.GetNumMintermsString(notInSCCs, rows.n()));
@@ -191,13 +191,12 @@ public class SCCComputerLockstep implements SCCComputer
 		} */
 
 		// trim nodes
-		/* JDD.Ref(edges);
+		JDD.Ref(edges);
 		nodes = trim(nodes, edges);
 		JDD.Ref(nodes);
 		edges = JDD.Apply(JDD.TIMES, edges, nodes);
 		JDD.Ref(nodes);
 		edges = JDD.Apply(JDD.TIMES, edges, JDD.PermuteVariables(nodes, rows, cols));
-		*/
 		
 		// pick a starting node
 		JDD.Ref(nodes);
diff --git a/prism/src/prism/SCCComputerSCCFind.java b/prism/src/prism/SCCComputerSCCFind.java
index 2f3f2049..7beb8d8c 100644
--- a/prism/src/prism/SCCComputerSCCFind.java
+++ b/prism/src/prism/SCCComputerSCCFind.java
@@ -71,11 +71,13 @@ public class SCCComputerSCCFind implements SCCComputer
 		tasks = new Stack<DecompTask>();
 		JDD.Ref(initialNodes);
 		JDD.Ref(initialEdges);
-		tasks.push(new DecompTask(initialNodes, initialEdges, JDD.Constant(0), JDD.Constant(0)));
-		JDD.Ref(initialNodes);
+		JDDNode trimmedNodes = trim(initialNodes, initialEdges); 
+		JDD.Ref(initialEdges);
+		tasks.push(new DecompTask(trimmedNodes, initialEdges, JDD.Constant(0), JDD.Constant(0)));
 		while (!tasks.isEmpty()) {
 			sccFind(tasks.pop());
 		}
+		JDD.Ref(initialNodes);
 		notInSCCs = JDD.And(initialNodes, JDD.Not(allSCCs));
 		log.print(" BSCCs: " + sccs.size());
 		log.println(" Transient states: " + JDD.GetNumMintermsString(notInSCCs, rows.n()));
@@ -112,6 +114,40 @@ public class SCCComputerSCCFind implements SCCComputer
 		return tmp;
 	}
 	
+	// Trim nodes that have no path to a node in a nontrivial SCC
+	// or have no path from a node in a nontrivial SCC
+	// Refs: result
+	// Derefs: nodes, edges
+	private JDDNode trim(JDDNode nodes, JDDNode edges) {
+		JDDNode old;
+		JDDNode current; 
+		JDDNode img;
+		JDDNode pre;
+		int i = 1;
+
+		JDD.Ref(nodes);
+		current = nodes;
+		do {
+			old = current;
+			JDD.Ref(current);
+			JDD.Ref(edges);
+			img = image(current, edges);
+			JDD.Ref(current);
+			JDD.Ref(edges);
+			pre = preimage(current, edges);
+			current = JDD.And(current, JDD.And(img, pre));
+			if (prism.getVerbose()) {
+				log.println("Trimming pass " + i + ":");
+				JDD.PrintVector(current, rows);
+				i++;
+			}
+		} while (!current.equals(old));
+		JDD.Deref(nodes);
+		JDD.Deref(edges);
+
+		return current;
+	}
+	
 	// Report a SCC found by SCC-Find
 	private void report(JDDNode nodes)
 	{