From 17dc2a91b2e512e2362984813df248428f38a1bf Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 5 May 2014 20:47:27 +0000 Subject: [PATCH] NaN values in rewards cause an error (explicit engine only so far). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8188 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../explicit/rewards/ConstructRewards.java | 26 +++++++++++++++---- 1 file changed, 21 insertions(+), 5 deletions(-) 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); } } }