diff --git a/prism/src/dv/IntegerVector.java b/prism/src/dv/IntegerVector.java index ce96d571..65246169 100644 --- a/prism/src/dv/IntegerVector.java +++ b/prism/src/dv/IntegerVector.java @@ -89,11 +89,17 @@ public class IntegerVector /** * Create a new IntegerVector from an existing MTBDD representation of an array. + *
[ DEREFS: none ] + * @throws PrismException if number of states is too large (uses Java int based indices) */ - public IntegerVector(JDDNode dd, JDDVars vars, ODDNode odd) + public IntegerVector(JDDNode dd, JDDVars vars, ODDNode odd) throws PrismException { + long numStates = odd.getEOff() + odd.getTOff(); + if (numStates > Integer.MAX_VALUE) { + throw new PrismNotSupportedException("Can not create IntegerVector with more than " + Integer.MAX_VALUE + " states, have " + numStates + " states"); + } v = IV_ConvertMTBDD(dd.ptr(), vars.array(), vars.n(), odd.ptr()); - n = (int)(odd.getEOff() + odd.getTOff()); + n = (int)numStates; } private native long IV_ConvertMTBDD(long dd, long vars, int num_vars, long odd);