diff --git a/prism/src/explicit/rewards/ConstructRewards.java b/prism/src/explicit/rewards/ConstructRewards.java index 72a2bf64..b74bd617 100644 --- a/prism/src/explicit/rewards/ConstructRewards.java +++ b/prism/src/explicit/rewards/ConstructRewards.java @@ -39,6 +39,7 @@ import parser.ast.Expression; import parser.ast.RewardStruct; import prism.PrismException; import prism.PrismFileLog; +import prism.PrismLangException; import prism.PrismLog; import explicit.DTMC; import explicit.MDP; @@ -95,7 +96,10 @@ public class ConstructRewards } // Special case: constant rewards if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) { - return new StateRewardsConstant(rewStr.getReward(0).evaluateDouble(constantValues)); + double rew = rewStr.getReward(0).evaluateDouble(constantValues); + if (Double.isNaN(rew)) + throw new PrismLangException("Reward structure evaluates to NaN (at any state)", rewStr.getReward(0)); + return new StateRewardsConstant(rew); } // Normal: state rewards else { @@ -107,7 +111,10 @@ public class ConstructRewards guard = rewStr.getStates(i); for (j = 0; j < numStates; j++) { if (guard.evaluateBoolean(constantValues, statesList.get(j))) { - rewSA.addToStateReward(j, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j))); + double rew = rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)); + if (Double.isNaN(rew)) + throw new PrismLangException("Reward structure evaluates to NaN at state " + statesList.get(j), rewStr.getReward(i)); + rewSA.addToStateReward(j, rew); } } } @@ -131,7 +138,10 @@ public class ConstructRewards // Special case: constant state rewards if (rewStr.getNumStateItems() == 1 && Expression.isTrue(rewStr.getStates(0)) && rewStr.getReward(0).isConstant()) { - return new StateRewardsConstant(rewStr.getReward(0).evaluateDouble(constantValues)); + double rew = rewStr.getReward(0).evaluateDouble(constantValues); + if (Double.isNaN(rew)) + throw new PrismLangException("Reward structure evaluates to NaN (at any state)", rewStr.getReward(0)); + return new StateRewardsConstant(rew); } // Normal: state and transition rewards else { @@ -151,13 +161,19 @@ public class ConstructRewards for (k = 0; k < numChoices; k++) { mdpAction = mdp.getAction(j, k); if (mdpAction == null ? (action.isEmpty()) : mdpAction.equals(action)) { - rewSimple.addToTransitionReward(j, k, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j))); + double rew = rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)); + if (Double.isNaN(rew)) + throw new PrismLangException("Reward structure evaluates to NaN at state " + statesList.get(j), rewStr.getReward(i)); + rewSimple.addToTransitionReward(j, k, rew); } } } // State reward else { - rewSimple.addToStateReward(j, rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j))); + double rew = rewStr.getReward(i).evaluateDouble(constantValues, statesList.get(j)); + if (Double.isNaN(rew)) + throw new PrismLangException("Reward structure evaluates to NaN at state " + statesList.get(j), rewStr.getReward(i)); + rewSimple.addToStateReward(j, rew); } } }