Explicit engine reward construction handles model constants properly.

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

prism/src/explicit/ProbModelChecker.java

@@ -245,7 +245,7 @@ public class ProbModelChecker extends StateModelChecker
 			}
 			// Special case: constant rewards
 			if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) {
-				return new MCRewardsStateConstant(rewStr.getReward(0).evaluateDouble());
+				return new MCRewardsStateConstant(rewStr.getReward(0).evaluateDouble(constantValues));
 			}
 			// Normal: state rewards
 			else {
@@ -256,8 +256,8 @@ public class ProbModelChecker extends StateModelChecker
 				for (i = 0; i < n; i++) {
 					guard = rewStr.getStates(i);
 					for (j = 0; j < numStates; j++) {
-						if (guard.evaluateBoolean(statesList.get(j))) {
-							rewSA.setStateReward(j, rewStr.getReward(i).evaluateDouble(statesList.get(j)));
+						if (guard.evaluateBoolean(constantValues, statesList.get(j))) {
+							rewSA.setStateReward(j, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
 						}
 					}
 				}
@@ -284,7 +284,7 @@ public class ProbModelChecker extends StateModelChecker
 		// Special case: constant rewards
 		// TODO
 		/*if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) {
-			return new MCRewardsStateConstant(rewStr.getReward(0).evaluateDouble());
+			return new MCRewardsStateConstant(rewStr.getReward(0).evaluateDouble(constantValues));
 		}*/
 		// Normal: transition rewards
 		else {
@@ -296,12 +296,12 @@ public class ProbModelChecker extends StateModelChecker
 				guard = rewStr.getStates(i);
 				action = rewStr.getSynch(i);
 				for (j = 0; j < numStates; j++) {
-					if (guard.evaluateBoolean(statesList.get(j))) {
+					if (guard.evaluateBoolean(constantValues, statesList.get(j))) {
 						numChoices = mdp.getNumChoices(j);
 						for (k = 0; k < numChoices; k++) {
 							mdpAction = mdp.getAction(j, k); 
 							if (mdpAction == null ? (action == null) : mdpAction.equals(action)) {
-								rewSimple.setTransitionReward(j, k, rewStr.getReward(i).evaluateDouble(statesList.get(j)));
+								rewSimple.setTransitionReward(j, k, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
 							}
 						}
 					}