Handle bounded P/R operators in explicit engine.

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

prism/src/explicit/ProbModelChecker.java

@@ -27,12 +27,17 @@
 package explicit;
 
 import java.util.BitSet;
-import java.util.List;
 
-import explicit.rewards.*;
-import parser.State;
-import parser.ast.*;
-import prism.*;
+import parser.ast.Expression;
+import parser.ast.ExpressionProb;
+import parser.ast.ExpressionReward;
+import parser.ast.ExpressionSS;
+import parser.ast.RewardStruct;
+import prism.ModelType;
+import prism.PrismException;
+import explicit.rewards.ConstructRewards;
+import explicit.rewards.MCRewards;
+import explicit.rewards.MDPRewards;
 
 /**
  * Super class for explicit-state probabilistic model checkers
@@ -69,8 +74,10 @@ public class ProbModelChecker extends StateModelChecker
 	/**
 	 * Model check a P operator expression and return the values for all states.
 	 */
-	protected StateValues checkExpressionProb(Model model, ExpressionProb expr) throws PrismException
+	protected Object checkExpressionProb(Model model, ExpressionProb expr) throws PrismException
 	{
+		Expression pb; // Probability bound (expression)
+		double p = 0; // Probability bound (actual value)
 		String relOp; // Relational operator
 		boolean min = false; // For nondeterministic models, are we finding min (true) or max (false) probs
 		ModelType modelType = model.getModelType();
@@ -79,10 +86,12 @@ public class ProbModelChecker extends StateModelChecker
 
 		// Get info from prob operator
 		relOp = expr.getRelOp();
-
-		// Check for unhandled cases
-		if (expr.getProb() != null)
-			throw new PrismException("Explicit engine does not yet handle bounded P operators");
+		pb = expr.getProb();
+		if (pb != null) {
+			p = pb.evaluateDouble(constantValues);
+			if (p < 0 || p > 1)
+				throw new PrismException("Invalid probability bound " + p + " in P operator");
+		}
 
 		// For nondeterministic models, determine whether min or max probabilities needed
 		if (modelType.nondeterministic()) {
@@ -125,20 +134,27 @@ public class ProbModelChecker extends StateModelChecker
 		}
 
 		// For =? properties, just return values
-		return probs;
+		if (pb == null) {
+			return probs;
+		}
+		// Otherwise, compare against bound to get set of satisfying states
+		else {
+			BitSet sol = probs.getBitSetFromInterval(relOp, p);
+			probs.clear();
+			return sol;
+		}
 	}
 	
 	/**
 	 * Model check an R operator expression and return the values for all states.
 	 */
-	protected StateValues checkExpressionReward(Model model, ExpressionReward expr) throws PrismException
+	protected Object checkExpressionReward(Model model, ExpressionReward expr) throws PrismException
 	{
 		Object rs; // Reward struct index
 		RewardStruct rewStruct = null; // Reward struct object
 		Expression rb; // Reward bound (expression)
 		double r = 0; // Reward bound (actual value)
 		String relOp; // Relational operator
-		Expression expr2; // expression
 		boolean min = false; // For nondeterministic models, are we finding min (true) or max (false) rewards
 		ModelType modelType = model.getModelType();
 		StateValues rews = null;
@@ -156,11 +172,6 @@ public class ProbModelChecker extends StateModelChecker
 				throw new PrismException("Invalid reward bound " + r + " in R[] formula");
 		}
 
-		// Check for unhandled cases
-		if (expr.getReward() != null)
-			throw new PrismException("Explicit engine does not yet handle bounded R operators");
-		// More? TODO
-
 		// For nondeterministic models, determine whether min or max rewards needed
 		if (modelType.nondeterministic()) {
 			if (relOp.equals(">") || relOp.equals(">=") || relOp.equals("min=")) {
@@ -228,6 +239,14 @@ public class ProbModelChecker extends StateModelChecker
 		}
 
 		// For =? properties, just return values
-		return rews;
+		if (rb == null) {
+			return rews;
+		}
+		// Otherwise, compare against bound to get set of satisfying states
+		else {
+			BitSet sol = rews.getBitSetFromInterval(relOp, r);
+			rews.clear();
+			return sol;
+		}
 	}
 }

prism/src/explicit/StateValues.java

@@ -26,11 +26,11 @@
 
 package explicit;
 
-import java.util.*;
+import java.util.BitSet;
 
-import dv.DoubleVector;
-
-import parser.type.*;
+import parser.type.Type;
+import parser.type.TypeDouble;
+import parser.type.TypeInt;
 import prism.PrismException;
 import prism.PrismLog;
 
@@ -46,9 +46,9 @@ public class StateValues
 	// Vector (only one used, depending on type)
 	protected int[] valuesI;
 	protected double[] valuesD;
-	
+
 	// CONSTRUCTORS, etc.
