diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 00666eeb..4d9e11f8 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -528,22 +528,8 @@ public class NondetModelChecker extends NonProbModelChecker exprProb = null; relOp = exprReward.getRelOp(); Object rs = exprReward.getRewardStructIndex(); - JDDNode transRewards = null; - JDDNode stateRewards = null; - if (model.getNumRewardStructs() == 0) - throw new PrismException("Model has no rewards specified"); - if (rs == null) { - transRewards = model.getTransRewards(0); - stateRewards = model.getStateRewards(0); - } else if (rs instanceof Expression) { - int j = ((Expression) rs).evaluateInt(constantValues); - rs = new Integer(j); // for better error reporting below - transRewards = model.getTransRewards(j - 1); - stateRewards = model.getStateRewards(j - 1); - } else if (rs instanceof String) { - transRewards = model.getTransRewards((String) rs); - stateRewards = model.getStateRewards((String) rs); - } + JDDNode stateRewards = getStateRewardsByIndexObject(rs, model, constantValues); + JDDNode transRewards = getTransitionRewardsByIndexObject(rs, model, constantValues); //check if there are state rewards and display a warning if (stateRewards != null && !stateRewards.equals(JDD.ZERO))