diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 6ecfce96..74d74c4d 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -245,7 +245,7 @@ public class ProbModelChecker extends StateModelChecker } // Special case: constant rewards if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) { - return new MCRewardsStateConstant(rewStr.getReward(0).evaluateDouble()); + return new MCRewardsStateConstant(rewStr.getReward(0).evaluateDouble(constantValues)); } // Normal: state rewards else { @@ -256,8 +256,8 @@ public class ProbModelChecker extends StateModelChecker for (i = 0; i < n; i++) { guard = rewStr.getStates(i); for (j = 0; j < numStates; j++) { - if (guard.evaluateBoolean(statesList.get(j))) { - rewSA.setStateReward(j, rewStr.getReward(i).evaluateDouble(statesList.get(j))); + if (guard.evaluateBoolean(constantValues, statesList.get(j))) { + rewSA.setStateReward(j, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j))); } } } @@ -284,7 +284,7 @@ public class ProbModelChecker extends StateModelChecker // Special case: constant rewards // TODO /*if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) { - return new MCRewardsStateConstant(rewStr.getReward(0).evaluateDouble()); + return new MCRewardsStateConstant(rewStr.getReward(0).evaluateDouble(constantValues)); }*/ // Normal: transition rewards else { @@ -296,12 +296,12 @@ public class ProbModelChecker extends StateModelChecker guard = rewStr.getStates(i); action = rewStr.getSynch(i); for (j = 0; j < numStates; j++) { - if (guard.evaluateBoolean(statesList.get(j))) { + if (guard.evaluateBoolean(constantValues, statesList.get(j))) { numChoices = mdp.getNumChoices(j); for (k = 0; k < numChoices; k++) { mdpAction = mdp.getAction(j, k); if (mdpAction == null ? (action == null) : mdpAction.equals(action)) { - rewSimple.setTransitionReward(j, k, rewStr.getReward(i).evaluateDouble(statesList.get(j))); + rewSimple.setTransitionReward(j, k, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j))); } } }