-	
+
 	/**
 	 * Construct a new empty state values vector of unspecified type.
 	 * (Mostly for internal use.)
@@ -60,7 +60,7 @@ public class StateValues
 		valuesI = null;
 		valuesD = null;
 	}
-	
+
 	/**
 	 * Construct a new state values vector of the given type and size.
 	 * All values are initially set to zero.
@@ -70,7 +70,7 @@ public class StateValues
 		// TODO: check this: ? probably always returns Double due to typing
 		this(type, size, type instanceof TypeInt ? new Integer(0) : new Double(0.0));
 	}
-	
+
 	/**
 	 * Construct a new state values vector of the given type and size,
 	 * initialising all values to 'init'.
@@ -89,17 +89,17 @@ public class StateValues
 		// Create/initialise array of appropriate type
 		if (type instanceof TypeInt) {
 			valuesI = new int[size];
-			initI = ((Integer)init).intValue();
+			initI = ((Integer) init).intValue();
 			for (i = 0; i < size; i++)
 				valuesI[i] = initI;
 		} else if (type instanceof TypeDouble) {
 			valuesD = new double[size];
-			initD = ((Double)init).doubleValue();
+			initD = ((Double) init).doubleValue();
 			for (i = 0; i < size; i++)
 				valuesD[i] = initD;
 		}
 	}
-	
+
 	/**
 	 * Create a new (double-valued) state values vector from an existing array of doubles.
 	 * The array is stored directly, not copied.
@@ -128,9 +128,9 @@ public class StateValues
 		}
 		return createFromDoubleArray(array);
 	}
-		
+
 	// CONVERSION METHODS
-	
+
 	/*// convert to StateValuesDV (nothing to do)
 	public StateValuesDV convertToStateValuesDV()
 	{
@@ -144,23 +144,72 @@ public class StateValues
 		clear();
 		return res;
 	}*/
-	
+
+	/**
+	 * Generate BitSet for states in the given interval
+	 * (interval specified as relational operator and bound)
+	 */
+	public BitSet getBitSetFromInterval(String relOp, double bound)
+	{
+		BitSet sol = new BitSet();
+
+		if (type instanceof TypeInt) {
+			if (relOp.equals(">=")) {
+				for (int i = 0; i < size; i++) {
+					sol.set(i, valuesI[i] >= bound);
+				}
+			} else if (relOp.equals(">")) {
+				for (int i = 0; i < size; i++) {
+					sol.set(i, valuesI[i] > bound);
+				}
+			} else if (relOp.equals("<=")) {
+				for (int i = 0; i < size; i++) {
+					sol.set(i, valuesI[i] <= bound);
+				}
+			} else if (relOp.equals("<")) {
+				for (int i = 0; i < size; i++) {
+					sol.set(i, valuesI[i] < bound);
+				}
+			}
+		} else if (type instanceof TypeDouble) {
+			if (relOp.equals(">=")) {
+				for (int i = 0; i < size; i++) {
+					sol.set(i, valuesD[i] >= bound);
+				}
+			} else if (relOp.equals(">")) {
+				for (int i = 0; i < size; i++) {
+					sol.set(i, valuesD[i] > bound);
+				}
+			} else if (relOp.equals("<=")) {
+				for (int i = 0; i < size; i++) {
+					sol.set(i, valuesD[i] <= bound);
+				}
+			} else if (relOp.equals("<")) {
+				for (int i = 0; i < size; i++) {
+					sol.set(i, valuesD[i] < bound);
+				}
+			}
+		}
+
+		return sol;
+	}
+
 	// METHODS TO MODIFY VECTOR
-	
+
 	public void setIntValue(int i, int val)
 	{
 		valuesI[i] = val;
 	}
-	
+
 	public void setDoubleValue(int i, double val)
 	{
 		valuesD[i] = val;
 	}
-	
+
 	// ...
-	
+
 	// clear (free memory)
-	
+
 	/**
 	 * Clear the vector, i.e. free any used memory.
 	 * (Well, actually, just set pointer to null and wait for later garbage collection.)
@@ -172,7 +221,7 @@ public class StateValues
 	}
 
 	// METHODS TO ACCESS VECTOR DATA
-	
+
 	/**
 	 * Get the value of the ith element of the vector, as an Object.
 	 */
@@ -186,7 +235,7 @@ public class StateValues
 			return null;
 		}
 	}
-	
+
 	/*
 	// get num non zeros
 	
@@ -200,9 +249,9 @@ public class StateValues
 		return "" + getNNZ();
 	}
 	*/
-	
+
 	// PRINTING STUFF
-	
+
 	/**
 	 * Print vector to a log/file (non-zero entries only)
 	 */
@@ -213,12 +262,12 @@ public class StateValues
 			log.println(getValue(i));
 		}
 	}
-	
+
 	public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates) throws PrismException
 	{
 		print(log); //TODO
 	}
-	
+
 	/**
 	 * Make a (deep) copy of this vector
 	 */