From 617137b27d0aa4cd80ddd727e2ac3d5167445750 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 16 Dec 2010 22:33:28 +0000 Subject: [PATCH] Fix: Time-bounded probs for CTMC are exactly 1 (no round-off) for target states. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2341 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/DoubleVector.h | 8 ++++++ prism/include/dv.h | 1 + prism/src/dv/DoubleVector.cc | 22 +++++++++++++++++ prism/src/dv/DoubleVector.java | 7 ++++++ prism/src/dv/dv.cc | 34 ++++++++++++++++++++++++++ prism/src/prism/StateValues.java | 1 + prism/src/prism/StateValuesDV.java | 7 ++++++ prism/src/prism/StateValuesMTBDD.java | 8 ++++++ prism/src/prism/StochModelChecker.java | 3 +++ 9 files changed, 91 insertions(+) diff --git a/prism/include/DoubleVector.h b/prism/include/DoubleVector.h index 8b692c1f..bb88d54d 100644 --- a/prism/include/DoubleVector.h +++ b/prism/include/DoubleVector.h @@ -87,6 +87,14 @@ JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1TimesConstant JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1Filter (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong); +/* + * Class: dv_DoubleVector + * Method: DV_MaxMTBDD + * Signature: (JJJIJ)V + */ +JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1MaxMTBDD + (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong); + /* * Class: dv_DoubleVector * Method: DV_Clear diff --git a/prism/include/dv.h b/prism/include/dv.h index df717943..b92dc6fd 100644 --- a/prism/include/dv.h +++ b/prism/include/dv.h @@ -73,6 +73,7 @@ EXPORT DdNode *double_vector_to_bdd(DdManager *ddman, double *vec, int rel_op, d 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 void max_double_vector_mtbdd(DdManager *ddman, double *vec, DdNode *vec2, 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); EXPORT double min_double_vector_over_bdd(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, ODDNode *odd); EXPORT double max_double_vector_over_bdd(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, ODDNode *odd); diff --git a/prism/src/dv/DoubleVector.cc b/prism/src/dv/DoubleVector.cc index 22bbc045..88f98dd9 100644 --- a/prism/src/dv/DoubleVector.cc +++ b/prism/src/dv/DoubleVector.cc @@ -234,6 +234,28 @@ jlong __jlongpointer odd //------------------------------------------------------------------------------ +JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1MaxMTBDD +( +JNIEnv *env, +jobject obj, +jlong __jlongpointer vector, +jlong __jlongpointer vector2, +jlong __jlongpointer vars, +jint num_vars, +jlong __jlongpointer odd +) +{ + max_double_vector_mtbdd( + ddman, + jlong_to_double(vector), + jlong_to_DdNode(vector2), + jlong_to_DdNode_array(vars), num_vars, + jlong_to_ODDNode(odd) + ); +} + +//------------------------------------------------------------------------------ + JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1Clear ( JNIEnv *env, diff --git a/prism/src/dv/DoubleVector.java b/prism/src/dv/DoubleVector.java index 93bad597..f0d216e2 100644 --- a/prism/src/dv/DoubleVector.java +++ b/prism/src/dv/DoubleVector.java @@ -152,6 +152,13 @@ public class DoubleVector { DV_Filter(v, filter.ptr(), vars.array(), vars.n(), odd.ptr()); } + + // apply max operator, i.e. v[i] = max(v[i], v2[i]), where v2 is an mtbdd + private native void DV_MaxMTBDD(long v, long v2, long vars, int num_vars, long odd); + public void maxMTBDD(JDDNode v2, JDDVars vars, ODDNode odd) + { + DV_MaxMTBDD(v, v2.ptr(), vars.array(), vars.n(), odd.ptr()); + } // clear (free memory) private native void DV_Clear(long v); diff --git a/prism/src/dv/dv.cc b/prism/src/dv/dv.cc index 859361cb..2e2c8d4b 100644 --- a/prism/src/dv/dv.cc +++ b/prism/src/dv/dv.cc @@ -35,6 +35,7 @@ static void mtbdd_to_double_vector_rec(DdManager *ddman, DdNode *dd, DdNode **va 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 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 void max_double_vector_mtbdd_rec(DdManager *ddman, double *vec, DdNode *vec2, 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); static double max_double_vector_over_bdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o); @@ -237,6 +238,39 @@ void filter_double_vector_rec(DdManager *ddman, double *vec, DdNode *filter, DdN //------------------------------------------------------------------------------ +// apply max operator, i.e. vec[i] = max(vec[i], vec2[i]), where vec2 is an mtbdd + +EXPORT void max_double_vector_mtbdd(DdManager *ddman, double *vec, DdNode *vec2, DdNode **vars, int num_vars, ODDNode *odd) +{ + max_double_vector_mtbdd_rec(ddman, vec, vec2, vars, num_vars, 0, odd, 0); +} + +void max_double_vector_mtbdd_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o) +{ + DdNode *dd; + double d; + + if (level == num_vars) { + + d = Cudd_V(filter); + if (d > vec[o]) { + vec[o] = d; + } + } + else { + if (odd->eoff > 0) { + dd = (filter->index > vars[level]->index) ? filter : Cudd_E(filter); + max_double_vector_mtbdd_rec(ddman, vec, dd, vars, num_vars, level+1, odd->e, o); + } + if (odd->toff > 0) { + dd = (filter->index > vars[level]->index) ? filter : Cudd_T(filter); + max_double_vector_mtbdd_rec(ddman, vec, dd, vars, num_vars, level+1, odd->t, o+odd->eoff); + } + } +} + +//------------------------------------------------------------------------------ + // get value of first element in BDD filter EXPORT double get_first_from_bdd(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, ODDNode *odd) diff --git a/prism/src/prism/StateValues.java b/prism/src/prism/StateValues.java index 12da0f1d..19889fa3 100644 --- a/prism/src/prism/StateValues.java +++ b/prism/src/prism/StateValues.java @@ -43,6 +43,7 @@ public interface StateValues void add(StateValues sp); void timesConstant(double d); void filter(JDDNode filter); + public void maxMTBDD(JDDNode vec2); void clear(); int getNNZ(); String getNNZString(); diff --git a/prism/src/prism/StateValuesDV.java b/prism/src/prism/StateValuesDV.java index d0ad6829..1151fa98 100644 --- a/prism/src/prism/StateValuesDV.java +++ b/prism/src/prism/StateValuesDV.java @@ -196,6 +196,13 @@ public class StateValuesDV implements StateValues values.filter(filter, vars, odd); } + // apply max operator, i.e. vec[i] = max(vec[i], vec2[i]), where vec2 is an mtbdd + + public void maxMTBDD(JDDNode vec2) + { + values.maxMTBDD(vec2, vars, odd); + } + // clear (free memory) public void clear() diff --git a/prism/src/prism/StateValuesMTBDD.java b/prism/src/prism/StateValuesMTBDD.java index c4b38fb8..dc58ce0d 100644 --- a/prism/src/prism/StateValuesMTBDD.java +++ b/prism/src/prism/StateValuesMTBDD.java @@ -212,6 +212,14 @@ public class StateValuesMTBDD implements StateValues values = JDD.Apply(JDD.TIMES, values, filter); } + // apply max operator, i.e. vec[i] = max(vec[i], vec2[i]), where vec2 is an mtbdd + + public void maxMTBDD(JDDNode vec2) + { + JDD.Ref(vec2); + values = JDD.Apply(JDD.MAX, values, vec2); + } + // clear public void clear() diff --git a/prism/src/prism/StochModelChecker.java b/prism/src/prism/StochModelChecker.java index a5cfb416..480aa8c6 100644 --- a/prism/src/prism/StochModelChecker.java +++ b/prism/src/prism/StochModelChecker.java @@ -196,6 +196,9 @@ public class StochModelChecker extends ProbModelChecker throw e; } JDD.Deref(tmp); + // set values to exactly 1 for target (b2) states + // (these are computed inexactly during uniformisation) + probs.maxMTBDD(b2); } // [lTime,uTime] (including where lTime == uTime) else {