Added (in full) log function to PRISM language.

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

prism/include/JDD.h

@@ -39,6 +39,8 @@ extern "C" {
 #define jdd_JDD_POW 15L
 #undef jdd_JDD_MOD
 #define jdd_JDD_MOD 16L
+#undef jdd_JDD_LOGXY
+#define jdd_JDD_LOGXY 17L
 #undef jdd_JDD_ZERO_ONE
 #define jdd_JDD_ZERO_ONE 1L
 #undef jdd_JDD_LOW

prism/include/SimulatorEngine.h

@@ -615,6 +615,14 @@ JNIEXPORT jlong JNICALL Java_simulator_SimulatorEngine_createRealPow
 JNIEXPORT jlong JNICALL Java_simulator_SimulatorEngine_createMod
   (JNIEnv *, jclass, jlong, jlong);
 
+/*
+ * Class:     simulator_SimulatorEngine
+ * Method:    createLog
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_simulator_SimulatorEngine_createLog
+  (JNIEnv *, jclass, jlong, jlong);
+
 /*
  * Class:     simulator_SimulatorEngine
  * Method:    createNot

prism/include/dd_basics.h

@@ -45,6 +45,7 @@
 #define APPLY_CEIL 14
 #define APPLY_POW 15
 #define APPLY_MOD 16
+#define APPLY_LOGXY 17
 
 //------------------------------------------------------------------------------
 

prism/include/simengine.h

@@ -240,6 +240,8 @@ CExpression* Engine_Create_Real_Pow(CExpression* base, CExpression* exp);
 
 CExpression* Engine_Create_Mod(CNormalExpression* left, CNormalExpression* right);
 
+CExpression* Engine_Create_Log(CExpression* left, CExpression* right);
+
 CExpression*  Engine_Create_Not(CNormalExpression* expr);
 
 CExpression* Engine_Create_And(CNormalExpression** exprs, int no_expressions);

prism/include/simexpression.h

@@ -80,6 +80,7 @@ const int EXPR_NORMAL_LESS_THAN_EQUAL       = 34;
 const int EXPR_REAL_LESS_THAN_EQUAL         = 35;
 const int EXPR_NORMAL_GREATER_THAN_EQUAL    = 36;
 const int EXPR_REAL_GREATER_THAN_EQUAL      = 37;
+const int EXPR_LOG                          = 38;
 
 //Class definitions
 
@@ -519,6 +520,24 @@ class CMod: public CNormalExpression
                 void Write_Expression(int fd);
 };
 
+class CLog: public CRealExpression
+{
+	private:
+		CExpression * lexpr;
+		CExpression * rexpr;
+	public:
+		CLog(CExpression *, CExpression *);
+		~CLog();
+		int Get_Type();
+		double EvaluateDouble();
+		double EvaluateDouble(int*);
+		bool One_Result();
+		std::string To_String();
+                void Write_Expression(int fd);
+
+		  
+};
+
 class CNormalTimes: public CNormalExpression
 {
 	private:

prism/src/dd/dd_basics.cc

@@ -167,6 +167,7 @@ DdNode *DD_Apply(DdManager *ddman, int op, DdNode *dd1, DdNode *dd2)
 		case APPLY_LESSTHANEQUALS: res = Cudd_addApply(ddman, Cudd_addLessThanEquals, dd1, dd2); break;
 		case APPLY_POW: res = Cudd_addApply(ddman, Cudd_addPow, dd1, dd2); break;
 		case APPLY_MOD: res = Cudd_addApply(ddman, Cudd_addMod, dd1, dd2); break;
+		case APPLY_LOGXY: res = Cudd_addApply(ddman, Cudd_addLogXY, dd1, dd2); break;
 		default: printf("\nError: Invalid APPLY operator.\n"); exit(1);
 	}
 	Cudd_Ref(res);

prism/src/jdd/JDD.java

@@ -146,6 +146,7 @@ public class JDD
 	public static final int CEIL = 14;
 	public static final int POW = 15;
 	public static final int MOD = 16;
+	public static final int LOGXY = 17;
 
 	// print vector/matrix accuracy
 	public static final int ZERO_ONE = 1;

prism/src/parser/ExpressionFunc.java

@@ -477,7 +477,7 @@ public class ExpressionFunc extends ExpressionNary
 				
 				case LOG:
 				{
-					throw new SimulatorException("The log function is not yet supported in PRISM");
+					return SimulatorEngine.createLog(getOperand(0).toSimulator(sim), getOperand(1).toSimulator(sim));
 				}
 				
 				default:

prism/src/prism/Expression2MTBDD.java

@@ -540,7 +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");
+			case ExpressionFunc.LOG: return translateExpressionFuncLog(expr);
 			default: throw new PrismException("Unrecognised function \"" + expr.getName() + "\"");
 		}
 	}
@@ -629,6 +629,17 @@ public class Expression2MTBDD
 		return dd;
 	}
 
+	private JDDNode translateExpressionFuncLog(ExpressionFunc expr) throws PrismException
+	{
+		JDDNode dd1, dd2, dd;
+		
+		dd1 = translateExpression(expr.getOperand(0));
+		dd2 = translateExpression(expr.getOperand(1));
+		dd = JDD.Apply(JDD.LOGXY, dd1, dd2);
+		
+		return dd;
+	}
+
 	// translate a 'var'
 	
 	private JDDNode translateExpressionVar(ExpressionVar expr) throws PrismException

prism/src/prism/PrismUtils.java

@@ -61,8 +61,8 @@ public class PrismUtils
 	
 	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;
+		// If base is <0 or ==1 (or +Inf/NaN), then result is NaN
+		if (b <= 0 || b == 1 || (Double.isInfinite(b)) || Double.isNaN(b)) return Double.NaN;
 		
 		// Otherwise, log_b (x) is log(x) / log(b)
 		return Math.log(x) / Math.log(b);

prism/src/simulator/SimulatorEngine.java

@@ -2513,6 +2513,11 @@ public class SimulatorEngine
 	 */
 	public static native long createMod(long lexprPointer, long rexprPointer);
 	
+	/**
+	 * Used by the recursive model/properties loading methods (not part of the API)
+	 */
+	public static native long createLog(long lexprPointer, long rexprPointer);
+	
 	/**
 	 * Used by the recursive model/properties loading methods (not part of the API)
 	 */

prism/src/simulator/networking/NOTES

@@ -1,5 +1,7 @@
 Some thoughts:
 
+- binary import/output doesn't handle more recently defined functions
+
 - if stop early, should really let all current samples finish so as not to favour shorter traces
 
 - take care when generating multiple random seeds, esp. if all at same time

prism/src/simulator/simengine.cc

@@ -664,6 +664,11 @@ CExpression* Engine_Create_Mod(CNormalExpression* left, CNormalExpression* right
 	return new CMod(left, right);
 }
 
+CExpression* Engine_Create_Log(CExpression* left, CExpression* right)
+{
+	return new CLog(left, right);
+}
+
 CExpression*  Engine_Create_Not(CNormalExpression* expr)
 {
 	return new CNot(expr);

prism/src/simulator/simexpression.cc

@@ -1374,6 +1374,105 @@ void CMod::Write_Expression(int fd)
 }
 
 
+//Class methods for CLog
+
+CLog::CLog(CExpression * left, CExpression * right)
+{
+	this->lexpr = left; 
+	this->rexpr = right;
+	if(lexpr->Get_Type() == BOOLEAN ||
+		rexpr->Get_Type() == BOOLEAN) 
+		throw "type error when constructing log: Boolean not accepted.";
+}
+
+CLog::~CLog()
+{
+	if(lexpr != NULL)
+	delete lexpr;
+	if(rexpr != NULL)
+	delete rexpr;
+}
+
+int CLog::Get_Type()
+{
+	return DOUBLE;
+}
+
+double CLog::EvaluateDouble()
+{
+	double val, base, res;
+	// Evaluate children
+	if(lexpr->Get_Type() == INTEGER)
+		val = lexpr->Evaluate();
+	else
+		val = lexpr->EvaluateDouble();
+	if(rexpr->Get_Type() == INTEGER)
+		base = rexpr->Evaluate();
+	else
+		base = rexpr->EvaluateDouble();
+	// If base is <0 or ==1 (or +Inf/NaN), then result is NaN
+	if (base < 0 || base == 1.0 || base == HUGE_VAL || base != base) { res = 0.0; res /= res; }
+	// If arg is <0 or NaN, then result is NaN
+	else if (val < 0 || val != val) { res = 0.0; res /= res; }
+	// If arg is +Inf, then result is +Inf
+	else if (val == HUGE_VAL) res = HUGE_VAL;
+	// If arg is (positive/negative) 0, then result is -Inf
+	else if (val == 0.0 || val == -0.0) res = -HUGE_VAL;
+	// Default case: normal log
+	else res = log(val) / log(base);
+	
+	return res;
+}
+
+double CLog::EvaluateDouble(int* vars)
+{
+	double val, base, res;
+	// Evaluate children
+	if(lexpr->Get_Type() == INTEGER)
+		val = lexpr->Evaluate(vars);
+	else
+		val = lexpr->EvaluateDouble(vars);
+	if(rexpr->Get_Type() == INTEGER)
+		base = rexpr->Evaluate(vars);
+	else
+		base = rexpr->EvaluateDouble(vars);
+	// If base is <0 or ==1 (or +Inf/NaN), then result is NaN
+	if (base < 0 || base == 1.0 || base == HUGE_VAL || base != base) { res = 0.0; res /= res; }
+	// If arg is <0 or NaN, then result is NaN
+	else if (val < 0 || val != val) { res = 0.0; res /= res; }
+	// If arg is +Inf, then result is +Inf
+	else if (val == HUGE_VAL) res = HUGE_VAL;
+	// If arg is (positive/negative) 0, then result is -Inf
+	else if (val == 0.0 || val == -0.0) res = -HUGE_VAL;
+	// Default case: normal log
+	else res = log(val) / log(base);
+	
+	return res;
+}
+
+bool CLog::One_Result()
+{
+	return lexpr->One_Result() && rexpr->One_Result();
+}
+
+std::string CLog::To_String()
+{
+	return "log{"+lexpr->To_String() + "," + rexpr->To_String()+"}";
+}
+
+void CLog::Write_Expression(int fd)
+{
+    //the type of expression
+    int expr_type = EXPR_LOG;
+    write(fd, &expr_type, sizeof(int));
+    //the information
+    lexpr->Write_Expression(fd);
+    rexpr->Write_Expression(fd);
+    //null byte to finish off expression
+    write(fd, "\0", 1);
+}
+
+
 //Class methods for CNormalTimes
 
 
@@ -2672,6 +2771,17 @@ CExpression* Read_Expression(int fd)
                 throw "Error 068 when importing binary file: expression not terminated correctly";
             }
             return new CMod(n_expr1, n_expr2);
