Consistent treatment of illegal rewards in symbolic/explicit engines.

Both types of engine now disallow negative/infinite/NaN rewards.
Symbolic engines will mostly still not detect the presence of NaN
due to the way that CUDD deals with this.

Regression tests also added.

prism-tests/functionality/language/infinite-rewards.prism

@@ -0,0 +1,23 @@
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the die
+	d : [0..6] init 0;
+	
+	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+	[] s=7 -> (s'=7);
+	
+endmodule
+
+rewards "coin_flips"
+	s<7 : s/0;
+endrewards

prism-tests/functionality/language/infinite-rewards.prism.props

@@ -0,0 +1,2 @@
+// RESULT: Error
+R=? [F s=7];

prism-tests/functionality/language/infinite-rewards.prism.props.args

@@ -0,0 +1,2 @@
+-s
+-ex

prism-tests/functionality/language/nan-rewards.prism

@@ -0,0 +1,23 @@
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the die
+	d : [0..6] init 0;
+	
+	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+	[] s=7 -> (s'=7);
+	
+endmodule
+
+rewards "coin_flips"
+	s<7 : 0/0;
+endrewards

prism-tests/functionality/language/nan-rewards.prism.props

@@ -0,0 +1,2 @@
+// RESULT: Error
+R=? [F s=7];

prism-tests/functionality/language/nan-rewards.prism.props.args

@@ -0,0 +1,2 @@
+#-s
+-ex

prism-tests/functionality/language/negative-rewards.prism

@@ -0,0 +1,24 @@
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the die
+	d : [0..6] init 0;
+	
+	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+	[] s=7 -> (s'=7);
+	
+endmodule
+
+rewards "coin_flips"
+	s<7 : 2;
+	s<7 : 1-2;
+endrewards

prism-tests/functionality/language/negative-rewards.prism.props

@@ -0,0 +1,2 @@
+// RESULT: Error
+R=? [F s=7];

prism-tests/functionality/language/negative-rewards.prism.props.args

@@ -0,0 +1,2 @@
+-s
+-ex

prism/src/explicit/rewards/ConstructRewards.java

@@ -454,8 +454,8 @@ public class ConstructRewards extends PrismComponent
 	private void checkStateReward(double rew, Object stateIndex, ASTElement ast) throws PrismException
 	{
 		String error = null;
-		if (Double.isNaN(rew)) {
-			error = "State reward evaluates to NaN";
+		if (!Double.isFinite(rew)) {
+			error = "State reward is not finite";
 		} else if (!allowNegative && rew < 0) {
 			error = "State reward is negative (" + rew + ")";
 		}
@@ -483,8 +483,8 @@ public class ConstructRewards extends PrismComponent
 	private void checkTransitionReward(double rew, Object stateIndex, ASTElement ast) throws PrismException
 	{
 		String error = null;
-		if (Double.isNaN(rew)) {
-			error = "Transition reward evaluates to NaN";
+		if (!Double.isFinite(rew)) {
+			error = "Transition reward is not finite";
 		} else if (!allowNegative && rew < 0) {
 			error = "Transition reward is negative (" + rew + ")";
 		}

prism/src/prism/Modules2MTBDD.java

@@ -1968,9 +1968,23 @@ public class Modules2MTBDD
 				if (synch == null) {
 					// restrict rewards to relevant states
 					item = JDD.Apply(JDD.TIMES, states, rewards);
-					// check for negative rewards
-					if ((d = JDD.FindMin(item)) < 0) {
-						s = "Reward structure item contains negative rewards (" + d + ").";
+					// check for infinite/NaN/negative rewards
+					double dmin = JDD.FindMin(item);
+					double dmax = JDD.FindMax(item);
+					if (!Double.isFinite(dmin)) {
+						s = "Reward structure item contains non-finite rewards (" + dmin + ").";
+						s += "\nNote that these may correspond to states which are unreachable.";
+						s += "\nIf this is the case, try strengthening the predicate.";
+						throw new PrismLangException(s, rs.getRewardStructItem(i));
+					}
+					if (!Double.isFinite(dmax)) {
+						s = "Reward structure item contains non-finite rewards (" + dmax + ").";
+						s += "\nNote that these may correspond to states which are unreachable.";
+						s += "\nIf this is the case, try strengthening the predicate.";
+						throw new PrismLangException(s, rs.getRewardStructItem(i));
+					}
+					if (dmin < 0) {
+						s = "Reward structure item contains negative rewards (" + dmin + ").";
 						s += "\nNote that these may correspond to states which are unreachable.";
 						s += "\nIf this is the case, try strengthening the predicate.";
 						throw new PrismLangException(s, rs.getRewardStructItem(i));
@@ -2001,9 +2015,23 @@ public class Modules2MTBDD
 					item = JDD.Apply(JDD.TIMES, item, states);
 					// multiply by reward values
 					item = JDD.Apply(JDD.TIMES, item, rewards);
-					// check for negative rewards
-					if ((d = JDD.FindMin(item)) < 0) {
-						s = "Reward structure item contains negative rewards (" + d + ").";
+					// check for infinite/NaN/negative rewards
+					double dmin = JDD.FindMin(item);
+					double dmax = JDD.FindMax(item);
+					if (!Double.isFinite(dmin)) {
+						s = "Reward structure item contains non-finite rewards (" + dmin + ").";
+						s += "\nNote that these may correspond to states which are unreachable.";
+						s += "\nIf this is the case, try strengthening the predicate.";
+						throw new PrismLangException(s, rs.getRewardStructItem(i));
+					}
+					if (!Double.isFinite(dmax)) {
+						s = "Reward structure item contains non-finite rewards (" + dmax + ").";
+						s += "\nNote that these may correspond to states which are unreachable.";
+						s += "\nIf this is the case, try strengthening the predicate.";
+						throw new PrismLangException(s, rs.getRewardStructItem(i));
+					}
+					if (dmin < 0) {
+						s = "Reward structure item contains negative rewards (" + dmin + ").";
 						s += "\nNote that these may correspond to states which are unreachable.";
 						s += "\nIf this is the case, try strengthening the predicate.";
 						throw new PrismLangException(s, rs.getRewardStructItem(i));

prism/src/simulator/ModulesFileModelGenerator.java

@@ -415,8 +415,15 @@ public class ModulesFileModelGenerator implements ModelGenerator, RewardGenerato
 				Expression guard = rewStr.getStates(i);
 				if (guard.evaluateBoolean(modulesFile.getConstantValues(), state)) {
 					double rew = rewStr.getReward(i).evaluateDouble(modulesFile.getConstantValues(), state);
-					if (Double.isNaN(rew))
-						throw new PrismLangException("Reward structure evaluates to NaN at state " + state, rewStr.getReward(i));
+					// Check reward is finite/non-negative (would be checked at model construction time,
+					// but more fine grained error reporting can be done here)
+					// Note use of original model since modulesFile may have been simplified
+					if (!Double.isFinite(rew)) {
+						throw new PrismLangException("Reward structure is not finite at state " + state, originalModulesFile.getRewardStruct(r).getReward(i));
+					}
+					if (rew < 0) {
+						throw new PrismLangException("Reward structure is negative + (" + rew + ") at state " + state, originalModulesFile.getRewardStruct(r).getReward(i));
+					}
 					d += rew;
 				}
 			}
@@ -437,8 +444,15 @@ public class ModulesFileModelGenerator implements ModelGenerator, RewardGenerato
 				if (action == null ? (cmdAction.isEmpty()) : action.equals(cmdAction)) {
 					if (guard.evaluateBoolean(modulesFile.getConstantValues(), state)) {
 						double rew = rewStr.getReward(i).evaluateDouble(modulesFile.getConstantValues(), state);
-						if (Double.isNaN(rew))
-							throw new PrismLangException("Reward structure evaluates to NaN at state " + state, rewStr.getReward(i));
+						// Check reward is finite/non-negative (would be checked at model construction time,
+						// but more fine grained error reporting can be done here)
+						// Note use of original model since modulesFile may have been simplified
+						if (!Double.isFinite(rew)) {
+							throw new PrismLangException("Reward structure is not finite at state " + state, originalModulesFile.getRewardStruct(r).getReward(i));
+						}
+						if (rew < 0) {
+							throw new PrismLangException("Reward structure is negative + (" + rew + ") at state " + state, originalModulesFile.getRewardStruct(r).getReward(i));
+						}
 						d += rew;
 					}
 				}