StateValues: Consolidate documentation, add REF/DEREF information

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

prism/src/prism/StateValues.java

@@ -32,40 +32,208 @@ import jdd.JDDNode;
 import jdd.JDDVars;
 import parser.ast.RelOp;
 
-// Interface for classes for state-indexed vectors of (integer or double) values
-
+/**
+ * Interface for classes for state-indexed vectors of (integer or double) values
+ */
 public interface StateValues extends StateVector
 {
+	/** Converts to StateValuesDV, destroys (clear) this vector */
 	StateValuesDV convertToStateValuesDV();
+
+	/** Converts to StateValuesMTBDD, destroys (clear) this vector */
 	StateValuesMTBDD convertToStateValuesMTBDD();
+
+	/**
+	 * Set the elements of this vector by reading them in from a file.
+	 */
 	void readFromFile(File file) throws PrismException;
+
+	/** Round the values of this vector to the given number of decimal places. */
 	void roundOff(int places);
+
+	/** Subtract all values of this vector from 1 */
 	void subtractFromOne();
+
+	/**
+	 * Add the values of the other StateValues vector to the values of this vector.
+	 * <br>
+	 * The other StateValues vector has to have the same class as this vector.
+	 */
 	void add(StateValues sp);
+
+	/** Multiplies the values of this vector with the constant {@code d}. */
 	void timesConstant(double d);
+
+	/**
+	 * Compute dot (inner) product of this and another vector.
+	 * <br>
+	 * The other StateValues vector has to have the same class as this vector.
+	 */
 	double dotProduct(StateValues sp);
+
+	/**
+	 * Filter this vector using a BDD (set elements not in filter to 0).
+	 * <br>[ DEREFS: <i>none</i> ]
+	 */
 	void filter(JDDNode filter);
+
+	/**
+	 * Apply max operator, i.e. vec[i] = max(vec[i], vec2[i]), where vec2 is an MTBDD
+	 * <br>[ DEREFS: <i>none</i> ]
+	 */
 	public void maxMTBDD(JDDNode vec2);
+
+	/** Clear the stored information. */
 	void clear();
+
+	/** Get the number of non-zero values in this vector. */
 	int getNNZ();
+
+	/** Get the number of non-zero values in this vector as a String. */
 	String getNNZString();
+
+	/**
+	 * Get the value of the first vector element that is in the (BDD) filter.
+	 * <br>
+	 * Should be called with a non-empty filter. For an empty filter, will return
+	 * {@code Double.NaN}.
+	 * <br>[ DEREFS: <i>none</i> ]
+	 */
 	double firstFromBDD(JDDNode filter);
+
+	/**
+	 * Get the minimum value of those that are in the (BDD) filter.
+	 * <br>
+	 * If the filter is empty for this vector, returns positive infinity.
+	 * <br>[ DEREFS: <i>none</i> ]
+	 */
 	double minOverBDD(JDDNode filter);
+
+	/**
+	 * Get the maximum value of those that are in the (BDD) filter.
+	 * <br>
+	 * If the filter is empty for this vector, returns negative infinity.
+	 * <br>[ DEREFS: <i>none</i> ]
+	 */
 	double maxOverBDD(JDDNode filter);
+
+	/**
+	 * Get the sum of those elements that are in the (BDD) filter.
+	 * If the filter is empty for this vector, returns 0.
+ 	 * <br>[ DEREFS: <i>none</i> ]
+	 */
 	double sumOverBDD(JDDNode filter);
+
+	/**
+	 * Do a weighted sum of the elements of the vector and the values the MTBDD passed in
+	 * (used for CSL reward steady state operator).
+	 */
 	double sumOverMTBDD(JDDNode mult);
+
+	/**
+	* Sum up the elements of the vector, over a subset of its DD vars,
+	* store the result in a new StateValues (for newModel).
+	* <br>[ DEREFS: <i>none</i> ]
+	*/
 	StateValues sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException;
+
+	/** Returns an Object with the value of the i-th entry in this vector. */
 	Object getValue(int i);
+
+	/**
+	 * Generate BDD for states in the given interval
+	 * (interval specified as relational operator and bound)
+	 * <br>[ REFS: <i>result</i> ]
+	 */
 	JDDNode getBDDFromInterval(String relOpString, double bound);
+
+	/**
+	 * Generate BDD for states in the given interval
+	 * (interval specified as relational operator and bound)
+	 * <br>[ REFS: <i>result</i> ]
+	 */
 	JDDNode getBDDFromInterval(RelOp relOp, double bound);
+
+	/**
+	 * Generate BDD for states in the given interval
+	 * (interval specified as inclusive lower/upper bound)
+	 * <br>[ REFS: <i>result</i> ]
+	 */
 	JDDNode getBDDFromInterval(double lo, double hi);
+
+	/**
+	 * Generate BDD for states whose value is close to 'value'
+	 * (within either absolute or relative error 'epsilon')
+	 * <br>[ REFS: <i>result</i> ]
+	 * @param val the value
+	 * @param epsilon the error bound
+	 * @param abs true for absolute error calculation
+	 */
 	JDDNode getBDDFromCloseValue(double val, double epsilon, boolean abs);
+
+	/**
+	 * Generate BDD for states whose value is close to 'value'
+	 * (within absolute error 'epsilon')
+	 * <br>[ REFS: <i>result</i> ]
+	 * @param val the value
+	 * @param epsilon the error bound
+	 */
 	JDDNode getBDDFromCloseValueAbs(double val, double epsilon);
+
+	/**
+	 * Generate BDD for states whose value is close to 'value'
+	 * (within relative error 'epsilon')
+	 * <br>[ REFS: <i>result</i> ]
+	 * @param val the value
+	 * @param epsilon the error bound
+	 */
 	JDDNode getBDDFromCloseValueRel(double val, double epsilon);
+
+	/**
+	 * Print vector to a log/file (non-zero entries only)
+	 */
 	void print(PrismLog log) throws PrismException;
+
+	/**
+	 * Print vector to a log/file.
+	 * @param log The log
+	 * @param printSparse Print non-zero elements only?
+	 * @param printMatlab Print in Matlab format?
+	 * @param printStates Print states (variable values) for each element?
+	 */
 	void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException;
+
+	/**
+	 * Print vector to a log/file.
+	 * @param log The log
+	 * @param printSparse Print non-zero elements only?
+	 * @param printMatlab Print in Matlab format?
+	 * @param printStates Print states (variable values) for each element?
+	 * @param printIndices Print state indices for each element?
+	 */
 	void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException;
+
+	/**
+	 * Print part of a vector to a log/file (non-zero entries only).
+	 * <br>[ DEREFS: <i>none</i> ]
+	 * @param log The log
+	 * @param filter A BDD specifying which states to print for.
+	 */
 	void printFiltered(PrismLog log, JDDNode filter) throws PrismException;
+
+	/**
+	 * Print part of a vector to a log/file (non-zero entries only).
+	 * <br>[ DEREFS: <i>none</i> ]
+	 * @param log The log
+	 * @param filter A BDD specifying which states to print for.
+	 * @param printSparse Print non-zero elements only?
+	 * @param printMatlab Print in Matlab format?
+	 * @param printStates Print states (variable values) for each element?
+	 */
 	void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException;
+
+	/**
+	 * Make a (deep) copy of this vector
+	 */
 	StateValues deepCopy() throws PrismException; 
 }

