diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java
index 08a32d3e..cb259c9a 100644
--- a/prism/src/jdd/JDD.java
+++ b/prism/src/jdd/JDD.java
@@ -954,6 +954,20 @@ public class JDD
return rv;
}
+ /**
+ * Returns the minimum terminal in the part of
+ * dd that overlaps with filter.
+ * If filter is empty, returns +infinity.
+ *
[ REFS: none, DEREFS: filter ]
+ */
+ public static double FindMinOver(JDDNode dd, JDDNode filter)
+ {
+ JDDNode filtered = JDD.ITE(filter, dd.copy(), JDD.PlusInfinity());
+ double rv = FindMin(filtered);
+ JDD.Deref(filtered);
+ return rv;
+ }
+
/**
* returns maximum terminal in dd
*
[ REFS: none, DEREFS: none ]
@@ -977,6 +991,20 @@ public class JDD
return rv;
}
+ /**
+ * Returns the maximum terminal in the part of
+ * dd that overlaps with filter.
+ * If filter is empty, returns -infinity.
+ *
[ REFS: none, DEREFS: filter ]
+ */
+ public static double FindMaxOver(JDDNode dd, JDDNode filter)
+ {
+ JDDNode filtered = JDD.ITE(filter, dd.copy(), JDD.MinusInfinity());
+ double rv = FindMax(filtered);
+ JDD.Deref(filtered);
+ return rv;
+ }
+
/**
* returns dd restricted to first non-zero path (cube)
*
[ REFS: result, DEREFS: dd ]