Refactoring of extraction of rewards in symbolic model checking engine.

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

prism/src/prism/NondetModelChecker.java

@@ -200,34 +200,17 @@ public class NondetModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkExpressionReward(ExpressionReward expr) throws PrismException
 	{
-		StateValues rewards = null;
-		int i;
-
 		// Get info from R operator
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
 		MinMax minMax = opInfo.getMinMax(model.getModelType());
 
-		// Get reward info
-		JDDNode stateRewards = null, transRewards = null, sol;
+		// Get rewards
 		Object rs = expr.getRewardStructIndex();
-		if (model.getNumRewardStructs() == 0)
-			throw new PrismException("Model has no rewards specified");
-		if (rs == null) {
-			stateRewards = model.getStateRewards(0);
-			transRewards = model.getTransRewards(0);
-		} else if (rs instanceof Expression) {
-			i = ((Expression) rs).evaluateInt(constantValues);
-			rs = new Integer(i); // for better error reporting below
-			stateRewards = model.getStateRewards(i - 1);
-			transRewards = model.getTransRewards(i - 1);
-		} else if (rs instanceof String) {
-			stateRewards = model.getStateRewards((String) rs);
-			transRewards = model.getTransRewards((String) rs);
-		}
-		if (stateRewards == null || transRewards == null)
-			throw new PrismException("Invalid reward structure index \"" + rs + "\"");
+		JDDNode stateRewards = getStateRewardsByIndexObject(rs, model, constantValues);
+		JDDNode transRewards = getTransitionRewardsByIndexObject(rs, model, constantValues);
 
 		// Compute rewards
+		StateValues rewards = null;
 		Expression expr2 = expr.getExpression();
 		if (expr2 instanceof ExpressionTemporal) {
 			switch (((ExpressionTemporal) expr2).getOperator()) {
@@ -257,7 +240,7 @@ public class NondetModelChecker extends NonProbModelChecker
 		}
 		// Otherwise, compare against bound to get set of satisfying states
 		else {
-			sol = rewards.getBDDFromInterval(opInfo.getRelOp(), opInfo.getBound());
+			JDDNode sol = rewards.getBDDFromInterval(opInfo.getRelOp(), opInfo.getBound());
 			// remove unreachable states from solution
 			JDD.Ref(reach);
 			sol = JDD.And(sol, reach);

prism/src/prism/ProbModelChecker.java

@@ -38,6 +38,7 @@ import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
 import mtbdd.PrismMTBDD;
+import parser.Values;
 import parser.ast.Expression;
 import parser.ast.ExpressionProb;
 import parser.ast.ExpressionReward;
@@ -202,25 +203,10 @@ public class ProbModelChecker extends NonProbModelChecker
 		// Get info from R operator
 		OpRelOpBound opInfo = expr.getRelopBoundInfo(constantValues);
 		
-		// Get reward info
-		JDDNode stateRewards = null, transRewards = null;
+		// Get rewards
 		Object rs = expr.getRewardStructIndex();
-		if (model.getNumRewardStructs() == 0)
-			throw new PrismException("Model has no rewards specified");
-		if (rs == null) {
-			stateRewards = model.getStateRewards(0);
-			transRewards = model.getTransRewards(0);
-		} else if (rs instanceof Expression) {
-			int i = ((Expression) rs).evaluateInt(constantValues);
-			rs = new Integer(i); // for better error reporting below
-			stateRewards = model.getStateRewards(i - 1);
-			transRewards = model.getTransRewards(i - 1);
-		} else if (rs instanceof String) {
-			stateRewards = model.getStateRewards((String) rs);
-			transRewards = model.getTransRewards((String) rs);
-		}
-		if (stateRewards == null || transRewards == null)
-			throw new PrismException("Invalid reward structure index \"" + rs + "\"");
+		JDDNode stateRewards = getStateRewardsByIndexObject(rs, model, constantValues);
+		JDDNode transRewards = getTransitionRewardsByIndexObject(rs, model, constantValues);
 
 		// Print a warning if Rmin/Rmax used
 		if (opInfo.getRelOp() == RelOp.MIN || opInfo.getRelOp() == RelOp.MAX) {

prism/src/prism/StateModelChecker.java

@@ -1344,6 +1344,54 @@ public class StateModelChecker implements ModelChecker
 
 		return resVals;
 	}
+
+	// Utility functions for symbolic model checkers 
+	
+	/**
+	 * Get the state rewards (from a model) corresponding to the index of this R operator.
+	 * Throws an exception (with explanatory message) if it cannot be found.
+	 */
+	public JDDNode getStateRewardsByIndexObject(Object rs, Model model, Values constantValues) throws PrismException
+	{
+		JDDNode stateRewards = null;
+		if (model.getNumRewardStructs() == 0)
+			throw new PrismException("Model has no rewards specified");
+		if (rs == null) {
+			stateRewards = model.getStateRewards(0);
+		} else if (rs instanceof Expression) {
+			int i = ((Expression) rs).evaluateInt(constantValues);
+			rs = new Integer(i); // for better error reporting below
+			stateRewards = model.getStateRewards(i - 1);
+		} else if (rs instanceof String) {
+			stateRewards = model.getStateRewards((String) rs);
+		}
+		if (stateRewards == null)
+			throw new PrismException("Invalid reward structure index \"" + rs + "\"");
+		return stateRewards; 
+	}
+	
+	/**
+	 * Get the transition rewards (from a model) corresponding to the index of this R operator.
+	 * Throws an exception (with explanatory message) if it cannot be found.
+	 */
+	public JDDNode getTransitionRewardsByIndexObject(Object rs, Model model, Values constantValues) throws PrismException
+	{
+		JDDNode transRewards = null;
+		if (model.getNumRewardStructs() == 0)
+			throw new PrismException("Model has no rewards specified");
+		if (rs == null) {
+			transRewards = model.getTransRewards(0);
+		} else if (rs instanceof Expression) {
+			int i = ((Expression) rs).evaluateInt(constantValues);
+			rs = new Integer(i); // for better error reporting below
+			transRewards = model.getTransRewards(i - 1);
+		} else if (rs instanceof String) {
+			transRewards = model.getTransRewards((String) rs);
+		}
+		if (transRewards == null)
+			throw new PrismException("Invalid reward structure index \"" + rs + "\"");
+		return transRewards; 
+	}
 }
 
 // ------------------------------------------------------------------------------