From 738b806fd2732b565acbafde33827b7374ef4e61 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 26 Feb 2008 15:02:21 +0000 Subject: [PATCH] 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 | 2 + prism/include/SimulatorEngine.h | 8 ++ prism/include/dd_basics.h | 1 + prism/include/simengine.h | 2 + prism/include/simexpression.h | 19 +++ prism/src/dd/dd_basics.cc | 1 + prism/src/jdd/JDD.java | 1 + prism/src/parser/ExpressionFunc.java | 2 +- prism/src/prism/Expression2MTBDD.java | 13 ++- prism/src/prism/PrismUtils.java | 4 +- prism/src/simulator/SimulatorEngine.java | 5 + prism/src/simulator/networking/NOTES | 2 + prism/src/simulator/simengine.cc | 5 + prism/src/simulator/simexpression.cc | 121 ++++++++++++++++++++ prism/src/simulator/simexpressionbuilder.cc | 9 ++ 15 files changed, 191 insertions(+), 4 deletions(-) diff --git a/prism/include/JDD.h b/prism/include/JDD.h index ebdb10a3..728711d2 100644 --- a/prism/include/JDD.h +++ b/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 diff --git a/prism/include/SimulatorEngine.h b/prism/include/SimulatorEngine.h index f37945c1..bacbef53 100644 --- a/prism/include/SimulatorEngine.h +++ b/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 diff --git a/prism/include/dd_basics.h b/prism/include/dd_basics.h index c5c26f24..e1da863d 100644 --- a/prism/include/dd_basics.h +++ b/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 //------------------------------------------------------------------------------ diff --git a/prism/include/simengine.h b/prism/include/simengine.h index 4c2b3582..647faff9 100644 --- a/prism/include/simengine.h +++ b/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); diff --git a/prism/include/simexpression.h b/prism/include/simexpression.h index b1ae4745..8944be10 100644 --- a/prism/include/simexpression.h +++ b/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: diff --git a/prism/src/dd/dd_basics.cc b/prism/src/dd/dd_basics.cc index 4b990a65..96cd013b 100644 --- a/prism/src/dd/dd_basics.cc +++ b/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); diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index 6b00b866..83d439e8 100644 --- a/prism/src/jdd/JDD.java +++ b/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; diff --git a/prism/src/parser/ExpressionFunc.java b/prism/src/parser/ExpressionFunc.java index 0e71356e..75aa1bfe 100644 --- a/prism/src/parser/ExpressionFunc.java +++ b/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: diff --git a/prism/src/prism/Expression2MTBDD.java b/prism/src/prism/Expression2MTBDD.java index d859d63c..72331a25 100644 --- a/prism/src/prism/Expression2MTBDD.java +++ b/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 diff --git a/prism/src/prism/PrismUtils.java b/prism/src/prism/PrismUtils.java index efd0737d..7b909cbb 100644 --- a/prism/src/prism/PrismUtils.java +++ b/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); diff --git a/prism/src/simulator/SimulatorEngine.java b/prism/src/simulator/SimulatorEngine.java index bd98788c..a2b30355 100644 --- a/prism/src/simulator/SimulatorEngine.java +++ 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) */ diff --git a/prism/src/simulator/networking/NOTES b/prism/src/simulator/networking/NOTES index c3b18ccf..05fc534a 100644 --- a/prism/src/simulator/networking/NOTES +++ b/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 diff --git a/prism/src/simulator/simengine.cc b/prism/src/simulator/simengine.cc index d531862a..0eeef4dc 100644 --- a/prism/src/simulator/simengine.cc +++ b/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); diff --git a/prism/src/simulator/simexpression.cc b/prism/src/simulator/simexpression.cc index bf4fc975..0aee9057 100644 --- a/prism/src/simulator/simexpression.cc +++ b/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); diff --git a/prism/src/simulator/simexpressionbuilder.cc b/prism/src/simulator/simexpressionbuilder.cc index 84110f7a..8d874513 100644 --- a/prism/src/simulator/simexpressionbuilder.cc +++ b/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) {