IntegerVector: Check that number of states fit into int

If the number of states is too large for the index of the vector to
fit into a Java int throw a PrismNotSupportedException.



git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12023 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/dv/IntegerVector.java

@@ -89,11 +89,17 @@ public class IntegerVector
 	
 	/**
 	 * Create a new IntegerVector from an existing MTBDD representation of an array.
+	 * <br>[ DEREFS: <i>none</i> ]
+	 * @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);