Tweaks, tidies + addition for State{Probs,List} classes.

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

prism/src/prism/StateListMTBDD.java

@@ -115,6 +115,8 @@ public class StateListMTBDD implements StateList
 		limit = false;
 		outputLog = log;
 		doPrint();
+		if (count == 0)
+			outputLog.println("(none)");
 	}
 	public void printMatlab(PrismLog log)
 	{
@@ -148,7 +150,10 @@ public class StateListMTBDD implements StateList
 		numToPrint = n;
 		outputLog = log;
 		doPrint();
+		if (count == 0)
+			outputLog.println("(none)");
 	}
+	
 	public void printMatlab(PrismLog log, int n)
 	{
 		outputFormat = OutputFormat.MATLAB;

prism/src/prism/StateProbs.java

@@ -54,6 +54,9 @@ public interface StateProbs
 	StateProbs sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException;
 	JDDNode getBDDFromInterval(String relOp, double bound);
 	JDDNode getBDDFromInterval(double lo, double hi);
+	JDDNode getBDDFromCloseValue(double val, double epsilon, boolean abs);
+	JDDNode getBDDFromCloseValueAbs(double val, double epsilon);
+	JDDNode getBDDFromCloseValueRel(double val, double epsilon);
 	void print(PrismLog log) throws PrismException;
 	void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException;
 	void printFiltered(PrismLog log, JDDNode filter) throws PrismException;

prism/src/prism/StateProbsDV.java

@@ -223,6 +223,8 @@ public class StateProbsDV implements StateProbs
 		return "" + getNNZ();
 	}
 	
+	// Filter operations
+	
 	/**
 	 * Get the value of first vector element that is in the (BDD) filter.
 	 */
@@ -255,18 +257,20 @@ public class StateProbsDV implements StateProbs
 		return probs.sumOverBDD(filter, vars, odd);
 	}
 	
-	// do a weighted sum of the elements of the vector and the values the mtbdd passed in
-	// (used for csl reward steady state operator)
-	
+	/**
+	 * Do a weighted sum of the elements of the vector and the values the mtbdd passed in
+	 * (used for CSL reward steady state operator).
+	 */
 	public double sumOverMTBDD(JDDNode mult)
 	{
 		return probs.sumOverMTBDD(mult, vars, odd);
 	}
 	
-	// sum up the elements of the vector, over a subset of its dd vars
-	// store the result in a new StateProbsDV (for newModel)
-	// throws PrismException on out-of-memory
-
+	/**
+	* Sum up the elements of the vector, over a subset of its DD vars
+	* store the result in a new StateProbs (for newModel)
+	* @throws PrismException (on out-of-memory)
+	*/
 	public StateProbs sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException
 	{
 		DoubleVector tmp;
@@ -276,20 +280,54 @@ public class StateProbsDV implements StateProbs
 		return new StateProbsDV(tmp, newModel);
 	}
 	
-	// generate bdd from an interval (relative operator and bound)
-	
+	/**
+	 * 	Generate BDD for states in the given interval
+	 * (interval specified as relational operator and bound)
+	 */
 	public JDDNode getBDDFromInterval(String relOp, double bound)
 	{
 		return probs.getBDDFromInterval(relOp, bound, vars, odd);
 	}
 	
-	// generate bdd from an interval (lower/upper bound)
-	
+	/**
+	 * 	Generate BDD for states in the given interval
+	 * (interval specified as lower/upper bound)
+	 */
 	public JDDNode getBDDFromInterval(double lo, double hi)
 	{
 		return probs.getBDDFromInterval(lo, hi, vars, odd);
 	}
 