prism/src/prism/StateValuesDV.java

@@ -35,20 +35,25 @@ import parser.VarList;
 import parser.ast.RelOp;
 import parser.type.*;
 
-;
-
-// Class for state-indexed vectors of (integer or double) values, represented by a vector of doubles
-
+/**
+ * Class for state-indexed vectors of (integer or double) values,
+ * represented by a vector of doubles.
+ */
 public class StateValuesDV implements StateValues
 {
-	// Double vector storing values
+	/** Double vector storing values */
 	DoubleVector values;
 
 	// info from model
+	/** The underlying model */
 	Model model;
+	/** The BDD row variables of the underlying model */
 	JDDVars vars;
+	/** The number of BDD row variables in the underlying model */
 	int numVars;
+	/** The ODD for the reachable states of the underlying model */
 	ODDNode odd;
+	/** The VarList of the underlying model*/
 	VarList varList;
 
 	// stuff to keep track of variable values in print method
@@ -58,17 +63,25 @@ public class StateValuesDV implements StateValues
 	int currentVarLevel;
 	int counter;
 
-	// log for output from print method
+	/** Log for output from print method */
 	PrismLog outputLog;
 
-	// flags
+	/** Flag: printSparse (only non-zero values) */
 	boolean printSparse = true;
+	/** Flag: printMatlab */
 	boolean printMatlab = false;
+	/** Flag: printStates (variable values on the model) */
 	boolean printStates = true;
+	/** Flag: printIndizes (indizes for the states) */
 	boolean printIndices = true;
 
 	// CONSTRUCTORS
 
+	/**
+	 * Constructor from a double vector (which is stored, not copied).
+	 * @param values the double vector
+	 * @param model the underlying model
+	 */
 	public StateValuesDV(DoubleVector values, Model model)
 	{
 		int i;
@@ -91,25 +104,34 @@ public class StateValuesDV implements StateValues
 		varValues = new int[varList.getNumVars()];
 	}
 
+	/**
+	 * Constructor from an MTBDD.
+	 * <br>
+	 * Note: The JDDNode dd must only be non-zero for reachable states
+	 * (otherwise bad things happen)
+	 * <br>[ DEREFS: <i>none</i> ]
+	 * @param dd the double vector
+	 * @param model the underlying model
+	 */
 	public StateValuesDV(JDDNode dd, Model model)
 	{
-		// construct double vector from an mtbdd
-		// (note: dd must only be non-zero for reachable states)
-		// (otherwise bad things happen)
+		// TODO: Enforce/check that dd is zero for all non-reachable states
 		this(new DoubleVector(dd, model.getAllDDRowVars(), model.getODD()), model);
 	}
 
 	// CONVERSION METHODS
 
-	// convert to StateValuesDV (nothing to do)
+	@Override
 	public StateValuesDV convertToStateValuesDV()
 	{
+		// convert to StateValuesDV (nothing to do)
 		return this;
 	}
 
-	// convert to StateValuesMTBDD, destroy (clear) old vector
+	@Override
 	public StateValuesMTBDD convertToStateValuesMTBDD()
 	{
+		// convert to StateValuesMTBDD, destroy (clear) old vector
 		StateValuesMTBDD res = new StateValuesMTBDD(values.convertToMTBDD(vars, odd), model);
 		clear();
 		return res;
@@ -125,9 +147,7 @@ public class StateValuesDV implements StateValues
 		values.setElement(i, d);
 	}
 
-	/**
-	 * Set the elements of this vector by reading them in from a file.
-	 */
+	@Override
 	public void readFromFile(File file) throws PrismException
 	{
 		BufferedReader in;
@@ -177,50 +197,43 @@ public class StateValuesDV implements StateValues
 		}
 	}
 
