More filters in explicit engine.

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

prism/src/explicit/StateModelChecker.java

@@ -595,36 +595,32 @@ public class StateModelChecker
 			resVals = vals;
 			// Set vals to null to stop it being cleared below
 			vals = null;
-			break;
+			break;*/
 		case MIN:
 			// Compute min
-			d = vals.minOverBDD(bsFilter);
-			// Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion)
-			resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d));
-			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			// Store as object/vector
+			resObj = vals.minOverBitSet(bsFilter);
+			resVals = new StateValues(expr.getType(), model.getNumStates(), resObj); 
 			// Create explanation of result and print some details to log
 			resultExpl = "Minimum value over " + filterStatesString;
 			mainLog.println("\n" + resultExpl + ": " + resObj);
 			// Also find states that (are close to) selected value for display to log
-			ddMatch = vals.getBDDFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE);
-			JDD.Ref(bsFilter);
-			ddMatch = JDD.And(ddMatch, bsFilter);
+			bsMatch = vals.getBitSetFromCloseValue(resObj, termCritParam, termCrit == TermCrit.ABSOLUTE);
+			bsMatch.and(bsFilter);
 			break;
 		case MAX:
 			// Compute max
-			d = vals.maxOverBDD(bsFilter);
-			// Store as object/vector (note crazy Object cast to avoid Integer->int auto conversion)
-			resObj = (expr.getType() instanceof TypeInt) ? ((Object) new Integer((int) d)) : (new Double(d));
-			resVals = new StateValuesMTBDD(JDD.Constant(d), model);
+			// Store as object/vector
+			resObj = vals.maxOverBitSet(bsFilter);
+			resVals = new StateValues(expr.getType(), model.getNumStates(), resObj); 
 			// Create explanation of result and print some details to log
 			resultExpl = "Maximum value over " + filterStatesString;
 			mainLog.println("\n" + resultExpl + ": " + resObj);
 			// Also find states that (are close to) selected value for display to log
-			bsMatch = vals.getBitSetFromCloseValue(d, prism.getTermCritParam(), prism.getTermCrit() == Prism.ABSOLUTE);
-			JDD.Ref(bsFilter);
-			bsMatch = JDD.And(bsMatch, bsFilter);
+			bsMatch = vals.getBitSetFromCloseValue(resObj, termCritParam, termCrit == TermCrit.ABSOLUTE);
+			bsMatch.and(bsFilter);
 			break;
-		case ARGMIN:
+		/*case ARGMIN:
 			// Compute/display min
 			d = vals.minOverBDD(bsFilter);
 			mainLog.print("\nMinimum value over " + filterStatesString + ": ");

prism/src/explicit/StateValues.java

@@ -40,6 +40,7 @@ import prism.PrismException;
 import prism.PrismFileLog;
 import prism.PrismLangException;
 import prism.PrismLog;
+import prism.PrismUtils;
 
 /**
  * Class for explicit-state storage of a state-indexed vector of (integer or double) values.
@@ -226,6 +227,30 @@ public class StateValues
 		return sol;
 	}
 
+	/**
+	 * 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)
+	{
+		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));
+			}
+		} 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));
+			}
+		}
+		
+		return sol;
+	}
+	
 	// METHODS TO MODIFY VECTOR
 
 	public void setIntValue(int i, int val)