diff --git a/prism/include/odd.h b/prism/include/odd.h index c7c8f2f6..2af55eed 100644 --- a/prism/include/odd.h +++ b/prism/include/odd.h @@ -29,6 +29,8 @@ //------------------------------------------------------------------------------ +#include + #include #include #include @@ -51,8 +53,8 @@ struct ODDNode ODDNode *next; ODDNode *e; ODDNode *t; - long eoff; - long toff; + int64_t eoff; + int64_t toff; }; // function prototypes diff --git a/prism/src/odd/ODDUtils.java b/prism/src/odd/ODDUtils.java index c209c881..5fdbad7d 100644 --- a/prism/src/odd/ODDUtils.java +++ b/prism/src/odd/ODDUtils.java @@ -27,6 +27,7 @@ package odd; import jdd.*; +import prism.PrismException; public class ODDUtils { @@ -65,17 +66,20 @@ 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 */ - public static ODDNode BuildODD(JDDNode dd, JDDVars vars) + public static ODDNode BuildODD(JDDNode dd, JDDVars vars) throws PrismException { if (jdd.SanityJDD.enabled) { // ODD construction requires the JDDVars to be in ascending order jdd.SanityJDD.checkVarsAreSorted(vars); } - return new ODDNode( - ODD_BuildODD(dd.ptr(), vars.array(), vars.n()) - ); + 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"); + } + return new ODDNode(res); } private static native void ODD_ClearODD(long ptr); diff --git a/prism/src/odd/odd.cc b/prism/src/odd/odd.cc index 9efea586..bd530756 100644 --- a/prism/src/odd/odd.cc +++ b/prism/src/odd/odd.cc @@ -32,7 +32,7 @@ static int num_odd_nodes = 0; // local prototypes static ODDNode *build_odd_rec(DdManager *ddman, DdNode *dd, int level, DdNode **vars, int num_vars, ODDNode **tables); -static long add_offsets(DdManager *ddman, ODDNode *dd, int level, int num_vars); +static int64_t add_offsets(DdManager *ddman, ODDNode *dd, int level, int num_vars); static DdNode *single_index_to_bdd_rec(DdManager *ddman, int i, DdNode **vars, int num_vars, int level, ODDNode *odd, long o); //------------------------------------------------------------------------------ @@ -82,7 +82,12 @@ ODDNode *build_odd(DdManager *ddman, DdNode *dd, DdNode **vars, int num_vars) } // add offsets to odd - add_offsets(ddman, res, 0, num_vars); + if (add_offsets(ddman, res, 0, num_vars) < 0) { + // negative value indicates that there was an arithmetic overflow + // cleanup and return 0 + clear_odd(res); + res = 0; + } // free memory delete tables; @@ -138,9 +143,14 @@ static ODDNode *build_odd_rec(DdManager *ddman, DdNode *dd, int level, DdNode ** //------------------------------------------------------------------------------ -long add_offsets(DdManager *ddman, ODDNode *odd, int level, int num_vars) +// +// Compute the actual eoff and toff values. +// Returns eoff + toff for this odd node or -1 if there is an arithmetic overflow +// (can not store eoff+toff in an int64_t) +int64_t add_offsets(DdManager *ddman, ODDNode *odd, int level, int num_vars) { if ((odd->eoff == -1) || (odd->toff == -1)) { + // this node has not yet been seen if (level == num_vars) { if (odd->dd == Cudd_ReadZero(ddman)) { odd->eoff = 0; @@ -153,10 +163,22 @@ long add_offsets(DdManager *ddman, ODDNode *odd, int level, int num_vars) } else { odd->eoff = add_offsets(ddman, odd->e, level+1, num_vars); + if (odd->eoff < 0) return -1; odd->toff = add_offsets(ddman, odd->t, level+1, num_vars); + if (odd->toff < 0) return -1; + } + + // overflow check for sum + // do unsigned addition, guaranteed to not overflow + // as eoff and toff are signed and positive, cast sum to signed and + // check that it is larger than one of the summands + int64_t tmp = (int64_t)((uint64_t)odd->eoff + (uint64_t)odd->toff); + if (tmp < odd->eoff) { + // we have an overflow + return -1; } } - + return odd->eoff + odd->toff; } diff --git a/prism/src/prism/Model.java b/prism/src/prism/Model.java index da47dad8..98b0fb00 100644 --- a/prism/src/prism/Model.java +++ b/prism/src/prism/Model.java @@ -164,9 +164,9 @@ public interface Model void resetTrans(JDDNode trans); void resetTransRewards(int i, JDDNode transRewards); - void doReachability(); - void skipReachability(); - void setReach(JDDNode reach); + void doReachability() throws PrismException; + void skipReachability() throws PrismException; + void setReach(JDDNode reach) throws PrismException; void setTransActions(JDDNode transActions); // MDPs only void setTransPerAction(JDDNode[] transPerAction); // D/CTMCs only void filterReachableStates(); diff --git a/prism/src/prism/NondetModel.java b/prism/src/prism/NondetModel.java index f3ac6d23..46715248 100644 --- a/prism/src/prism/NondetModel.java +++ b/prism/src/prism/NondetModel.java @@ -202,7 +202,7 @@ public class NondetModel extends ProbModel // do reachability - public void doReachability() + public void doReachability() throws PrismException { JDDNode tmp; @@ -227,7 +227,7 @@ public class NondetModel extends ProbModel *
[ REFS: result, DEREFS: seed ] * @param seed set of states (over ddRowVars) that is known to be reachable */ - public void doReachability(JDDNode seed) + public void doReachability(JDDNode seed) throws PrismException { JDDNode tmp; diff --git a/prism/src/prism/ProbModel.java b/prism/src/prism/ProbModel.java index 2f608030..7843fb1e 100644 --- a/prism/src/prism/ProbModel.java +++ b/prism/src/prism/ProbModel.java @@ -567,7 +567,7 @@ public class ProbModel implements Model // do reachability - public void doReachability() + public void doReachability() throws PrismException { // compute reachable states setReach(PrismMTBDD.Reachability(trans01, allDDRowVars, allDDColVars, start)); @@ -581,7 +581,7 @@ public class ProbModel implements Model *
[ REFS: result, DEREFS: seed ] * @param seed set of states (over ddRowVars) that is known to be reachable */ - public void doReachability(JDDNode seed) + public void doReachability(JDDNode seed) throws PrismException { // do sanity check on seed if checking is enabled if (SanityJDD.enabled) @@ -597,7 +597,7 @@ public class ProbModel implements Model // this method allows you to skip the reachability phase // it is only here for experimental purposes - not general use. - public void skipReachability() + public void skipReachability() throws PrismException { // don't compute reachable states - assume all reachable reach = JDD.Constant(1); @@ -608,6 +608,7 @@ public class ProbModel implements Model // build odd, clear old one if (odd != null) { ODDUtils.ClearODD(odd); + odd = null; } odd = ODDUtils.BuildODD(reach, allDDRowVars); } @@ -616,7 +617,7 @@ public class ProbModel implements Model * Set reachable states BDD (and compute number of states and ODD) */ - public void setReach(JDDNode reach) + public void setReach(JDDNode reach) throws PrismException { if (this.reach != null) JDD.Deref(this.reach); @@ -628,6 +629,7 @@ public class ProbModel implements Model // build odd, clear old one if (odd != null) { ODDUtils.ClearODD(odd); + odd = null; } odd = ODDUtils.BuildODD(reach, allDDRowVars); }