ParamModelChecker: fix CTMC reward computation for transition rewards (--param / --exact mode)

For CTMCs, only the state rewards, but not the transition rewards
are scaled by the rates.

Failing tests e.g.
functionality/verify/ctmcs/rewards/ctmc_rewards.sm

(14) R{"a"}=? [ F s=1 ]

from functionality/verify/ctmcs/rewards/ctmc_rewards.sm.props
in the test suite with --exact mode


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

prism/src/param/ParamModelChecker.java

@@ -1083,6 +1083,10 @@ final public class ParamModelChecker extends PrismComponent
 						Function sumOut = model.sumLeaving(choice);
 						Function choiceReward;
 						if (!isTransitionReward) {
+							// for state reward, scale by sumOut
+							// For DTMC/MDP, this changes nothing;
+							// for CTMC this takes the expected duration
+							// in this state into account
 							choiceReward = newReward.divide(sumOut);
 						} else {
 							choiceReward = functionFactory.getZero();
@@ -1092,7 +1096,7 @@ final public class ParamModelChecker extends PrismComponent
 									choiceReward = choiceReward.add(newReward.multiply(model.succProb(succ)));
 								}
 							}
-							choiceReward = choiceReward.divide(sumOut);
+							// does not get scaled by sumOut
 						}
 						rewSimple.addReward(choice, choiceReward);
 					}