Bug fix in creating reward structures in explicit engine (from Hongyang).

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

prism/src/explicit/rewards/ConstructRewards.java

@@ -104,7 +104,7 @@ public class ConstructRewards
 				guard = rewStr.getStates(i);
 				for (j = 0; j < numStates; j++) {
 					if (guard.evaluateBoolean(constantValues, statesList.get(j))) {
-						rewSA.setStateReward(j, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
+						rewSA.addToStateReward(j, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
 					}
 				}
 			}
@@ -148,13 +148,13 @@ public class ConstructRewards
 							for (k = 0; k < numChoices; k++) {
 								mdpAction = mdp.getAction(j, k);
 								if (mdpAction == null ? (action.isEmpty()) : mdpAction.equals(action)) {
-									rewSimple.setTransitionReward(j, k, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
+									rewSimple.addToTransitionReward(j, k, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
 								}
 							}
 						}
 						// State reward
 						else {
-							rewSimple.setStateReward(j, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
+							rewSimple.addToStateReward(j, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)));
 						}
 					}
 				}

prism/src/explicit/rewards/MDPRewardsSimple.java

@@ -71,6 +71,14 @@ public class MDPRewardsSimple implements MDPRewards
 		stateRewards.set(s, r);
 	}
 
+	/**
+	 * Add {@code r} to the state reward for state {@code s}.
+	 */
+	public void addToStateReward(int s, double r)
+	{
+		setStateReward(s, stateRewards.get(s) + r);
+	}
+
 	/**
 	 * Set the transition reward for choice {@code i} of state {@code s} to {@code r}.
 	 */
@@ -101,6 +109,14 @@ public class MDPRewardsSimple implements MDPRewards
 		list.set(i, r);
 	}
 
+	/**
+	 * Add {@code r} to the transition reward for choice {@code i} of state {@code s}.
+	 */
+	public void addToTransitionReward(int s, int i, double r)
+	{
+		setTransitionReward(s, i, getTransitionReward(s, i) + r);
+	}
+	
 	/**
 	 * Clear all rewards for state s.
 	 */

prism/src/explicit/rewards/StateRewardsArray.java

@@ -55,6 +55,14 @@ public class StateRewardsArray implements MCRewards, MDPRewards
 		stateRewards[s] = r;
 	}
 	
+	/**
+	 * Add {@code r} to the state reward for state {@code s} .
+	 */
+	public void addToStateReward(int s, double r)
+	{
+		stateRewards[s] += r;
+	}
+	
 	// Accessors
 	
 	@Override