StateValues: new method filter(dd, double), sets values not in filter to d

Adapt DoubleVector to make value for filter user-definable.


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

prism/include/DoubleVector.h

@@ -98,10 +98,10 @@ JNIEXPORT jdouble JNICALL Java_dv_DoubleVector_DV_1DotProduct
 /*
  * Class:     dv_DoubleVector
  * Method:    DV_Filter
- * Signature: (JJJIJ)V
+ * Signature: (JJDJIJ)V
  */
 JNIEXPORT void JNICALL Java_dv_DoubleVector_DV_1Filter
-  (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+  (JNIEnv *, jobject, jlong, jlong, jdouble, jlong, jint, jlong);
 
 /*
  * Class:     dv_DoubleVector

prism/include/dv.h

@@ -72,7 +72,7 @@ EXPORT DdNode *double_vector_to_mtbdd(DdManager *ddman, double *vec, DdNode **va
 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 void filter_double_vector(DdManager *ddman, double *vec, DdNode *filter, double d, 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);

prism/src/dv/DoubleVector.cc

@@ -258,6 +258,7 @@ JNIEnv *env,
 jobject obj,
 jlong __jlongpointer vector,
 jlong __jlongpointer filter,
+jdouble d,
 jlong __jlongpointer vars,
 jint num_vars,
 jlong __jlongpointer odd
@@ -267,6 +268,7 @@ jlong __jlongpointer odd
 		ddman,
 		jlong_to_double(vector),
 		jlong_to_DdNode(filter),
+		d,
 		jlong_to_DdNode_array(vars), num_vars,
 		jlong_to_ODDNode(odd)
 	);

prism/src/dv/DoubleVector.java

@@ -199,11 +199,24 @@ public class DoubleVector
 		return DV_DotProduct(v, n, dv.v);
 	}
 
-	// filter vector using a bdd (set elements not in filter to 0)
-	private native void DV_Filter(long v, long filter, long vars, int num_vars, long odd);
+
+	private native void DV_Filter(long v, long filter, double d, long vars, int num_vars, long odd);
+	/**
+	 * Filter vector using a bdd (set elements not in filter to d)
+	 * <br>[ REFS: <i>result</i>, DEREFS: <i>none</i> ]
+	 */
+	public void filter(JDDNode filter, double d, JDDVars vars, ODDNode odd)
+	{
+		DV_Filter(v, filter.ptr(), d, vars.array(), vars.n(), odd.ptr());
+	}
+
+	/**
+	 * Filter vector using a bdd (set elements not in filter to 0)
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
 	public void filter(JDDNode filter, JDDVars vars, ODDNode odd)
 	{
-		DV_Filter(v, filter.ptr(), vars.array(), vars.n(), odd.ptr());
+		DV_Filter(v, filter.ptr(), 0.0, vars.array(), vars.n(), odd.ptr());
 	}
 	
 	// apply max operator, i.e. v[i] = max(v[i], v2[i]), where v2 is an mtbdd

prism/src/dv/dv.cc

@@ -34,7 +34,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 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 filter_double_vector_rec(DdManager *ddman, double *vec, DdNode *filter, double d, 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);
@@ -208,33 +208,33 @@ DdNode *double_vector_to_bdd_rec(DdManager *ddman, double *vec, int rel_op, doub
 
 //------------------------------------------------------------------------------
 
-// filter vector using a bdd (set elements not in filter to 0)
+// filter vector using a bdd (set elements not in filter to constant d)
 
-EXPORT void filter_double_vector(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, ODDNode *odd)
+EXPORT void filter_double_vector(DdManager *ddman, double *vec, DdNode *filter, double d, DdNode **vars, int num_vars, ODDNode *odd)
 {
-	filter_double_vector_rec(ddman, vec, filter, vars, num_vars, 0, odd, 0);
+	filter_double_vector_rec(ddman, vec, filter, d, vars, num_vars, 0, odd, 0);
 }
 
-void filter_double_vector_rec(DdManager *ddman, double *vec, DdNode *filter, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
+void filter_double_vector_rec(DdManager *ddman, double *vec, DdNode *filter, double d, DdNode **vars, int num_vars, int level, ODDNode *odd, long o)
 {
 	DdNode *dd;
 	
 	if (level == num_vars) {
 		if (Cudd_V(filter) == 0) {
-			vec[o] = 0;
+			vec[o] = d;
 		}
 	}
 	else {
 		if (odd->eoff > 0) {
 			dd = (filter->index > vars[level]->index) ? filter : Cudd_E(filter);
-			filter_double_vector_rec(ddman, vec, dd, vars, num_vars, level+1, odd->e, o);
+			filter_double_vector_rec(ddman, vec, dd, d, vars, num_vars, level+1, odd->e, o);
 		}
 		if (odd->toff > 0) {
 			dd = (filter->index > vars[level]->index) ? filter : Cudd_T(filter);
-			filter_double_vector_rec(ddman, vec, dd, vars, num_vars, level+1, odd->t, o+odd->eoff);
+			filter_double_vector_rec(ddman, vec, dd, d, vars, num_vars, level+1, odd->t, o+odd->eoff);
 		}
 	}
-}	
+}
 
 //------------------------------------------------------------------------------
 

prism/src/prism/StateValues.java

@@ -77,6 +77,12 @@ public interface StateValues extends StateVector
 	 */
 	void filter(JDDNode filter);
 
+	/**
+	 * Filter this vector using a BDD (set elements not in filter to constant {@code d}).
+	 * <br>[ DEREFS: <i>none</i> ]
+	 */
+	void filter(JDDNode filter, double d);
+
 	/**
 	 * Apply max operator, i.e. vec[i] = max(vec[i], vec2[i]), where vec2 is an MTBDD
 	 * <br>[ DEREFS: <i>none</i> ]

prism/src/prism/StateValuesDV.java

@@ -233,6 +233,12 @@ public class StateValuesDV implements StateValues
 		values.filter(filter, vars, odd);
 	}
 
+	@Override
+	public void filter(JDDNode filter, double d)
+	{
+		values.filter(filter, d, vars, odd);
+	}
+
 	@Override
 	public void maxMTBDD(JDDNode vec2)
 	{

prism/src/prism/StateValuesMTBDD.java

@@ -246,7 +246,15 @@ public class StateValuesMTBDD implements StateValues
 		JDD.Ref(filter);
 		values = JDD.Apply(JDD.TIMES, values, filter);
 	}
-	
+
+	@Override
+	public void filter(JDDNode filter, double d)
+	{
+		// If filter, then keep value, else constant d,
+		// but only for the reachable states
+		values = JDD.Times(reach.copy(), JDD.ITE(filter.copy(), values, JDD.Constant(d)));
+	}
+
 	@Override
 	public void maxMTBDD(JDDNode vec2)
 	{

prism/src/prism/StateValuesVoid.java

@@ -125,6 +125,12 @@ public class StateValuesVoid implements StateValues
 		throw new UnsupportedOperationException();
 	}
 
+	@Override
+	public void filter(JDDNode filter, double d)
+	{
+		throw new UnsupportedOperationException();
+	}
+
 	@Override
 	public void maxMTBDD(JDDNode vec2)
 	{