From eacd8b3bd8a3a892f04cc68be2e116be71c7ffa4 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 2 May 2007 11:34:41 +0000
Subject: [PATCH] Added log function to PRISM language (but not actually
 supported yet, except in constant evaluations).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@325 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/ExpressionFunc.java  | 26 +++++++++++++++++++++++---
 prism/src/prism/Expression2MTBDD.java |  1 +
 prism/src/prism/PrismUtils.java       | 17 +++++++++++++++--
 3 files changed, 39 insertions(+), 5 deletions(-)

diff --git a/prism/src/parser/ExpressionFunc.java b/prism/src/parser/ExpressionFunc.java
index 396d2dcd..cc6e6c71 100644
--- a/prism/src/parser/ExpressionFunc.java
+++ b/prism/src/parser/ExpressionFunc.java
@@ -30,6 +30,7 @@ package parser;
 import java.util.Vector;
 
 import prism.PrismException;
+import prism.PrismUtils;
 import simulator.*;
 
 public class ExpressionFunc extends ExpressionNary
@@ -41,11 +42,12 @@ public class ExpressionFunc extends ExpressionNary
 	public static final int CEIL = 3;
 	public static final int POW = 4;
 	public static final int MOD = 5;
+	public static final int LOG = 6;
 	// strings for names
-	public static final String names[] = {"min", "max", "floor", "ceil", "pow", "mod"};
+	public static final String names[] = {"min", "max", "floor", "ceil", "pow", "mod", "log"};
 	// min/max function arities
-	public static final int minArities[] = {2, 2, 1, 1, 2, 2};
-	public static final int maxArities[] = {-1, -1, 1, 1, 2, 2};
+	public static final int minArities[] = {2, 2, 1, 1, 2, 2, 2};
+	public static final int maxArities[] = {-1, -1, 1, 1, 2, 2, 2};
 
 	// function name
 	private String name = "";
@@ -178,6 +180,7 @@ public class ExpressionFunc extends ExpressionNary
 			case FLOOR:
 			case CEIL:
 			case POW:
+			case LOG:
 				// all operands must be ints or doubles
 				for (i = 0; i < n; i++) {
 					if (types[i] == Expression.BOOLEAN) {
@@ -217,6 +220,7 @@ public class ExpressionFunc extends ExpressionNary
 				break;
 				
 			case POW:
+			case LOG:
 				// resulting type is always double
 				setType(Expression.DOUBLE);
 				break;
@@ -239,6 +243,7 @@ public class ExpressionFunc extends ExpressionNary
 			case CEIL: return evaluateCeil(constantValues, varValues);
 			case POW: return evaluatePow(constantValues, varValues);
 			case MOD: return evaluateMod(constantValues, varValues);
+			case LOG: return evaluateLog(constantValues, varValues);
 			default: return null;
 		}
 	}
@@ -389,6 +394,15 @@ public class ExpressionFunc extends ExpressionNary
 // 		}
 	}
 
+	public Object evaluateLog(Values constantValues, Values varValues) throws PrismException
+	{
+		double x, b;
+		
+		x = getOperand(0).evaluateDouble(constantValues, varValues);
+		b = getOperand(1).evaluateDouble(constantValues, varValues);
+		return new Double(PrismUtils.log(x, b));
+	}
+	
 	/**
 	 *	Convert and build simulator expression data structure
 	 */
@@ -460,6 +474,12 @@ public class ExpressionFunc extends ExpressionNary
 				{
 					return SimulatorEngine.createMod(getOperand(0).toSimulator(sim), getOperand(1).toSimulator(sim));
 				}
+				
+				case LOG:
+				{
+					throw new SimulatorException("The log function is not yet supported in PRISM");
+				}
+				
 				default:
 					throw new SimulatorException("Unrecognised function \"" + name + "\"");
 			}
diff --git a/prism/src/prism/Expression2MTBDD.java b/prism/src/prism/Expression2MTBDD.java
index 0e73b086..dfe5e9a1 100644
--- a/prism/src/prism/Expression2MTBDD.java
+++ b/prism/src/prism/Expression2MTBDD.java
@@ -540,6 +540,7 @@ public class Expression2MTBDD
 			case ExpressionFunc.CEIL: return translateExpressionFuncCeil(expr);
 			case ExpressionFunc.POW: return translateExpressionFuncPow(expr);
 			case ExpressionFunc.MOD: return translateExpressionFuncMod(expr);
+			case ExpressionFunc.LOG: throw new PrismException("The log function is not yet supported in PRISM");
 			default: throw new PrismException("Unrecognised function \"" + expr.getName() + "\"");
 		}
 	}
diff --git a/prism/src/prism/PrismUtils.java b/prism/src/prism/PrismUtils.java
index a8506e86..d8000f76 100644
--- a/prism/src/prism/PrismUtils.java
+++ b/prism/src/prism/PrismUtils.java
@@ -55,8 +55,21 @@ public class PrismUtils
 
 //------------------------------------------------------------------------------
 
-	// small utility methods in java
-
+	// Small utility methods in java
+	
+	// Logarithm of x to base b
+	
+	public static double log(double x, double b)
+	{
+		// Base needs to be >0 and !=1, otherwise return NaN
+		if (b <= 0 || b == 1) return Double.NaN;
+		
+		// Otherwise, log_b (x) is log(x) / log(b)
+		return Math.log(x) / Math.log(b);
+	}
+	
+	// Logarithm of x to base 2
+	
 	public static double log2(double x)
 	{
 		return Math.log(x) / Math.log(2);