From d1e2870fbc5f6427e287870c609e76f4ea06ab33 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 11 Jul 2014 21:17:11 +0000 Subject: [PATCH] Small refactor for reward construction in other model checkers. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8819 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- ...astAdaptiveUniformisationModelChecker.java | 24 +----------------- prism/src/param/ParamModelChecker.java | 25 +------------------ 2 files changed, 2 insertions(+), 47 deletions(-) diff --git a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java b/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java index dc601ff5..2289995a 100644 --- a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java +++ b/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java @@ -220,28 +220,6 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent return new Result(new Double(fau.getValue())); } - private RewardStruct findRewardStruct(ExpressionReward expr) throws PrismException - { - RewardStruct rewStruct = null; - Object rs = expr.getRewardStructIndex(); - if (modulesFile == null) - throw new PrismException("No model file to obtain reward structures"); - if (modulesFile.getNumRewardStructs() == 0) - throw new PrismException("Model has no rewards specified"); - if (rs == null) { - rewStruct = modulesFile.getRewardStruct(0); - } else if (rs instanceof Expression) { - int i = ((Expression) rs).evaluateInt(constantValues); - rs = new Integer(i); // for better error reporting below - rewStruct = modulesFile.getRewardStruct(i - 1); - } else if (rs instanceof String) { - rewStruct = modulesFile.getRewardStructByName((String) rs); - } - if (rewStruct == null) - throw new PrismException("Invalid reward structure index \"" + rs + "\""); - return rewStruct; - } - /** * Model check an R operator. */ @@ -262,7 +240,7 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent throw new PrismException("Currently only instantaneous or cumulative rewards are allowed."); } double time = temporal.getUpperBound().evaluateDouble(constantValues); - RewardStruct rewStruct = findRewardStruct(expr); + RewardStruct rewStruct = expr.getRewardStructByIndexObject(modulesFile, constantValues); fau.setRewardStruct(rewStruct); fau.setConstantValues(constantValues); fau.computeTransientProbsAdaptive(time); diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index 14903a9c..1451a3f0 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -957,18 +957,13 @@ final public class ParamModelChecker extends PrismComponent */ protected RegionValues checkExpressionReward(ParamModel model, ExpressionReward expr, BitSet needStates) throws PrismException { - Object rs; // Reward struct index - RewardStruct rewStruct = null; // Reward struct object Expression rb; // Reward bound (expression) BigRational r = null; // Reward bound (actual value) - //String relOp; // Relational operator - ModelType modelType = model.getModelType(); RegionValues rews = null; - int i; boolean min = false; // Get info from reward operator - rs = expr.getRewardStructIndex(); + RewardStruct rewStruct = expr.getRewardStructByIndexObject(modulesFile, constantValues); RelOp relOp = expr.getRelOp(); rb = expr.getReward(); if (rb != null) { @@ -979,24 +974,6 @@ final public class ParamModelChecker extends PrismComponent } min = relOp.isLowerBound() || relOp.isMin(); - // Get reward info - if (modulesFile == null) - throw new PrismException("No model file to obtain reward structures"); - if (modulesFile.getNumRewardStructs() == 0) - throw new PrismException("Model has no rewards specified"); - if (rs == null) { - rewStruct = modulesFile.getRewardStruct(0); - } else if (rs instanceof Expression) { - i = ((Expression) rs).evaluateInt(constantValues); - rs = new Integer(i); // for better error reporting below - rewStruct = modulesFile.getRewardStruct(i - 1); - } else if (rs instanceof String) { - rewStruct = modulesFile.getRewardStructByName((String) rs); - } - if (rewStruct == null) - throw new PrismException("Invalid reward structure index \"" + rs + "\""); - - ParamRewardStruct rew = constructRewards(model, rewStruct, constantValues); mainLog.println("Building reward structure..."); rews = checkRewardFormula(model, rew, expr.getExpression(), min, needStates);