From 4cca315ef27c51b2887940dad908018de3f8ebcb Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Tue, 5 Jul 2016 10:34:24 +0000
Subject: [PATCH] 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     |  8 ++++++++
 prism/include/dd_term.h |  1 +
 prism/src/dd/dd_term.cc | 27 +++++++++++++++++++++++++++
 prism/src/jdd/JDD.cc    |  8 ++++++++
 prism/src/jdd/JDD.java  | 16 +++++++++++++++-
 5 files changed, 59 insertions(+), 1 deletion(-)

diff --git a/prism/include/JDD.h b/prism/include/JDD.h
index ef18ba45..064931f7 100644
--- a/prism/include/JDD.h
+++ b/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
diff --git a/prism/include/dd_term.h b/prism/include/dd_term.h
index 0f8561ad..c627ec3a 100644
--- a/prism/include/dd_term.h
+++ b/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);
diff --git a/prism/src/dd/dd_term.cc b/prism/src/dd/dd_term.cc
index 538c3663..24d3ec44 100644
--- a/prism/src/dd/dd_term.cc
+++ b/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,
diff --git a/prism/src/jdd/JDD.cc b/prism/src/jdd/JDD.cc
index afb6acba..53b9122c 100644
--- a/prism/src/jdd/JDD.cc
+++ b/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));
diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java
index ebfe9e75..4c42cd67 100644
--- a/prism/src/jdd/JDD.java
+++ b/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);
@@ -921,7 +922,20 @@ public class JDD
 		checkForCuddError();
 		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> ]