exact engine: protect against negative/non-normal rewards for Rmax[F] / Rmin[F] and non-normal rewards for R[F]

prism/src/param/ParamRewardStruct.java

@@ -26,6 +26,9 @@
 
 package param;
 
+import prism.PrismException;
+import prism.PrismNotSupportedException;
+
 /**
  * Reward structure for parametric model.
  * We only consider rewards assigned to a certain nondeterministic choice,
@@ -122,7 +125,47 @@ final class ParamRewardStruct {
 	{
 		return rewards[choice];
 	}
-	
+
+	/**
+	 * Returns true if there are negative rewards.
+	 * <br>
+	 * Can only be called on a reward structure that
+	 * has been instantiated, i.e., where all rewards
+	 * are constant rational numbers.
+	 * <br>
+	 * If either +/-Inf or NaN are encountered, an exception is thrown.
+	 */
+	public boolean hasNegativeRewards() throws PrismException
+	{
+		for (Function r : rewards) {
+			if (!r.isConstant()) {
+				throw new UnsupportedOperationException("Can not check for negative rewards against non-constant functions");
+			}
+			BigRational v = r.asBigRational();
+			if (v.isSpecial()) {
+				throw new PrismNotSupportedException("Reward value " + v + " not supported");
+			}
+			if (r.asBigRational().signum() < 0) {
+				return true;
+			}
+		}
+
+		return false;
+	}
+
+	/**
+	 * Check for non-normal reward values, i.e., +/-Inf and NaN,
+	 * throw exception if detected.
+	 */
+	public void checkForNonNormalRewards() throws PrismException
+	{
+		for (Function r : rewards) {
+			if (r.isInf() || r.isMInf() || r.isNaN()) {
+				throw new PrismNotSupportedException("Reward value " + r + " not supported");
+			}
+		}
+	}
+
 	@Override
 	public String toString() {
 		StringBuffer result = new StringBuffer();

prism/src/param/ValueComputer.java

@@ -294,12 +294,16 @@ final class ValueComputer extends PrismComponent
 		}
 	}
 
-	private RegionValues computeUnboundedMC(Region region, StateValues b1, StateValues b2, ParamRewardStruct rew)
+	private RegionValues computeUnboundedMC(Region region, StateValues b1, StateValues b2, ParamRewardStruct rew) throws PrismException
 	{
 		// Convert to MutablePMC, using trivial scheduler (take first choice everywhere)
 		Scheduler trivialScheduler = new Scheduler(model);
 
 		MutablePMC pmc = buildAlterablePMCForReach(model, b1, b2, trivialScheduler, rew);
+		if (rew != null && mode == ParamMode.EXACT) {
+			rew.checkForNonNormalRewards();
+		}
+
 		StateValues values = computeValues(pmc, model.getFirstInitialState());
 		return regionFactory.completeCover(values);
 	}
@@ -395,6 +399,9 @@ final class ValueComputer extends PrismComponent
 		ParamRewardStruct rewConcrete = null;
 		if (rew != null) {
 			rewConcrete = rew.instantiate(point);
+			if (mode == ParamMode.EXACT && rewConcrete.hasNegativeRewards()) {
+				throw new PrismNotSupportedException(mode.Engine() + " currently does not support negative rewards in reachability reward computations");
+			}
 		}
 		
 		Scheduler scheduler = lookupScheduler(point, concrete, PropType.REACH, b1, b2, min, rewConcrete);