-	// round
-
+	@Override
 	public void roundOff(int places)
 	{
 		values.roundOff(places);
 	}
 
-	// subtract all values from 1
-
+	@Override
 	public void subtractFromOne()
 	{
 		values.subtractFromOne();
 	}
 
-	// add another vector to this one
-
+	@Override
 	public void add(StateValues sp)
 	{
 		values.add(((StateValuesDV) sp).values);
 	}
 
-	// multiply vector by a constant
-
+	@Override
 	public void timesConstant(double d)
 	{
 		values.timesConstant(d);
 	}
 
-	// compute dot (inner) product of this and another vector
-	
+	@Override
 	public double dotProduct(StateValues sv)
 	{
 		return values.dotProduct(((StateValuesDV) sv).values);
 	}
 
-	// filter vector using a bdd (set elements not in filter to 0)
-
+	@Override
 	public void filter(JDDNode filter)
 	{
 		values.filter(filter, vars, odd);
 	}
 
-	// apply max operator, i.e. vec[i] = max(vec[i], vec2[i]), where vec2 is an mtbdd
-
+	@Override
 	public void maxMTBDD(JDDNode vec2)
 	{
 		values.maxMTBDD(vec2, vars, odd);
@@ -247,20 +260,19 @@ public class StateValuesDV implements StateValues
 		return values.getElement(i);
 	}
 
