From e24275eb8c4128ec067271d2b1dde51450c6439a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 11 Jul 2014 20:50:09 +0000 Subject: [PATCH] Small refactor for reward construction in explicit model checkers. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8814 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ProbModelChecker.java | 34 +++++++++++++++--------- 1 file changed, 22 insertions(+), 12 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index aa462ab1..47583de0 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -703,18 +703,7 @@ public class ProbModelChecker extends NonProbModelChecker // Build rewards mainLog.println("Building reward structure..."); - ConstructRewards constructRewards = new ConstructRewards(mainLog); - switch (model.getModelType()) { - case CTMC: - case DTMC: - rewards = constructRewards.buildMCRewardStructure((DTMC) model, rewStruct, constantValues); - break; - case MDP: - rewards = constructRewards.buildMDPRewardStructure((MDP) model, rewStruct, constantValues); - break; - default: - throw new PrismException("Cannot build rewards for " + model.getModelType() + "s"); - } + rewards = constructRewards(model, rewStruct); // Compute rewards MinMax minMax = (relOp.isLowerBound() || relOp.isMin()) ? MinMax.min() : MinMax.max(); @@ -738,6 +727,27 @@ public class ProbModelChecker extends NonProbModelChecker } } + /** + * Construct rewards from a reward structure and a model. + */ + protected Rewards constructRewards(Model model, RewardStruct rewStruct) throws PrismException + { + Rewards rewards; + ConstructRewards constructRewards = new ConstructRewards(mainLog); + switch (model.getModelType()) { + case CTMC: + case DTMC: + rewards = constructRewards.buildMCRewardStructure((DTMC) model, rewStruct, constantValues); + break; + case MDP: + rewards = constructRewards.buildMDPRewardStructure((MDP) model, rewStruct, constantValues); + break; + default: + throw new PrismException("Cannot build rewards for " + model.getModelType() + "s"); + } + return rewards; + } + /** * Compute rewards for the contents of an R operator. */