Add JDD.FindMinPositive (minimal positive terminal constant of an MTBDD)

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

prism/include/JDD.h

@@ -439,6 +439,14 @@ JNIEXPORT jboolean JNICALL Java_jdd_JDD_DD_1EqualSupNorm
 JNIEXPORT jdouble JNICALL Java_jdd_JDD_DD_1FindMin
   (JNIEnv *, jclass, jlong);
 
+/*
+ * Class:     jdd_JDD
+ * Method:    DD_FindMinPositive
+ * Signature: (J)D
+ */
+JNIEXPORT jdouble JNICALL Java_jdd_JDD_DD_1FindMinPositive
+  (JNIEnv *, jclass, jlong);
+
 /*
  * Class:     jdd_JDD
  * Method:    DD_FindMax

prism/include/dd_term.h

@@ -41,6 +41,7 @@ DdNode *DD_RoundOff(DdManager *ddman, DdNode *dd, int places);
 bool DD_EqualSupNorm(DdManager *ddman, DdNode *dd1, DdNode *dd2, double epsilon);
 bool DD_EqualSupNormRel(DdManager *ddman, DdNode *dd1, DdNode *dd2, double epsilon);
 double DD_FindMin(DdManager *ddman, DdNode *dd);
+double DD_FindMinPositive(DdManager *ddman, DdNode *dd);
 double DD_FindMax(DdManager *ddman, DdNode *dd);
 DdNode *DD_RestrictToFirst(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars);
 bool DD_IsZeroOneMTBDD(DdManager *ddman, DdNode *dd);

prism/src/dd/dd_term.cc

@@ -250,6 +250,33 @@ DdNode *dd
 
 //------------------------------------------------------------------------------
 
+// Find minimal terminal node (constant) that is greater than zero
+double DD_FindMinPositive
+(
+DdManager *ddman,
+DdNode *dd
+)
+{
+	DdGen *gen;
+	DdNode *node;
+	bool rv = true;
+
+	double min_v = std::numeric_limits<double>::infinity();
+
+	Cudd_ForeachNode(ddman, dd, gen, node) {
+		if (Cudd_IsConstant(node)) {
+			double v = Cudd_V(node);
+			if (v > 0 && v < min_v) {
+				min_v = v;
+			}
+		}
+	}
+
+	return min_v;
+}
+
+//------------------------------------------------------------------------------
+
 double DD_FindMax
 (
 DdManager *ddman,

prism/src/jdd/JDD.cc

@@ -426,6 +426,14 @@ JNIEXPORT jdouble JNICALL Java_jdd_JDD_DD_1FindMin(JNIEnv *env, jclass cls, jlon
 //------------------------------------------------------------------------------
 
 
+JNIEXPORT jdouble JNICALL Java_jdd_JDD_DD_1FindMinPositive(JNIEnv *env, jclass cls, jlong __jlongpointer dd)
+{
+	return DD_FindMinPositive(ddman, jlong_to_DdNode(dd));
+}
+
+//------------------------------------------------------------------------------
+
+
 JNIEXPORT jdouble JNICALL Java_jdd_JDD_DD_1FindMax(JNIEnv *env, jclass cls, jlong __jlongpointer dd)
 {
 	return DD_FindMax(ddman, jlong_to_DdNode(dd));

prism/src/jdd/JDD.java

@@ -89,6 +89,7 @@ public class JDD
 	private static native long DD_RoundOff(long dd, int places);
 	private static native boolean DD_EqualSupNorm(long dd1, long dd2, double epsilon);
 	private static native double DD_FindMin(long dd);
+	private static native double DD_FindMinPositive(long dd);
 	private static native double DD_FindMax(long dd);
 	private static native long DD_RestrictToFirst(long dd, long vars, int num_vars);
 	private static native boolean DD_IsZeroOneMTBDD(long dd);
@@ -922,6 +923,19 @@ public class JDD
 		return rv;
 	}
 
+	/**
+	 * Returns minimal positive terminal in dd, i.e.,
+	 * the smallest constant greater than zero.
+	 * If there is none, returns +infinity.
+	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]
+	 */
+	public static double FindMinPositive(JDDNode dd)
+	{
+		double rv = DD_FindMinPositive(dd.ptr());
+		checkForCuddError();
+		return rv;
+	}
+
 	/**
 	 * returns maximum terminal in dd
 	 * <br>[ REFS: <i>none</i>, DEREFS: <i>none</i> ]