-	// get vector
-
+	/** Get the underlying double vector of this StateValuesDV */
 	public DoubleVector getDoubleVector()
 	{
 		return values;
 	}
 
-	// get num non zeros
-
+	@Override
 	public int getNNZ()
 	{
 		return values.getNNZ();
 	}
 
+	@Override
 	public String getNNZString()
 	{
 		return "" + getNNZ();
@@ -268,52 +280,37 @@ public class StateValuesDV implements StateValues
 
 	// Filter operations
 
-	/**
-	 * Get the value of first vector element that is in the (BDD) filter.
-	 */
+	@Override
 	public double firstFromBDD(JDDNode filter)
 	{
 		return values.firstFromBDD(filter, vars, odd);
 	}
 
-	/**
-	 * Get the minimum value of those that are in the (BDD) filter.
-	 */
+	@Override
 	public double minOverBDD(JDDNode filter)
 	{
 		return values.minOverBDD(filter, vars, odd);
 	}
 
-	/**
-	 * Get the minimum value of those that are in the (BDD) filter.
-	 */
+	@Override
 	public double maxOverBDD(JDDNode filter)
 	{
 		return values.maxOverBDD(filter, vars, odd);
 	}
 
-	/**
-	 * Get the sum of those elements that are in the (BDD) filter.
-	 */
+	@Override
 	public double sumOverBDD(JDDNode filter)
 	{
 		return values.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).
-	 */
+	@Override
 	public double sumOverMTBDD(JDDNode mult)
 	{
 		return values.sumOverMTBDD(mult, vars, odd);
 	}
 
-	/**
-	* Sum up the elements of the vector, over a subset of its DD vars
-	* store the result in a new StateValues (for newModel)
-	* @throws PrismException (on out-of-memory)
-	*/
+	@Override
 	public StateValues sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException
 	{
 		DoubleVector tmp;
@@ -323,19 +320,13 @@ public class StateValuesDV implements StateValues
 		return (StateValues) new StateValuesDV(tmp, newModel);
 	}
 
-	/**
-	 * 	Generate BDD for states in the given interval
-	 * (interval specified as relational operator and bound)
-	 */
+	@Override
 	public JDDNode getBDDFromInterval(String relOpString, double bound)
 	{
 		return getBDDFromInterval(RelOp.parseSymbol(relOpString), bound);
 	}
 
-	/**
-	 * 	Generate BDD for states in the given interval
-	 * (interval specified as relational operator and bound)
-	 */
+	@Override
 	public JDDNode getBDDFromInterval(RelOp relOp, double bound)
 	{
 		return values.getBDDFromInterval(relOp, bound, vars, odd);
@@ -350,10 +341,7 @@ public class StateValuesDV implements StateValues
 		return values.getBDDFromInterval(lo, hi, vars, odd);
 	}
 
-	/**
-	 * 	Generate BDD for states whose value is close to 'value'
-	 * (within either absolute or relative error 'epsilon')
-	 */
+	@Override
 	public JDDNode getBDDFromCloseValue(double value, double epsilon, boolean abs)
 	{
 		if (abs)
@@ -362,19 +350,13 @@ public class StateValuesDV implements StateValues
 			return values.getBDDFromCloseValueRel(value, epsilon, vars, odd);
 	}
 
-	/**
-	 * 	Generate BDD for states whose value is close to 'value'
-	 * (within absolute error 'epsilon')
-	 */
+	@Override
 	public JDDNode getBDDFromCloseValueAbs(double value, double epsilon)
 	{
 		return values.getBDDFromCloseValueAbs(value, epsilon, vars, odd);
 	}
 
-	/**
-	 * 	Generate BDD for states whose value is close to 'value'
-	 * (within relative error 'epsilon')
-	 */
+	@Override
 	public JDDNode getBDDFromCloseValueRel(double value, double epsilon)
 	{
 		return values.getBDDFromCloseValueRel(value, epsilon, vars, odd);
@@ -382,34 +364,19 @@ public class StateValuesDV implements StateValues
 
 	// PRINTING STUFF
 
-	/**
-	 * Print vector to a log/file (non-zero entries only)
-	 */
+	@Override
 	public void print(PrismLog log) throws PrismException
 	{
 		print(log, true, false, true, true);
 	}
 
-	/**
-	 * Print vector to a log/file.
-	 * @param log The log
-	 * @param printSparse Print non-zero elements only? 
-	 * @param printMatlab Print in Matlab format?
-	 * @param printStates Print states (variable values) for each element? 
-	 */
+	@Override
 	public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException
 	{
 		print(log, printSparse, printMatlab, printStates, true);
 	}
 
-	/**
-	 * Print vector to a log/file.
-	 * @param log The log
-	 * @param printSparse Print non-zero elements only? 
-	 * @param printMatlab Print in Matlab format?
-	 * @param printStates Print states (variable values) for each element? 
-	 * @param printIndices Print state indices for each element? 
-	 */
+	@Override
 	public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException
 	{
 		int i;
@@ -502,24 +469,13 @@ public class StateValuesDV implements StateValues
 		}
 	}
 
-	/**
-	 * Print part of a vector to a log/file (non-zero entries only).
-	 * @param log The log
-	 * @param filter A BDD specifying which states to print for.
-	 */
+	@Override
 	public void printFiltered(PrismLog log, JDDNode filter) throws PrismException
 	{
 		printFiltered(log, filter, true, false, true, true);
 	}
 
-	/**
-	 * Print part of a vector to a log/file (non-zero entries only).
-	 * @param log The log
-	 * @param filter A BDD specifying which states to print for.
-	 * @param printSparse Print non-zero elements only? 
-	 * @param printMatlab Print in Matlab format?
-	 * @param printStates Print states (variable values) for each element? 
-	 */
+	@Override
 	public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException
 	{
 		printFiltered(log, filter, printSparse, printMatlab, printStates, true);
@@ -532,7 +488,7 @@ public class StateValuesDV implements StateValues
 	 * @param printSparse Print non-zero elements only? 
 	 * @param printMatlab Print in Matlab format?
 	 * @param printStates Print states (variable values) for each element?
-	 * @param printIndices Print state indices for each element? 
+	 * @param printIndizes Print indizes before states? 
 	 */
 	public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices)
 			throws PrismException
@@ -681,9 +637,7 @@ public class StateValuesDV implements StateValues
 		}
 	}
 
