symbolic ECComputerDefault: remove the two numeric methods in EC computations

findMaximalStableSetOld has not been in use since 2013 (replaced by findMaximalStableset),
maxStableSetTrans is replaced by getStableTransReln.

Methods were private, so we just remove instead of marking as deprecated.


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

prism/src/prism/ECComputerDefault.java

@@ -147,68 +147,4 @@ 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
-	 * 
-	 * Old version of the code (uses probability sum, which shouldn't be needed).
-	 */
-	private JDDNode findMaximalStableSetOld(JDDNode candidateStates)
-	{
-		JDDNode old = JDD.Constant(0);
-		JDDNode current = candidateStates;
-
-		while (!current.equals(old)) {
-			JDD.Deref(old);
-			JDD.Ref(current);
-			old = current;
-
-			JDD.Ref(current);
-			JDD.Ref(trans);
-			// Select transitions starting in current
-			JDDNode currTrans = JDD.Apply(JDD.TIMES, trans, current);
-			// Select transitions starting in current and ending in current
-			JDDNode tmp = JDD.PermuteVariables(current, allDDRowVars, allDDColVars);
-			tmp = JDD.Apply(JDD.TIMES, currTrans, tmp);
-			// Sum all successor probabilities for each (state, action) tuple
-			tmp = JDD.SumAbstract(tmp, allDDColVars);
-			// If the sum for a (state,action) tuple is 1,
-			// there is an action that remains in the stable set with prob 1
-			tmp = JDD.GreaterThan(tmp, 1 - sumRoundOff);
-			// Without fairness, we just need one action per state
-			current = JDD.ThereExists(tmp, allDDNondetVars);
-		}
-		JDD.Deref(old);
-		return current;
-	}
-
-	/**
-	 * Returns the transition relation of a stable set
-	 * 
-	 * @param b BDD of a stable set (dereferenced after calling this function)
-	 * @return referenced BDD of the transition relation restricted to the stable set
-	 */
-	private JDDNode maxStableSetTrans(JDDNode b)
-	{
-
-		JDD.Ref(b);
-		JDD.Ref(trans);
-		// Select transitions starting in b
-		JDDNode currTrans = JDD.Apply(JDD.TIMES, trans, b);
-		JDDNode mask = JDD.PermuteVariables(b, allDDRowVars, allDDColVars);
-		// Select transitions starting in current and ending in current
-		mask = JDD.Apply(JDD.TIMES, currTrans, mask);
-		// Sum all successor probabilities for each (state, action) tuple
-		mask = JDD.SumAbstract(mask, allDDColVars);
-		// If the sum for a (state,action) tuple is 1,
-		// there is an action that remains in the stable set with prob 1
-		mask = JDD.GreaterThan(mask, 1 - sumRoundOff);
-		// select the transitions starting in these tuples
-		JDD.Ref(trans01);
-		JDDNode stableTrans01 = JDD.And(trans01, mask);
-		// Abstract over actions
-		return JDD.ThereExists(stableTrans01, allDDNondetVars);
-	}
 }