Fix: floor/ceil of NaN/inf is an error.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2185 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/parser/ast/ExpressionFunc.java

@@ -232,12 +232,20 @@ public class ExpressionFunc extends Expression
 
 	public Object evaluateFloor(EvaluateContext ec) throws PrismLangException
 	{
-		return new Integer((int) Math.floor(getOperand(0).evaluateDouble(ec)));
+		double d = Math.floor(getOperand(0).evaluateDouble(ec));
+		// Check for NaN or +/-inf, otherwise possible errors lost in cast to int
+		if (Double.isNaN(d) || Double.isInfinite(d))
+			throw new PrismLangException("Cannot take floor() of " + d, this);
+		return new Integer((int) d);
 	}
 
 	public Object evaluateCeil(EvaluateContext ec) throws PrismLangException
 	{
-		return new Integer((int) Math.ceil(getOperand(0).evaluateDouble(ec)));
+		double d = Math.ceil(getOperand(0).evaluateDouble(ec));
+		// Check for NaN or +/-inf, otherwise possible errors lost in cast to int
+		if (Double.isNaN(d) || Double.isInfinite(d))
+			throw new PrismLangException("Cannot take ceil() of " + d, this);
+		return new Integer((int) d);
 	}
 
 	public Object evaluatePow(EvaluateContext ec) throws PrismLangException

prism/src/prism/StateModelChecker.java

@@ -781,9 +781,11 @@ public class StateModelChecker implements ModelChecker
 			dd1 = ((StateValuesMTBDD) res1).getJDDNode();
 			switch (op) {
 			case ExpressionFunc.FLOOR:
+				// NB: Floor result kept as double, so don't need to check if operand is NaN
 				dd1 = JDD.MonadicApply(JDD.FLOOR, dd1);
 				break;
 			case ExpressionFunc.CEIL:
+				// NB: Ceil result kept as double, so don't need to check if operand is NaN
 				dd1 = JDD.MonadicApply(JDD.CEIL, dd1);
 				break;
 			}
@@ -795,10 +797,12 @@ public class StateModelChecker implements ModelChecker
 			n = dv1.getSize();
 			switch (op) {
 			case ExpressionFunc.FLOOR:
+				// NB: Floor result kept as double, so don't need to check if operand is NaN
 				for (i = 0; i < n; i++)
 					dv1.setElement(i, Math.floor(dv1.getElement(i)));
 				break;
 			case ExpressionFunc.CEIL:
+				// NB: Ceil result kept as double, so don't need to check if operand is NaN
 				for (i = 0; i < n; i++)
 					dv1.setElement(i, Math.ceil(dv1.getElement(i)));
 				break;