-	/**
-	 * Make a (deep) copy of this vector
-	 */
+	@Override
 	public StateValuesDV deepCopy() throws PrismException
 	{
 		// Clone vector

prism/src/prism/StateValuesMTBDD.java

@@ -37,20 +37,27 @@ import parser.VarList;
 import parser.ast.RelOp;
 import parser.type.*;
 
-// Class for state-indexed vectors of (integer or double) values, represented by an MTBDD
-
+/**
+ * Class for state-indexed vectors of (integer or double) values, represented by an MTBDD
+ */
 public class StateValuesMTBDD implements StateValues
 {
-	// MTBDD storing vector of values
+	/** MTBDD storing vector of values */
 	JDDNode values;
 
 	// info from model
+	/** The underlying model */
 	Model model;
+	/** The BDD row variables of the underlying model */
 	JDDVars vars;
 	JDDNode reach;
+	/** The number of BDD row variables in the underlying model */
 	int numDDRowVars;
+	/** The number of BDD row variables in the underlying model */
 	int numVars;
+	/** The ODD for the reachable states of the underlying model */
 	ODDNode odd;
+	/** The VarList of the underlying model*/
 	VarList varList;
 
 	// stuff to keep track of variable values in print method
@@ -59,11 +66,17 @@ public class StateValuesMTBDD implements StateValues
 	int currentVar;
 	int currentVarLevel;
 	
-	// log for output from print method
+	/** log for output from print method */
 	PrismLog outputLog;
 
 	// CONSTRUCTOR
 	
+	/**
+	 * Constructor from a JDDNode (which is stored, not copied).
+	 * <br>[ STORES: values, derefed on later call to clear() ]
+	 * @param values the JddNode for the values
+	 * @param model the underlying model
+	 */
 	public StateValuesMTBDD(JDDNode values, Model model)
 	{
 		int i;
@@ -90,17 +103,19 @@ public class StateValuesMTBDD implements StateValues
 
 	// CONVERSION METHODS
 	
-	// convert to StateValuesDV, destroy (clear) old vector
+	@Override
 	public StateValuesDV convertToStateValuesDV()
 	{
+		// convert to StateValuesDV, destroy (clear) old vector
 		StateValuesDV res = new StateValuesDV(values, model);
 		clear();
 		return res;
 	}
 
-	// convert to StateValuesMTBDD (nothing to do)
+	@Override
 	public StateValuesMTBDD convertToStateValuesMTBDD()
 	{
+		// convert to StateValuesMTBDD (nothing to do)
 		return this;
 	}
 
@@ -135,9 +150,7 @@ public class StateValuesMTBDD implements StateValues
 		values = JDD.ITE(dd, JDD.Constant(d), values);
 	}
 
-	/**
-	 * Set the elements of this vector by reading them in from a file.
-	 */
+	@Override
 	public void readFromFile(File file) throws PrismException
 	{
 		BufferedReader in;
@@ -187,23 +200,20 @@ public class StateValuesMTBDD implements StateValues
 		}
 	}
 
-	// round
-	
+	@Override
 	public void roundOff(int places)
 	{
 		values = JDD.RoundOff(values, places);
 	}
 
-	// subtract all values from 1
-	
+	@Override
 	public void subtractFromOne() 
 	{
 		JDD.Ref(reach);
 		values = JDD.Apply(JDD.MINUS, reach, values);
 	}
 
-	// add another vector to this one
-	
+	@Override
 	public void add(StateValues sp) 
 	{
 		StateValuesMTBDD spm = (StateValuesMTBDD) sp;
@@ -211,15 +221,13 @@ public class StateValuesMTBDD implements StateValues
 		values = JDD.Apply(JDD.PLUS, values, spm.values);
 	}
 
-	// multiply vector by a constant
-	
+	@Override
 	public void timesConstant(double d) 
 	{
 		values = JDD.Apply(JDD.TIMES, values, JDD.Constant(d));
 	}
 
-	// compute dot (inner) product of this and another vector
-	
+	@Override
 	public double dotProduct(StateValues sp) 
 	{
 		StateValuesMTBDD spm = (StateValuesMTBDD) sp;
@@ -232,16 +240,14 @@ public class StateValuesMTBDD implements StateValues
 		return d;
 	}
 
-	// filter vector using a bdd (set elements not in filter to 0)
-	
+	@Override
 	public void filter(JDDNode filter)
 	{
 		JDD.Ref(filter);
 		values = JDD.Apply(JDD.TIMES, values, filter);
 	}
 	
-	// apply max operator, i.e. vec[i] = max(vec[i], vec2[i]), where vec2 is an mtbdd
-	
+	@Override
 	public void maxMTBDD(JDDNode vec2)
 	{
 		JDD.Ref(vec2);
@@ -282,21 +288,26 @@ public class StateValuesMTBDD implements StateValues
 		return dd.getValue();
 	}
 
-	// get mtbdd
-	
+	/**
+	 * Get the underlying JDDNode of this StateValuesMTBDD.
+	 * <br>
+	 * Note: The returned JDDNode is NOT a copy, i.e., the caller
+	 * is responsible that the node does not get derefed.
+	 * <br>[ REFS: <i>none</i> ]
+	 */
 	public JDDNode getJDDNode()
 	{
 		return values;
 	}
 
-	// get num non zeros
-	
+	@Override
 	public int getNNZ()
 	{
 		double nnz = JDD.GetNumMinterms(values, numDDRowVars);
 		return (nnz > Integer.MAX_VALUE) ? -1 : (int)Math.round(nnz);
 	}
 
+	@Override
 	public String getNNZString()
 	{
 		return "" + getNNZ();
@@ -304,9 +315,7 @@ public class StateValuesMTBDD implements StateValues
 
 	// Filter operations
 
-	/**
-	 * Get the value of first vector element that is in the (BDD) filter.
-	 */
+	@Override
 	public double firstFromBDD(JDDNode filter)
 	{
 		JDDNode tmp;
@@ -338,9 +347,7 @@ public class StateValuesMTBDD implements StateValues
 		return d;
 	}
 
-	/**
-	 * Get the minimum value of those that are in the (BDD) filter.
-	 */
+	@Override
 	public double minOverBDD(JDDNode filter)
 	{
 		JDDNode tmp;
@@ -364,8 +371,7 @@ public class StateValuesMTBDD implements StateValues
 		return d;
 	}
 
-	// get max value over BDD filter
-	
+	@Override
 	public double maxOverBDD(JDDNode filter)
 	{
 		JDDNode tmp;
@@ -389,9 +395,7 @@ public class StateValuesMTBDD implements StateValues
 		return d;
 	}
 
-	/**
-	 * Get the sum of those elements that are in the (BDD) filter.
-	 */
+	@Override
 	public double sumOverBDD(JDDNode filter)
 	{
 		JDDNode tmp;
@@ -407,10 +411,7 @@ public class StateValuesMTBDD implements StateValues
 		return d;
 	}
 
-	/**
-	 * Do a weighted sum of the elements of the vector and the values the mtbdd passed in
-	 * (used for CSL reward steady state operator).
-	 */
+	@Override
 	public double sumOverMTBDD(JDDNode mult)
 	{
 		JDDNode tmp;
@@ -426,10 +427,7 @@ public class StateValuesMTBDD implements StateValues
 		return d;
 	}
 
-	/**
-	* Sum up the elements of the vector, over a subset of its DD vars
-	* store the result in a new StateValues (for newModel)
-	*/
+	@Override
 	public StateValues sumOverDDVars(JDDVars sumVars, Model newModel)
 	{
 		JDDNode tmp;
@@ -440,19 +438,13 @@ public class StateValuesMTBDD implements StateValues
 		return new StateValuesMTBDD(tmp, newModel);
 	}
 
-	/**
-	 * 	Generate BDD for states in the given interval
-	 * (interval specified as relational operator and bound)
-	 */
+	@Override
 	public JDDNode getBDDFromInterval(String relOpString, double bound)
 	{
 		return getBDDFromInterval(RelOp.parseSymbol(relOpString), bound);
 	}
 
-	/**
-	 * 	Generate BDD for states in the given interval
-	 * (interval specified as relational operator and bound)
-	 */
+	@Override
 	public JDDNode getBDDFromInterval(RelOp relOp, double bound)
 	{
 		JDDNode sol = null;
@@ -477,10 +469,7 @@ public class StateValuesMTBDD implements StateValues
 		return sol;
 	}
 
-	/**
-	 * 	Generate BDD for states in the given interval
-	 * (interval specified as lower/upper bound)
-	 */
+	@Override
 	public JDDNode getBDDFromInterval(double lo, double hi)
 	{
 		JDDNode sol;
@@ -491,10 +480,7 @@ public class StateValuesMTBDD implements StateValues
 		return sol;
 	}
 
-	/**
-	 * 	Generate BDD for states whose value is close to 'value'
-	 * (within either absolute or relative error 'epsilon')
-	 */
+	@Override
 	public JDDNode getBDDFromCloseValue(double value, double epsilon, boolean abs)
 	{
 		if (abs)
@@ -503,10 +489,7 @@ public class StateValuesMTBDD implements StateValues
 			return getBDDFromCloseValueRel(value, epsilon);
 	}
 
-	/**
-	 * Generate BDD for states whose value is close to 'value'
-	 * (within absolute error 'epsilon')
-	 */
+	@Override
 	public JDDNode getBDDFromCloseValueAbs(double value, double epsilon)
 	{
 		JDDNode sol;
@@ -521,10 +504,7 @@ public class StateValuesMTBDD implements StateValues
 		return sol;
 	}
 
-	/**
-	 * 	Generate BDD for states whose value is close to 'value'
-	 * (within relative error 'epsilon')
-	 */
+	@Override
 	public JDDNode getBDDFromCloseValueRel(double value, double epsilon)
 	{
 		JDDNode sol;
@@ -543,9 +523,7 @@ public class StateValuesMTBDD implements StateValues
 
 	// PRINTING STUFF
 
-	/**
-	 * Print vector to a log/file (non-zero entries only)
-	 */
+	@Override
 	public void print(PrismLog log)
 	{
 		int i;
@@ -588,26 +566,13 @@ public class StateValuesMTBDD implements StateValues
 		}
 	}
 
-	/**
-	 * Print vector to a log/file.
-	 * @param log The log
-	 * @param printSparse Print non-zero elements only? 
-	 * @param printMatlab Print in Matlab format?
-	 * @param printStates Print states (variable values) for each element? 
-	 */
+	@Override
 	public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException
 	{
 		print(log, printSparse, printMatlab, printStates, true);
 	}
 
-	/**
-	 * Print vector to a log/file.
-	 * @param log The log
-	 * @param printSparse Print non-zero elements only? 
-	 * @param printMatlab Print in Matlab format?
-	 * @param printStates Print states (variable values) for each element? 
-	 * @param printIndices Print state indices for each element? 
-	 */
+	@Override
 	public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException
 	{
 		// Because non-sparse output from MTBDD requires a bit more effort...
@@ -680,13 +645,9 @@ public class StateValuesMTBDD implements StateValues
 		varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel));
 	}
 
