From 62880190ebffe7c202109c34345be7a950a01a51 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 7 Jan 2010 21:25:51 +0000 Subject: [PATCH] Utility methods in double vectors. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1677 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/DoubleVector.h | 16 +++++++ prism/include/dv.h | 17 +++++--- prism/src/dv/DoubleVector.cc | 52 +++++++++++++++++++++++ prism/src/dv/DoubleVector.java | 55 +++++++++++++++++++++--- prism/src/dv/dv.cc | 78 ++++++++++++++++++++++++++++------ 5 files changed, 191 insertions(+), 27 deletions(-) diff --git a/prism/include/DoubleVector.h b/prism/include/DoubleVector.h index 15e87aee..8b692c1f 100644 --- a/prism/include/DoubleVector.h +++ b/prism/include/DoubleVector.h @@ -191,6 +191,22 @@ JNIEXPORT jlong JNICALL Java_dv_DoubleVector_DV_1BDDLessThan JNIEXPORT jlong JNICALL Java_dv_DoubleVector_DV_1BDDInterval (JNIEnv *, jobject, jlong, jdouble, jdouble, jlong, jint, jlong); +/* + * Class: dv_DoubleVector + * Method: DV_BDDCloseValueAbs + * Signature: (JDDJIJ)J + */ +JNIEXPORT jlong JNICALL Java_dv_DoubleVector_DV_1BDDCloseValueAbs + (JNIEnv *, jobject, jlong, jdouble, jdouble, jlong, jint, jlong); + +/* + * Class: dv_DoubleVector + * Method: DV_BDDCloseValueRel + * Signature: (JDDJIJ)J + */ +JNIEXPORT jlong JNICALL Java_dv_DoubleVector_DV_1BDDCloseValueRel + (JNIEnv *, jobject, jlong, jdouble, jdouble, jlong, jint, jlong); + /* * Class: dv_DoubleVector * Method: DV_ConvertToMTBDD diff --git a/prism/include/dv.h b/prism/include/dv.h index 661e132c..df717943 100644 --- a/prism/include/dv.h +++ b/prism/include/dv.h @@ -43,10 +43,12 @@ // constants #define DV_GREATER_THAN_EQUALS 1 -#define DV_GREATER_THAN 2 -#define DV_LESS_THAN_EQUALS 3 -#define DV_LESS_THAN 4 -#define DV_INTERVAL 5 +#define DV_GREATER_THAN 2 +#define DV_LESS_THAN_EQUALS 3 +#define DV_LESS_THAN 4 +#define DV_INTERVAL 5 +#define DV_CLOSE_ABS 6 +#define DV_CLOSE_REL 7 // distinct vectors @@ -67,8 +69,8 @@ struct DistVector EXPORT double *mtbdd_to_double_vector(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd); EXPORT double *mtbdd_to_double_vector(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, ODDNode *odd, double *res); EXPORT DdNode *double_vector_to_mtbdd(DdManager *ddman, double *vec, DdNode **vars, int num_vars, ODDNode *odd); -EXPORT DdNode *double_vector_to_bdd(DdManager *ddman, double *vec, int rel_op, double bound, DdNode **vars, int num_vars, ODDNode *odd); -EXPORT DdNode *double_vector_to_bdd(DdManager *ddman, double *vec, int rel_op, double bound1, double bound2, DdNode **vars, int num_vars, ODDNode *odd); +EXPORT DdNode *double_vector_to_bdd(DdManager *ddman, double *vec, int rel_op, double value, DdNode **vars, int num_vars, ODDNode *odd); +EXPORT DdNode *double_vector_to_bdd(DdManager *ddman, double *vec, int rel_op, double value1, double value2, DdNode **vars, int num_vars, ODDNode *odd); EXPORT void filter_double_vector(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, ODDNode *odd); EXPORT double get_first_from_bdd(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, ODDNode *odd); @@ -80,6 +82,9 @@ EXPORT void sum_double_vector_over_dd_vars(DdManager *ddman, double *vec, double EXPORT DistVector *double_vector_to_dist(double *v, int n); +EXPORT bool doubles_are_close_abs(double d1, double d2, double epsilon); +EXPORT bool doubles_are_close_rel(double d1, double d2, double epsilon); + //------------------------------------------------------------------------------ #endif diff --git a/prism/src/dv/DoubleVector.cc b/prism/src/dv/DoubleVector.cc index 990926cc..22bbc045 100644 --- a/prism/src/dv/DoubleVector.cc +++ b/prism/src/dv/DoubleVector.cc @@ -531,6 +531,58 @@ jlong __jlongpointer odd //------------------------------------------------------------------------------ +JNIEXPORT jlong __jlongpointer JNICALL Java_dv_DoubleVector_DV_1BDDCloseValueAbs +( +JNIEnv *env, +jobject obj, +jlong __jlongpointer vector, +jdouble value, +jdouble epsilon, +jlong __jlongpointer vars, +jint num_vars, +jlong __jlongpointer odd +) +{ + return ptr_to_jlong( + double_vector_to_bdd( + ddman, + jlong_to_double(vector), + DV_CLOSE_ABS, + value, epsilon, + jlong_to_DdNode_array(vars), num_vars, + jlong_to_ODDNode(odd) + ) + ); +} + +//------------------------------------------------------------------------------ + +JNIEXPORT jlong __jlongpointer JNICALL Java_dv_DoubleVector_DV_1BDDCloseValueRel +( +JNIEnv *env, +jobject obj, +jlong __jlongpointer vector, +jdouble value, +jdouble epsilon, +jlong __jlongpointer vars, +jint num_vars, +jlong __jlongpointer odd +) +{ + return ptr_to_jlong( + double_vector_to_bdd( + ddman, + jlong_to_double(vector), + DV_CLOSE_REL, + value, epsilon, + jlong_to_DdNode_array(vars), num_vars, + jlong_to_ODDNode(odd) + ) + ); +} + +//------------------------------------------------------------------------------ + JNIEXPORT jlong __jlongpointer JNICALL Java_dv_DoubleVector_DV_1ConvertToMTBDD ( JNIEnv *env, diff --git a/prism/src/dv/DoubleVector.java b/prism/src/dv/DoubleVector.java index 54a9a457..93bad597 100644 --- a/prism/src/dv/DoubleVector.java +++ b/prism/src/dv/DoubleVector.java @@ -215,11 +215,10 @@ public class DoubleVector return dv2; } - // generate bdd (from an interval: relative operator and bound) - private native long DV_BDDGreaterThanEquals(long v, double bound, long vars, int num_vars, long odd); - private native long DV_BDDGreaterThan(long v, double bound, long vars, int num_vars, long odd); - private native long DV_BDDLessThanEquals(long v, double bound, long vars, int num_vars, long odd); - private native long DV_BDDLessThan(long v, double bound, long vars, int num_vars, long odd); + /** + * Generate BDD for states in the given interval + * (interval specified as relational operator and bound) + */ public JDDNode getBDDFromInterval(String relOp, double bound, JDDVars vars, ODDNode odd) { JDDNode sol = null; @@ -247,9 +246,15 @@ public class DoubleVector return sol; } + private native long DV_BDDGreaterThanEquals(long v, double bound, long vars, int num_vars, long odd); + private native long DV_BDDGreaterThan(long v, double bound, long vars, int num_vars, long odd); + private native long DV_BDDLessThanEquals(long v, double bound, long vars, int num_vars, long odd); + private native long DV_BDDLessThan(long v, double bound, long vars, int num_vars, long odd); - // generate bdd (from an interval: lower/upper bound) - private native long DV_BDDInterval(long v, double lo, double hi, long vars, int num_vars, long odd); + /** + * Generate BDD for states in the given interval + * (interval specified as lower/upper bound) + */ public JDDNode getBDDFromInterval(double lo, double hi, JDDVars vars, ODDNode odd) { JDDNode sol; @@ -260,7 +265,43 @@ public class DoubleVector return sol; } + private native long DV_BDDInterval(long v, double lo, double hi, long vars, int num_vars, long odd); + + /** + * Generate BDD for states whose value is close to 'value' + * (within absolute error 'epsilon') + */ + public JDDNode getBDDFromCloseValueAbs(double value, double epsilon, JDDVars vars, ODDNode odd) + { + JDDNode sol; + + sol = new JDDNode( + DV_BDDCloseValueAbs(v, value, epsilon, vars.array(), vars.n(), odd.ptr()) + ); + + return sol; + } + private native long DV_BDDCloseValueAbs(long v, double value, double epsilon, long vars, int num_vars, long odd); + + /** + * Generate BDD for states whose value is close to 'value' + * (within relative error 'epsilon') + */ + public JDDNode getBDDFromCloseValueRel(double value, double epsilon, JDDVars vars, ODDNode odd) + { + JDDNode sol; + + sol = new JDDNode( + DV_BDDCloseValueRel(v, value, epsilon, vars.array(), vars.n(), odd.ptr()) + ); + + return sol; + } + private native long DV_BDDCloseValueRel(long v, double value, double epsilon, long vars, int num_vars, long odd); + /** + * Convert to an MTBDD representation. + */ private native long DV_ConvertToMTBDD(long v, long vars, int num_vars, long odd); public JDDNode convertToMTBDD(JDDVars vars, ODDNode odd) { diff --git a/prism/src/dv/dv.cc b/prism/src/dv/dv.cc index 46136719..859361cb 100644 --- a/prism/src/dv/dv.cc +++ b/prism/src/dv/dv.cc @@ -33,7 +33,7 @@ static void mtbdd_to_double_vector_rec(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars, int level, ODDNode *odd, long o, double *res); static DdNode *double_vector_to_mtbdd_rec(DdManager *ddman, double *vec, DdNode **vars, int num_vars, int level, ODDNode *odd, long o); -static DdNode *double_vector_to_bdd_rec(DdManager *ddman, double *vec, int rel_op, double bound1, double bound2, DdNode **vars, int num_vars, int level, ODDNode *odd, long o); +static DdNode *double_vector_to_bdd_rec(DdManager *ddman, double *vec, int rel_op, double value1, double value2, DdNode **vars, int num_vars, int level, ODDNode *odd, long o); static void filter_double_vector_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o); static double get_first_from_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o); static double min_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o); @@ -42,6 +42,9 @@ static double sum_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNo static double sum_double_vector_over_mtbdd_rec(DdManager *ddman, double *vec, DdNode *mult, DdNode **vars, int num_vars, int level, ODDNode *odd, long o); static void sum_double_vector_over_dd_vars_rec(DdManager *ddman, double *vec, double *vec2, DdNode **vars, int num_vars, int level, int first_var, int last_var, ODDNode *odd, ODDNode *odd2, long o, long o2); +// Threshold for comparison of doubles +static double epsilon_double = 1e-12; + //------------------------------------------------------------------------------ // converts an mtbdd representing a vector to an array of doubles @@ -138,40 +141,53 @@ DdNode *double_vector_to_mtbdd_rec(DdManager *ddman, double *vec, DdNode **vars, //------------------------------------------------------------------------------ -// converts an array of doubles to a bdd using a relational operator and one or more bounds +// Converts an array of doubles to a BDD using a relational operator and a value (or values) +// Options for rel_op: +// * DV_GREATER_THAN_EQUALS: >= value +// * DV_GREATER_THAN: > value +// * DV_LESS_THAN_EQUALS <= value +// * DV_LESS_THAN: < value +// * DV_INTERVAL: in [value1,value2] +// * DV_CLOSE_ABS: =value1 (with absolute error <= value2) +// * DV_CLOSE_REL: =value1 (with relative error <= value2) + -EXPORT DdNode *double_vector_to_bdd(DdManager *ddman, double *vec, int rel_op, double bound, DdNode **vars, int num_vars, ODDNode *odd) +EXPORT DdNode *double_vector_to_bdd(DdManager *ddman, double *vec, int rel_op, double value, DdNode **vars, int num_vars, ODDNode *odd) { - return double_vector_to_bdd(ddman, vec, rel_op, bound, 0, vars, num_vars, odd); + return double_vector_to_bdd(ddman, vec, rel_op, value, 0, vars, num_vars, odd); } -EXPORT DdNode *double_vector_to_bdd(DdManager *ddman, double *vec, int rel_op, double bound1, double bound2, DdNode **vars, int num_vars, ODDNode *odd) +EXPORT DdNode *double_vector_to_bdd(DdManager *ddman, double *vec, int rel_op, double value1, double value2, DdNode **vars, int num_vars, ODDNode *odd) { - return double_vector_to_bdd_rec(ddman, vec, rel_op, bound1, bound2, vars, num_vars, 0, odd, 0); + return double_vector_to_bdd_rec(ddman, vec, rel_op, value1, value2, vars, num_vars, 0, odd, 0); } -DdNode *double_vector_to_bdd_rec(DdManager *ddman, double *vec, int rel_op, double bound1, double bound2, DdNode **vars, int num_vars, int level, ODDNode *odd, long o) +// Recursive call for double_vector_to_bdd methods + +DdNode *double_vector_to_bdd_rec(DdManager *ddman, double *vec, int rel_op, double value1, double value2, DdNode **vars, int num_vars, int level, ODDNode *odd, long o) { DdNode *e, *t; if (level == num_vars) { switch (rel_op) { - case DV_GREATER_THAN_EQUALS: return (vec[o] >= bound1) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; - case DV_GREATER_THAN: return (vec[o] > bound1) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; - case DV_LESS_THAN_EQUALS: return (vec[o] <= bound1) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; - case DV_LESS_THAN: return (vec[o] < bound1) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; - case DV_INTERVAL: return (vec[o] >= bound1 && vec[o] <= bound2) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; + case DV_GREATER_THAN_EQUALS: return (vec[o] >= value1) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; + case DV_GREATER_THAN: return (vec[o] > value1) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; + case DV_LESS_THAN_EQUALS: return (vec[o] <= value1) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; + case DV_LESS_THAN: return (vec[o] < value1) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; + case DV_INTERVAL: return (vec[o] >= value1 && vec[o] <= value2) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; + case DV_CLOSE_ABS: return doubles_are_close_abs(vec[o], value1, value2) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; + case DV_CLOSE_REL: return doubles_are_close_rel(vec[o], value1, value2) ? DD_Constant(ddman, 1) : DD_Constant(ddman, 0); break; } } else { if (odd->eoff > 0) { - e = double_vector_to_bdd_rec(ddman, vec, rel_op, bound1, bound2, vars, num_vars, level+1, odd->e, o); + e = double_vector_to_bdd_rec(ddman, vec, rel_op, value1, value2, vars, num_vars, level+1, odd->e, o); } else { e = DD_Constant(ddman, 0); } if (odd->toff > 0) { - t = double_vector_to_bdd_rec(ddman, vec, rel_op, bound1, bound2, vars, num_vars, level+1, odd->t, o+odd->eoff); + t = double_vector_to_bdd_rec(ddman, vec, rel_op, value1, value2, vars, num_vars, level+1, odd->t, o+odd->eoff); } else { t = DD_Constant(ddman, 0); @@ -517,3 +533,37 @@ EXPORT DistVector::~DistVector() //------------------------------------------------------------------------------ +// Utililty methods for checking whether two doubles are close +// (based on code in prism.PrismUtils.java) + +EXPORT bool doubles_are_close_abs(double d1, double d2, double epsilon) +{ + // Deal with infinite cases + if (isinf(d1)) { + return isinf(d2) && (d1 > 0) == (d2 > 0); + } else if (isinf(d2)) { + return false; + } + // Compute/check error + return (fabs(d1 - d2) < epsilon); +} + +EXPORT bool doubles_are_close_rel(double d1, double d2, double epsilon) +{ + // Deal with infinite cases + if (isinf(d1)) { + return isinf(d2) && (d1 > 0) == (d2 > 0); + } else if (isinf(d2)) { + return false; + } + // Compute/check error + d1 = fabs(d1); + d2 = fabs(d2); + // For two (near) zero values, return true, for just one, return false + if (d1 < epsilon_double) + return (d2 < epsilon_double); + return (fabs(d1 - d2) / d1 < epsilon); +} + +//------------------------------------------------------------------------------ +