symbolic ECComputer: move findMaximalStableSet to ECComputer, make public

The provided functionality is useful as well when doing further
analysis on (M)ECs outside of the EC computations.



git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12026 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/prism/ECComputer.java

@@ -30,6 +30,7 @@ package prism;
 
 import java.util.List;
 
+import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
 
@@ -132,4 +133,47 @@ public abstract class ECComputer extends PrismComponent
 	{
 		return mecs;
 	}
+
+	/**
+	 * Returns the maximal stable set of states contained in {@code candidateStates},
+	 * i.e. the maximal subset of states which have a choice whose transitions remain in the subset.
+	 *
+	 * <br>[ REFS: <i>result</i>, DEREFS: candidateStates ]
+	 * @param candidateStates BDD for a set of states (over allDDRowVars)
+	 * @return A referenced BDD with the maximal stable set in candidateStates
+	 */
+	public JDDNode findMaximalStableSet(JDDNode candidateStates)
+	{
+		// Store two copies to allow check for fixed point
+		JDDNode current = candidateStates;
+		JDDNode old = JDD.Constant(0);
+		// Fixed point
+		while (!current.equals(old)) {
+			// Remember last set
+			JDD.Deref(old);
+			JDD.Ref(current);
+			old = current;
+			// Find transitions starting in current
+			JDD.Ref(trans01);
+			JDD.Ref(current);
+			JDDNode currTrans = JDD.Apply(JDD.TIMES, trans01, current);
+			// Find transitions starting in current *and* ending in current
+			current = JDD.PermuteVariables(current, allDDRowVars, allDDColVars);
+			JDD.Ref(currTrans);
+			JDDNode currTrans2 = JDD.Apply(JDD.TIMES, currTrans, current);
+			// Find transitions leaving current
+			JDD.Ref(currTrans2);
+			currTrans = JDD.And(currTrans, JDD.Not(currTrans2));
+			// Find choices leaving current
+			currTrans = JDD.ThereExists(currTrans, allDDColVars);
+			// Remove leaving choices
+			currTrans2 = JDD.ThereExists(currTrans2, allDDColVars);
+			currTrans2 = JDD.And(currTrans2, JDD.Not(currTrans));
+			// Keep states with at least one choice
+			current = JDD.ThereExists(currTrans2, allDDNondetVars);
+		}
+		JDD.Deref(old);
+		return current;
+	}
+
 }

prism/src/prism/ECComputerDefault.java

@@ -148,46 +148,6 @@ public class ECComputerDefault extends ECComputer
 		return mecs;
 	}
 
-	/**
-	 * Returns the maximal stable set of states contained in {@code candidateStates},
-	 * i.e. the maximal subset of states which have a choice whose transitions remain in the subset. 
-	 * @param candidateStates BDD for a set of states (over allDDRowVars) (dereferenced after calling this function)
-	 * @return A referenced BDD with the maximal stable set in c
-	 */
-	private JDDNode findMaximalStableSet(JDDNode candidateStates)
-	{
-		// Store two copies to allow check for fixed point 
-		JDDNode current = candidateStates;
-		JDDNode old = JDD.Constant(0);
-		// Fixed point
-		while (!current.equals(old)) {
-			// Remember last set
-			JDD.Deref(old);
-			JDD.Ref(current);
-			old = current;
-			// Find transitions starting in current
-			JDD.Ref(trans01);
-			JDD.Ref(current);
-			JDDNode currTrans = JDD.Apply(JDD.TIMES, trans01, current);
-			// Find transitions starting in current *and* ending in current
-			current = JDD.PermuteVariables(current, allDDRowVars, allDDColVars);
-			JDD.Ref(currTrans);
-			JDDNode currTrans2 = JDD.Apply(JDD.TIMES, currTrans, current);
-			// Find transitions leaving current
-			JDD.Ref(currTrans2);
-			currTrans = JDD.And(currTrans, JDD.Not(currTrans2));
-			// Find choices leaving current
-			currTrans = JDD.ThereExists(currTrans, allDDColVars);
-			// Remove leaving choices
-			currTrans2 = JDD.ThereExists(currTrans2, allDDColVars);
-			currTrans2 = JDD.And(currTrans2, JDD.Not(currTrans));
-			// Keep states with at least one choice
-			current = JDD.ThereExists(currTrans2, allDDNondetVars);
-		}
-		JDD.Deref(old);
-		return current;
-	}
-
 	/**
 	 * Returns the maximal stable set of states contained in {@code candidateStates},
 	 * i.e. the maximal subset of states which have a choice whose transitions remain in the subset.