-	/**
-	 * Print part of a vector to a log/file (non-zero entries only).
-	 * @param log The log
-	 * @param filter A BDD specifying which states to print for.
-	 */
+	@Override
 	public void printFiltered(PrismLog log, JDDNode filter) throws PrismException
-		{
+	{
 		int i;
 		JDDNode tmp;
 		
@@ -714,14 +675,7 @@ public class StateValuesMTBDD implements StateValues
 		JDD.Deref(tmp);
 	}
 
-	/**
-	 * Print part of a vector to a log/file (non-zero entries only).
-	 * @param log The log
-	 * @param filter A BDD specifying which states to print for.
-	 * @param printSparse Print non-zero elements only? 
-	 * @param printMatlab Print in Matlab format?
-	 * @param printStates Print states (variable values) for each element? 
-	 */
+	@Override
 	public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException
 	{
 		// Because non-sparse output from MTBDD requires a bit more effort... 

prism/src/prism/StateValuesVoid.java

@@ -38,8 +38,10 @@ import jdd.JDDVars;
  */
 public class StateValuesVoid implements StateValues
 {
+	/** The stored object */
 	private Object value = null;
 
+	/** Constructor, store value */
 	public StateValuesVoid(Object value)
 	{
 		this.value = value;
@@ -57,61 +59,73 @@ public class StateValuesVoid implements StateValues
 		return value;
 	}
 
+	/** Get the value */
 	public Object getValue()
 	{
 		return value;
 	}
 
+	/** Set the value */
 	public void setValue(Object value)
 	{
 		this.value = value;
 	}
 
+	@Override
 	public StateValuesDV convertToStateValuesDV()
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public StateValuesMTBDD convertToStateValuesMTBDD()
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void readFromFile(File file) throws PrismException
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void roundOff(int places)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void subtractFromOne()
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void add(StateValues sp)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void timesConstant(double d)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public double dotProduct(StateValues sp)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void filter(JDDNode filter)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void maxMTBDD(JDDNode vec2)
 	{
 		throw new UnsupportedOperationException();
@@ -123,101 +137,121 @@ public class StateValuesVoid implements StateValues
 		// Do nothing
 	}
 
+	@Override
 	public int getNNZ()
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public String getNNZString()
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public double firstFromBDD(JDDNode filter)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public double minOverBDD(JDDNode filter)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public double maxOverBDD(JDDNode filter)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public double sumOverBDD(JDDNode filter)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public double sumOverMTBDD(JDDNode mult)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public StateValues sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public JDDNode getBDDFromInterval(String relOpString, double bound)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public JDDNode getBDDFromInterval(RelOp relOp, double bound)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public JDDNode getBDDFromInterval(double lo, double hi)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public JDDNode getBDDFromCloseValue(double val, double epsilon, boolean abs)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public JDDNode getBDDFromCloseValueAbs(double val, double epsilon)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public JDDNode getBDDFromCloseValueRel(double val, double epsilon)
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void print(PrismLog log) throws PrismException
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void printFiltered(PrismLog log, JDDNode filter) throws PrismException
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public void printFiltered(PrismLog log, JDDNode filter, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException
 	{
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
 	public StateValues deepCopy() throws PrismException
 	{
 		throw new UnsupportedOperationException();