From 8a9701e7ec386261ace7702babcd1548f77e33f3 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 16 Jul 2015 22:35:56 +0000 Subject: [PATCH] Code tidy git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10339 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/ProbModelChecker.java | 62 ++++++++++++------------ 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index b7139e88..ede5acaf 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -916,37 +916,6 @@ public class ProbModelChecker extends NonProbModelChecker return rewards; } - /** - * Compute rewards for a reachability reward operator. - */ - protected StateValues checkRewardReach(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException - { - // Model check the operand for all states - BitSet target = checkExpression(model, expr.getOperand2(), null).getBitSet(); - - // Compute/return the rewards - ModelCheckerResult res = null; - switch (model.getModelType()) { - case DTMC: - res = ((DTMCModelChecker) this).computeReachRewards((DTMC) model, (MCRewards) modelRewards, target); - break; - case CTMC: - res = ((CTMCModelChecker) this).computeReachRewards((CTMC) model, (MCRewards) modelRewards, target); - break; - case MDP: - res = ((MDPModelChecker) this).computeReachRewards((MDP) model, (MDPRewards) modelRewards, target, minMax.isMin()); - result.setStrategy(res.strat); - break; - case STPG: - res = ((STPGModelChecker) this).computeReachRewards((STPG) model, (STPGRewards) modelRewards, target, minMax.isMin1(), minMax.isMin2()); - break; - default: - throw new PrismNotSupportedException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType() - + "s"); - } - return StateValues.createFromDoubleArray(res.soln, model); - } - /** * Compute rewards for an instantaneous reward operator. */ @@ -1063,6 +1032,37 @@ public class ProbModelChecker extends NonProbModelChecker throw new PrismException("Invalid contents for an R operator: " + expr); } + /** + * Compute rewards for a reachability reward operator. + */ + protected StateValues checkRewardReach(Model model, Rewards modelRewards, ExpressionTemporal expr, MinMax minMax, BitSet statesOfInterest) throws PrismException + { + // Model check the operand for all states + BitSet target = checkExpression(model, expr.getOperand2(), null).getBitSet(); + + // Compute/return the rewards + ModelCheckerResult res = null; + switch (model.getModelType()) { + case DTMC: + res = ((DTMCModelChecker) this).computeReachRewards((DTMC) model, (MCRewards) modelRewards, target); + break; + case CTMC: + res = ((CTMCModelChecker) this).computeReachRewards((CTMC) model, (MCRewards) modelRewards, target); + break; + case MDP: + res = ((MDPModelChecker) this).computeReachRewards((MDP) model, (MDPRewards) modelRewards, target, minMax.isMin()); + result.setStrategy(res.strat); + break; + case STPG: + res = ((STPGModelChecker) this).computeReachRewards((STPG) model, (STPGRewards) modelRewards, target, minMax.isMin1(), minMax.isMin2()); + break; + default: + throw new PrismNotSupportedException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType() + + "s"); + } + return StateValues.createFromDoubleArray(res.soln, model); + } + /** * Compute rewards for a co-safe LTL reward operator. */