From ccbd11118deb55def53398b5dc322674018d7932 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 23 Apr 2019 21:44:31 +0200 Subject: [PATCH] ODD creation: Return null instead of exception on overflow After the previous changes, we are now ready to do MTBDD model checking even if we can't create the ODD (number of reachable states too large to fit into an int64_t). --- prism/src/odd/ODDUtils.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/prism/src/odd/ODDUtils.java b/prism/src/odd/ODDUtils.java index 514da635..c56fcd66 100644 --- a/prism/src/odd/ODDUtils.java +++ b/prism/src/odd/ODDUtils.java @@ -67,7 +67,7 @@ public class ODDUtils private static native long ODD_BuildODD(long dd, long vars, int num_vars); /** * Build an ODD. - * @throws PrismException if the ODD could not be constructed + * If the ODD could not be constructed, returns {@code null}. */ public static ODDNode BuildODD(JDDNode dd, JDDVars vars) throws PrismException { @@ -78,7 +78,9 @@ public class ODDUtils long res = ODD_BuildODD(dd.ptr(), vars.array(), vars.n()); if (res == 0) { - throw new PrismException("Can not construct ODD for this model, number of states too large: " + JDD.GetNumMintermsString(dd, vars.n()) + " states"); + // we could not build the ODD (i.e., we had more than Long.MAX_LONG states + // we return null and will have to live with the limited functionality + return null; } return new ODDNode(res); }