From 03cf76f5d6fb0a281344c0501754e5732f0dac32 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 22 Oct 2010 09:41:29 +0000 Subject: [PATCH] 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 | 12 ++++++++++-- prism/src/prism/StateModelChecker.java | 4 ++++ 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/prism/src/parser/ast/ExpressionFunc.java b/prism/src/parser/ast/ExpressionFunc.java index 848551cb..3aece49a 100644 --- a/prism/src/parser/ast/ExpressionFunc.java +++ b/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 diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index d53f2a0e..53e07083 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/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;