From ff697f7196d874cd0680e499e3b4995bbb86b25d Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 22 Oct 2010 07:51:56 +0000
Subject: [PATCH] Correct detection of erroneous integer powers with negative
 exponent.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2180 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/ast/ExpressionFunc.java |  7 +++++-
 prism/src/prism/StateModelChecker.java   | 31 ++++++++++++++++++++++--
 2 files changed, 35 insertions(+), 3 deletions(-)

diff --git a/prism/src/parser/ast/ExpressionFunc.java b/prism/src/parser/ast/ExpressionFunc.java
index b4eff66b..e5eecdb4 100644
--- a/prism/src/parser/ast/ExpressionFunc.java
+++ b/prism/src/parser/ast/ExpressionFunc.java
@@ -242,7 +242,12 @@ public class ExpressionFunc extends Expression
 
 	public Object evaluatePow(EvaluateContext ec) throws PrismLangException
 	{
-		double res = Math.pow(getOperand(0).evaluateDouble(ec), getOperand(1).evaluateDouble(ec));
+		double base = getOperand(0).evaluateDouble(ec);
+		double exp = getOperand(1).evaluateDouble(ec);
+		// Not allowed to do e.g. pow(1,-2) because of typing (should be pow(1.0,-2) instead)
+		if (type instanceof TypeInt || (exp < 0))
+			throw new PrismLangException("Negative exponent not allowed for integer power", this);
+		double res = Math.pow(base, exp);
 		if (type instanceof TypeInt) {
 			if (res > Integer.MAX_VALUE)
 				throw new PrismLangException("Overflow evaluating integer power", this);
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index 8a8d3024..0a153e86 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -832,7 +832,23 @@ public class StateModelChecker implements ModelChecker
 			dd2 = ((StateValuesMTBDD) res2).getJDDNode();
 			switch (op) {
 			case ExpressionFunc.POW:
+				// Deref dd1/dd2 because may still need below
+				JDD.Ref(dd1);
+				JDD.Ref(dd2);
 				dd = JDD.Apply(JDD.POW, dd1, dd2);
+				// Check for some possible problems in case of integer power
+				// (denote error with NaN for states with problems)
+				if (expr.getType() instanceof TypeInt) {
+					// Negative exponent not allowed for integer power
+					JDD.Ref(dd2);
+					dd = JDD.ITE(JDD.LessThan(dd2, 0), JDD.Constant(0.0/0.0), dd);
+					// Check for integer overflow 
+					JDD.Ref(dd);
+					dd = JDD.ITE(JDD.GreaterThan(dd, Integer.MAX_VALUE), JDD.Constant(0.0/0.0), dd);
+				}
+				// Late deref of dd1/dd2 because needed above
+				JDD.Deref(dd1);
+				JDD.Deref(dd2);
 				break;
 			case ExpressionFunc.MOD:
 				dd = JDD.Apply(JDD.MOD, dd1, dd2);
@@ -850,8 +866,19 @@ public class StateModelChecker implements ModelChecker
 			n = dv1.getSize();
 			switch (op) {
 			case ExpressionFunc.POW:
-				for (i = 0; i < n; i++)
-					dv1.setElement(i, Math.pow(dv1.getElement(i), dv2.getElement(i)));
+				// For integer power, have to check for errors and flag as NaN
+				if (expr.getType() instanceof TypeInt) {
+					double base, exp, pow;
+					for (i = 0; i < n; i++) {
+						base = dv1.getElement(i);
+						exp = dv2.getElement(i);
+						pow = Math.pow(base, exp);
+						dv1.setElement(i, (exp < 0 || pow > Integer.MAX_VALUE) ? 0.0/0.0: pow);
+					}
+				} else {
+					for (i = 0; i < n; i++)
+						dv1.setElement(i, Math.pow(dv1.getElement(i), dv2.getElement(i)));
+				}
 				break;
 			case ExpressionFunc.MOD:
 				for (i = 0; i < n; i++) {