+        case EXPR_LOG:
+            //read 2 sub-expressions
+            expr1 = Read_Expression(fd);
+            expr2 = Read_Expression(fd);
+            //read off null byte
+            read(fd, &str_buf, 1);
+            if(strcmp(str_buf, "") != 0)
+            {
+                throw "Error 068.5 when importing binary file: expression not terminated correctly";
+            }
+            return new CLog(expr1, expr2);
         case EXPR_NORMAL_TIMES:
             //read 2 sub-expressions
             n_expr1 = Read_Normal_Expression(fd);
@@ -3271,6 +3381,17 @@ CRealExpression* Read_Real_Expression(int fd)
             }
             //create the expression
             return new CRealMin(exprs, buf_int);
+        case EXPR_LOG:
+            //read 2 sub-expressions
+            expr1 = Read_Expression(fd);
+            expr2 = Read_Expression(fd);
+            //read off null byte
+            read(fd, &str_buf, 1);
+            if(strcmp(str_buf, "") != 0)
+            {
+                throw "Error 038.5 when importing binary file: expression not terminated correctly";
+            }
+            return new CLog(expr1, expr2);
         case EXPR_REAL_POW:
             //read 2 sub-expressions
             expr1 = Read_Expression(fd);

prism/src/simulator/simexpressionbuilder.cc

@@ -112,6 +112,15 @@ JNIEXPORT jlong __pointer JNICALL Java_simulator_SimulatorEngine_createMod
 	return ptr_to_jlong(modExpr);
 }
 
+JNIEXPORT jlong __pointer JNICALL Java_simulator_SimulatorEngine_createLog
+  (JNIEnv *env, jclass cls, jlong __pointer lexprPointer, jlong __pointer rexprPointer)
+{
+	CExpression * lexpr = (jlong_to_CExpression(lexprPointer));
+	CExpression * rexpr = (jlong_to_CExpression(rexprPointer));
+	CExpression * logExpr = new CLog(lexpr, rexpr);
+	return ptr_to_jlong(logExpr);
+}
+
 JNIEXPORT jlong __pointer JNICALL Java_simulator_SimulatorEngine_createNot
 (JNIEnv * env, jclass cls, jlong __pointer exprPointer)
 {