diff --git a/prism/src/explicit/StateValues.java b/prism/src/explicit/StateValues.java index 0b5eba4b..421ab5d7 100644 --- a/prism/src/explicit/StateValues.java +++ b/prism/src/explicit/StateValues.java @@ -48,6 +48,7 @@ import prism.PrismException; import prism.PrismLangException; import prism.PrismLog; import prism.PrismUtils; +import prism.ResultTesting; import prism.StateVector; /** @@ -320,24 +321,46 @@ public class StateValues implements StateVector return sol; } + /** + * Generate BitSet for states whose value is close to 'value' + * (if present, accuracy info used to determine closeness) + * The type of 'value' is assumed to match that of the vector. + */ + public BitSet getBitSetFromCloseValue(Object value) throws PrismException + { + Accuracy accuracy = ResultTesting.getTestingAccuracy(getAccuracy()); + return getBitSetFromCloseValue(value, accuracy); + } + /** * Generate BitSet for states whose value is close to 'value' * (within either absolute or relative error 'epsilon') * The type of 'value' is assumed to match that of the vector. */ public BitSet getBitSetFromCloseValue(Object value, double epsilon, boolean abs) throws PrismException + { + Accuracy accuracy = new Accuracy(Accuracy.AccuracyLevel.BOUNDED, epsilon, abs); + return getBitSetFromCloseValue(value, accuracy); + } + + /** + * Generate BitSet for states whose value is close to 'value' + * (use the passed in level of accuracy to determine closeness) + * The type of 'value' is assumed to match that of the vector. + */ + public BitSet getBitSetFromCloseValue(Object value, Accuracy accuracy) throws PrismException { BitSet sol = new BitSet(); if (type instanceof TypeInt) { int valueI = ((Integer) value).intValue(); for (int i = 0; i < size; i++) { - sol.set(i, PrismUtils.doublesAreClose(valuesI[i], valueI, epsilon, abs)); + sol.set(i, PrismUtils.measureSupNormAbs(valuesI[i], valueI) <= accuracy.getAbsoluteErrorBound(valuesI[i])); } } else if (type instanceof TypeDouble) { double valueD = ((Double) value).doubleValue(); for (int i = 0; i < size; i++) { - sol.set(i, PrismUtils.doublesAreClose(valuesD[i], valueD, epsilon, abs)); + sol.set(i, PrismUtils.measureSupNormAbs(valuesD[i], valueD) <= accuracy.getAbsoluteErrorBound(valuesD[i])); } } else { throw new PrismException("Can't getBitSetFromCloseValue for a vector of type " + type); diff --git a/prism/src/prism/StateValues.java b/prism/src/prism/StateValues.java index 5f016ed3..cc5b2fbf 100644 --- a/prism/src/prism/StateValues.java +++ b/prism/src/prism/StateValues.java @@ -31,6 +31,7 @@ import java.io.File; import jdd.JDDNode; import jdd.JDDVars; import parser.ast.RelOp; +import prism.Accuracy.AccuracyType; /** * Interface for classes for state-indexed vectors of (integer or double) values @@ -195,6 +196,20 @@ public interface StateValues extends StateVector */ JDDNode getBDDFromInterval(double lo, double hi); + /** + * Generate BDD for states whose value is close to 'value' + * (if present, accuracy info used to determine closeness) + *
[ REFS: result ] + * @param val the value + * @param epsilon the error bound + * @param abs true for absolute error calculation + */ + default JDDNode getBDDFromCloseValue(double val) + { + Accuracy accuracy = ResultTesting.getTestingAccuracy(getAccuracy()); + return getBDDFromCloseValue(val, accuracy.getErrorBound(), accuracy.getType() == AccuracyType.ABSOLUTE); + } + /** * Generate BDD for states whose value is close to 'value' * (within either absolute or relative error 'epsilon')