Small refactor for reward construction in other model checkers.

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

prism/src/explicit/FastAdaptiveUniformisationModelChecker.java

@@ -220,28 +220,6 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent
 		return new Result(new Double(fau.getValue()));
 	}
 
-	private RewardStruct findRewardStruct(ExpressionReward expr) throws PrismException
-	{
-		RewardStruct rewStruct = null;		
-		Object rs = expr.getRewardStructIndex();
-		if (modulesFile == null)
-			throw new PrismException("No model file to obtain reward structures");
-		if (modulesFile.getNumRewardStructs() == 0)
-			throw new PrismException("Model has no rewards specified");
-		if (rs == null) {
-			rewStruct = modulesFile.getRewardStruct(0);
-		} else if (rs instanceof Expression) {
-			int i = ((Expression) rs).evaluateInt(constantValues);
-			rs = new Integer(i); // for better error reporting below
-			rewStruct = modulesFile.getRewardStruct(i - 1);
-		} else if (rs instanceof String) {
-			rewStruct = modulesFile.getRewardStructByName((String) rs);
-		}
-		if (rewStruct == null)
-			throw new PrismException("Invalid reward structure index \"" + rs + "\"");
-		return rewStruct;
-	}
-
 	/**
 	 * Model check an R operator.
 	 */
@@ -262,7 +240,7 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent
 			throw new PrismException("Currently only instantaneous or cumulative rewards are allowed.");
 		}
 		double time = temporal.getUpperBound().evaluateDouble(constantValues);
-		RewardStruct rewStruct = findRewardStruct(expr);
+		RewardStruct rewStruct = expr.getRewardStructByIndexObject(modulesFile, constantValues);
 		fau.setRewardStruct(rewStruct);
 		fau.setConstantValues(constantValues);
 		fau.computeTransientProbsAdaptive(time);

prism/src/param/ParamModelChecker.java

@@ -957,18 +957,13 @@ final public class ParamModelChecker extends PrismComponent
 	 */
 	protected RegionValues checkExpressionReward(ParamModel model, ExpressionReward expr, BitSet needStates) throws PrismException
 	{
-		Object rs; // Reward struct index
-		RewardStruct rewStruct = null; // Reward struct object
 		Expression rb; // Reward bound (expression)
 		BigRational r = null; // Reward bound (actual value)
-		//String relOp; // Relational operator
-		ModelType modelType = model.getModelType();
 		RegionValues rews = null;
-		int i;
 		boolean min = false;
 
 		// Get info from reward operator
-		rs = expr.getRewardStructIndex();
+		RewardStruct rewStruct = expr.getRewardStructByIndexObject(modulesFile, constantValues);
 		RelOp relOp = expr.getRelOp();
 		rb = expr.getReward();
 		if (rb != null) {
@@ -979,24 +974,6 @@ final public class ParamModelChecker extends PrismComponent
 		}
 		min = relOp.isLowerBound() || relOp.isMin();
 
-		// Get reward info
-		if (modulesFile == null)
-			throw new PrismException("No model file to obtain reward structures");
-		if (modulesFile.getNumRewardStructs() == 0)
-			throw new PrismException("Model has no rewards specified");
-		if (rs == null) {
-			rewStruct = modulesFile.getRewardStruct(0);
-		} else if (rs instanceof Expression) {
-			i = ((Expression) rs).evaluateInt(constantValues);
-			rs = new Integer(i); // for better error reporting below
-			rewStruct = modulesFile.getRewardStruct(i - 1);
-		} else if (rs instanceof String) {
-			rewStruct = modulesFile.getRewardStructByName((String) rs);
-		}
-		if (rewStruct == null)
-			throw new PrismException("Invalid reward structure index \"" + rs + "\"");
-
-		
 		ParamRewardStruct rew = constructRewards(model, rewStruct, constantValues);
 		mainLog.println("Building reward structure...");
 		rews = checkRewardFormula(model, rew, expr.getExpression(), min, needStates);