Correct handling of mod (error on non-positive divisor, positive result for negative dividend) (NB: needs CUDD fix too).

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

prism/src/parser/ast/ExpressionFunc.java

@@ -262,9 +262,12 @@ public class ExpressionFunc extends Expression
 	{
 		int i = getOperand(0).evaluateInt(ec);
 		int j = getOperand(1).evaluateInt(ec);
-		if (j == 0)
-			throw new PrismLangException("Attempt to compute modulo zero", this);
-		return new Integer(i % j);
+		// Non-positive divisor not allowed 
+		if (j <= 0)
+			throw new PrismLangException("Attempt to compute modulo with non-positive divisor", this);
+		// Take care of negative case (% is remainder, not modulo)
+		int rem = i % j;
+		return new Integer(rem < 0 ? rem + j : rem);
 	}
 
 	public Object evaluateLog(EvaluateContext ec) throws PrismLangException

prism/src/prism/StateModelChecker.java

@@ -882,9 +882,11 @@ public class StateModelChecker implements ModelChecker
 				break;
 			case ExpressionFunc.MOD:
 				for (i = 0; i < n; i++) {
-					d = (int) dv2.getElement(i);
-					d = (d == 0) ? Double.NaN : (int) dv1.getElement(i) % (int) d;
-					dv1.setElement(i, d);
+					double div = (int) dv2.getElement(i);
+					// Non-positive divisor not allowed (flag as NaN)
+					d = (div <= 0) ? Double.NaN : (int) dv1.getElement(i) % (int) div;
+					// Take care of negative case (% is remainder, not modulo)
+					dv1.setElement(i, d < 0 ? d + div : d);
 				}
 				break;
 			case ExpressionFunc.LOG: