s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Utility methods in double vectors. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1677 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 16 years ago
parent
6a0f1b733c
commit
62880190eb
5 changed files with 191 additions and 27 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      prism/include/DoubleVector.h
  2. 17
      prism/include/dv.h
  3. 52
      prism/src/dv/DoubleVector.cc
  4. 55
      prism/src/dv/DoubleVector.java
  5. 78
      prism/src/dv/dv.cc

16
prism/include/DoubleVector.h
View File

@ -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

17
prism/include/dv.h
View File

@ -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

52
prism/src/dv/DoubleVector.cc
View File

@ -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,

55
prism/src/dv/DoubleVector.java
View File

@ -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)
{

78
prism/src/dv/dv.cc
View File

@ -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);
}
//------------------------------------------------------------------------------
Write Preview
Loading…
Cancel
Save