+	/**
+	 * 	Generate BDD for states whose value is close to 'value'
+	 * (within either absolute or relative error 'epsilon')
+	 */
+	public JDDNode getBDDFromCloseValue(double value, double epsilon, boolean abs)
+	{
+		if (abs)
+			return probs.getBDDFromCloseValueAbs(value, epsilon, vars, odd);
+		else
+			return probs.getBDDFromCloseValueRel(value, epsilon, vars, odd);
+	}
+	
+	/**
+	 * 	Generate BDD for states whose value is close to 'value'
+	 * (within absolute error 'epsilon')
+	 */
+	public JDDNode getBDDFromCloseValueAbs(double value, double epsilon)
+	{
+		return probs.getBDDFromCloseValueAbs(value, epsilon, vars, odd);
+	}
+	
+	/**
+	 * 	Generate BDD for states whose value is close to 'value'
+	 * (within relative error 'epsilon')
+	 */
+	public JDDNode getBDDFromCloseValueRel(double value, double epsilon)
+	{
+		return probs.getBDDFromCloseValueRel(value, epsilon, vars, odd);
+	}
+	
 	// PRINTING STUFF
 	
 	/**

prism/src/prism/StateProbsMTBDD.java

@@ -346,9 +346,10 @@ public class StateProbsMTBDD implements StateProbs
 		return d;
 	}
 	
-	// do a weighted sum of the elements of a double array and the values the mtbdd passed in
-	// (used for csl reward steady state operator)
-	
+	/**
+	 * Do a weighted sum of the elements of the vector and the values the mtbdd passed in
+	 * (used for CSL reward steady state operator).
+	 */
 	public double sumOverMTBDD(JDDNode mult)
 	{
 		JDDNode tmp;
@@ -364,6 +365,11 @@ public class StateProbsMTBDD implements StateProbs
 		return d;
 	}
 	
+	/**
+	* Sum up the elements of the vector, over a subset of its DD vars
+	* store the result in a new StateProbs (for newModel)
+	* @throws PrismException (on out-of-memory)
+	*/
 	public StateProbs sumOverDDVars(JDDVars sumVars, Model newModel)
 	{
 		JDDNode tmp;
@@ -374,8 +380,10 @@ public class StateProbsMTBDD implements StateProbs
 		return new StateProbsMTBDD(tmp, newModel);
 	}
 	
-	// generate bdd (from an interval: relative operator and bound)
-	
+	/**
+	 * 	Generate BDD for states in the given interval
+	 * (interval specified as relational operator and bound)
+	 */
 	public JDDNode getBDDFromInterval(String relOp, double bound)
 	{
 		JDDNode sol = null;
@@ -397,8 +405,10 @@ public class StateProbsMTBDD implements StateProbs
 		return sol;
 	}
 	
-	// generate bdd from an interval (lower/upper bound)
-	
+	/**
+	 * 	Generate BDD for states in the given interval
+	 * (interval specified as lower/upper bound)
+	 */
 	public JDDNode getBDDFromInterval(double lo, double hi)
 	{
 		JDDNode sol;
@@ -409,6 +419,50 @@ public class StateProbsMTBDD implements StateProbs
 		return sol;
 	}
 
+	/**
+	 * 	Generate BDD for states whose value is close to 'value'
+	 * (within either absolute or relative error 'epsilon')
+	 */
+	public JDDNode getBDDFromCloseValue(double value, double epsilon, boolean abs)
+	{
+		if (abs)
+			return getBDDFromCloseValueAbs(value, epsilon);
+		else
+			return getBDDFromCloseValueRel(value, epsilon);
+	}
+	
+	/**
+	 * 	Generate BDD for states whose value is close to 'value'
+	 * (within absolute error 'epsilon')
+	 */
+	public JDDNode getBDDFromCloseValueAbs(double value, double epsilon)
+	{
+		JDDNode sol;
+		
+		// TODO: infinite cases
+		
+		JDD.Ref(probs);
+		sol = JDD.Interval(probs, value - epsilon, value + epsilon);
+		
+		return sol;
+	}
+	
+	/**
+	 * 	Generate BDD for states whose value is close to 'value'
+	 * (within relative error 'epsilon')
+	 */
+	public JDDNode getBDDFromCloseValueRel(double value, double epsilon)
+	{
+		JDDNode sol;
+		
+		// TODO: wrong
+		
+		JDD.Ref(probs);
+		sol = JDD.Interval(probs, value - epsilon, value + epsilon);
+		
+		return sol;
+	}
+	
 	// PRINTING STUFF
 	
 	/**