diff --git a/prism/src/prism/StateValues.java b/prism/src/prism/StateValues.java index 717f160a..299ce131 100644 --- a/prism/src/prism/StateValues.java +++ b/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. + *
+ * 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. + *
+ * 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). + *
[ DEREFS: none ] + */ void filter(JDDNode filter); + + /** + * Apply max operator, i.e. vec[i] = max(vec[i], vec2[i]), where vec2 is an MTBDD + *
[ DEREFS: none ] + */ 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. + *
+ * Should be called with a non-empty filter. For an empty filter, will return + * {@code Double.NaN}. + *
[ DEREFS: none ] + */ double firstFromBDD(JDDNode filter); + + /** + * Get the minimum value of those that are in the (BDD) filter. + *
+ * If the filter is empty for this vector, returns positive infinity. + *
[ DEREFS: none ] + */ double minOverBDD(JDDNode filter); + + /** + * Get the maximum value of those that are in the (BDD) filter. + *
+ * If the filter is empty for this vector, returns negative infinity. + *
[ DEREFS: none ] + */ 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. + *
[ DEREFS: none ] + */ 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). + *
[ DEREFS: none ] + */ 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) + *
[ REFS: result ] + */ JDDNode getBDDFromInterval(String relOpString, double bound); + + /** + * Generate BDD for states in the given interval + * (interval specified as relational operator and bound) + *
[ REFS: result ] + */ JDDNode getBDDFromInterval(RelOp relOp, double bound); + + /** + * Generate BDD for states in the given interval + * (interval specified as inclusive lower/upper bound) + *
[ REFS: result ] + */ JDDNode getBDDFromInterval(double lo, double hi); + + /** + * Generate BDD for states whose value is close to 'value' + * (within either absolute or relative error 'epsilon') + *
[ REFS: result ] + * @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') + *
[ REFS: result ] + * @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') + *
[ REFS: result ] + * @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). + *
[ DEREFS: none ] + * @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). + *
[ DEREFS: none ] + * @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; } diff --git a/prism/src/prism/StateValuesDV.java b/prism/src/prism/StateValuesDV.java index 085bb1d9..e625ef3e 100644 --- a/prism/src/prism/StateValuesDV.java +++ b/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. + *
+ * Note: The JDDNode dd must only be non-zero for reachable states + * (otherwise bad things happen) + *
[ DEREFS: none ] + * @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); @@ -246,21 +259,20 @@ public class StateValuesDV implements StateValues // TODO: cast to Integer or Double as required? 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); @@ -531,8 +487,8 @@ public class StateValuesDV implements StateValues * @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? - * @param printIndices Print state indices for each element? + * @param printStates Print states (variable values) 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 diff --git a/prism/src/prism/StateValuesMTBDD.java b/prism/src/prism/StateValuesMTBDD.java index 26dd0a97..3bfd2211 100644 --- a/prism/src/prism/StateValuesMTBDD.java +++ b/prism/src/prism/StateValuesMTBDD.java @@ -37,33 +37,46 @@ 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 int[] varSizes; int[] varValues; 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). + *
[ 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,22 +103,24 @@ 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; } - + // METHODS TO MODIFY VECTOR - + /** * Set element i of this vector to value d. */ @@ -134,10 +149,8 @@ public class StateValuesMTBDD implements StateValues // Add element to vector MTBDD 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; @@ -186,40 +199,35 @@ public class StateValuesMTBDD implements StateValues throw new PrismException("Error detected at line " + lineNum + " of file \"" + file + "\""); } } - - // 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; JDD.Ref(spm.values); 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; @@ -231,17 +239,15 @@ public class StateValuesMTBDD implements StateValues JDD.Deref(tmp); 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); @@ -261,7 +267,7 @@ public class StateValuesMTBDD implements StateValues { return (int) model.getNumStates(); } - + @Override public Object getValue(int i) { @@ -281,32 +287,35 @@ public class StateValuesMTBDD implements StateValues // TODO: cast to Integer or Double as required? return dd.getValue(); } - - // get mtbdd - + + /** + * Get the underlying JDDNode of this StateValuesMTBDD. + *
+ * Note: The returned JDDNode is NOT a copy, i.e., the caller + * is responsible that the node does not get derefed. + *
[ REFS: none ] + */ 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(); } - + // Filter operations - - /** - * Get the value of first vector element that is in the (BDD) filter. - */ + + @Override public double firstFromBDD(JDDNode filter) { JDDNode tmp; @@ -337,10 +346,8 @@ 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; @@ -363,9 +370,8 @@ public class StateValuesMTBDD implements StateValues return d; } - - // get max value over BDD filter - + + @Override public double maxOverBDD(JDDNode filter) { JDDNode tmp; @@ -388,10 +394,8 @@ 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; @@ -406,11 +410,8 @@ 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; @@ -425,11 +426,8 @@ 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; @@ -439,20 +437,14 @@ 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; @@ -476,11 +468,8 @@ 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) @@ -502,11 +488,8 @@ public class StateValuesMTBDD implements StateValues else 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; @@ -520,11 +503,8 @@ 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; @@ -540,12 +520,10 @@ public class StateValuesMTBDD implements StateValues return sol; } - + // 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... @@ -615,7 +580,7 @@ public class StateValuesMTBDD implements StateValues else throw new PrismException("Not supported"); // Note we also ignore printMatlab/printStates/printIndices due to laziness } - + /** * Recursive part of print method. * @@ -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; @@ -713,15 +674,8 @@ public class StateValuesMTBDD implements StateValues //log.println(); 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... diff --git a/prism/src/prism/StateValuesVoid.java b/prism/src/prism/StateValuesVoid.java index 29758ba3..19644324 100644 --- a/prism/src/prism/StateValuesVoid.java +++ b/prism/src/prism/StateValuesVoid.java @@ -38,13 +38,15 @@ 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; } - + @Override public int getSize() { @@ -57,167 +59,199 @@ 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(); } - + @Override public void clear() { // 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();