From 779878202932ca16157ce9862dfa23ffca4d486f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 30 Dec 2014 00:50:31 +0000 Subject: [PATCH] Refactoring of extraction of rewards in multi-objective model checking engine. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9466 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/NondetModelChecker.java | 18 ++---------------- 1 file changed, 2 insertions(+), 16 deletions(-) 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))