diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java
index 2e080f89..07bbd60e 100644
--- a/prism/src/jdd/JDD.java
+++ b/prism/src/jdd/JDD.java
@@ -433,7 +433,25 @@ public class JDD
}
return ptrToNode(DD_Apply(op, dd1.ptr(), dd2.ptr()));
}
-
+
+ /**
+ * Multi-operand Apply(JDD.TIMES) (multiplication) operation.
+ * Operands are processed from left-to-right.
+ *
[ REFS: result, DEREFS: all arguments ]
+ */
+ public static JDDNode Times(JDDNode... nodes) {
+ if (nodes.length <= 1) {
+ throw new IllegalArgumentException("JDD.Times needs at least two arguments.");
+ }
+
+ JDDNode result = nodes[0];
+ for (int i = 1; i[ REFS: result, DEREFS: dd ]