ExpressionReward: provide static variants of getRewardStructByIndexObject and getRewardStructIndexByIndexObject

Allows resolving of reward structure index objects when they occur outside of R operators.


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

prism/src/parser/ast/ExpressionReward.java

@@ -113,9 +113,19 @@ public class ExpressionReward extends ExpressionQuant
 	 * This means that, the method always returns a valid index if it finishes.
 	 */
 	public int getRewardStructIndexByIndexObject(ModelInfo modelInfo, Values constantValues) throws PrismException
+	{
+		return getRewardStructIndexByIndexObject(rewardStructIndex, modelInfo, constantValues);
+	}
+
+	/**
+	 * Get the index of a reward structure (within a model) corresponding to the rsi reward structure index object.
+	 * This is 0-indexed (as used e.g. in ModulesFile), not 1-indexed (as seen by user)
+	 * Throws an exception (with explanatory message) if it cannot be found.
+	 * This means that, the method always returns a valid index if it finishes.
+	 */
+	public static int getRewardStructIndexByIndexObject(Object rsi, ModelInfo modelInfo, Values constantValues) throws PrismException
 	{
 		int rewStruct = -1;
-		Object rsi = rewardStructIndex;
 		// Recall: the index is an Object which is either an Integer, denoting the index (starting from 0) directly,
 		// or an expression, which can be evaluated (possibly using the passed in constants) to an index. 
 		if (modelInfo == null)
@@ -127,8 +137,8 @@ public class ExpressionReward extends ExpressionQuant
 			rewStruct = 0;
 		}
 		// Expression - evaluate to an index
-		else if (rewardStructIndex instanceof Expression) {
-			int i = ((Expression) rewardStructIndex).evaluateInt(constantValues);
+		else if (rsi instanceof Expression) {
+			int i = ((Expression) rsi).evaluateInt(constantValues);
 			rsi = new Integer(i); // (for better error reporting below)
 			rewStruct = i - 1;
 		}
@@ -141,7 +151,7 @@ public class ExpressionReward extends ExpressionQuant
 		}
 		return rewStruct;
 	}
-	
+
 	/**
 	 * Get the reward structure (from a model) corresponding to the index of this R operator.
 	 * Throws an exception (with explanatory message) if it cannot be found.
@@ -151,6 +161,17 @@ public class ExpressionReward extends ExpressionQuant
 		int rewardStructIndex = getRewardStructIndexByIndexObject(modelInfo, constantValues);
 		return modelInfo.getRewardStruct(rewardStructIndex);
 	}
+
+	/**
+	 * Get the reward structure (from a model) corresponding to a reward structure index object.
+	 * Throws an exception (with explanatory message) if it cannot be found.
+	 */
+	public static RewardStruct getRewardStructByIndexObject(Object rsi, ModelInfo modelInfo, Values constantValues) throws PrismException
+	{
+		int rewardStructIndex = getRewardStructIndexByIndexObject(rsi, modelInfo, constantValues);
+		return modelInfo.getRewardStruct(rewardStructIndex);
+	}
+
 	
 	/**
 	 * Get info about the operator and bound.