From 9e92701a7402b79a1d582ae9758b533b43d3cc41 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 15 Aug 2017 07:46:44 +0000 Subject: [PATCH] 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 | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index 0b21ecd9..594d545d 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/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); }