DoubleVector: 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@12022 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/dv/DoubleVector.java

@@ -105,11 +105,16 @@ public class DoubleVector
 	/**
 	 * Create a new DoubleVector 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 DoubleVector(JDDNode dd, JDDVars vars, ODDNode odd)
+	public DoubleVector(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 DoubleVector with more than " + Integer.MAX_VALUE + " states, have " + numStates + " states");
+		}
 		v = DV_ConvertMTBDD(dd.ptr(), vars.array(), vars.n(), odd.ptr());
-		n = (int)(odd.getEOff() + odd.getTOff());
+		n = (int)numStates;
 	}
 	
 	private native long DV_ConvertMTBDD(long dd, long vars, int num_vars, long odd);

prism/src/prism/ProbModelChecker.java

@@ -1252,7 +1252,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	 * the (single) initial state or equiprobable over multiple initial states.
 	 * The type of storage (MTBDD or double vector) matches the current engine.
 	 */
-	private StateValues buildInitialDistribution()
+	private StateValues buildInitialDistribution() throws PrismException
 	{
 		StateValues dist = null;
 		JDDNode init;

prism/src/prism/StateValues.java

@@ -38,7 +38,7 @@ import parser.ast.RelOp;
 public interface StateValues extends StateVector
 {
 	/** Converts to StateValuesDV, destroys (clear) this vector */
-	StateValuesDV convertToStateValuesDV();
+	StateValuesDV convertToStateValuesDV() throws PrismException;
 
 	/** Converts to StateValuesMTBDD, destroys (clear) this vector */
 	StateValuesMTBDD convertToStateValuesMTBDD();

prism/src/prism/StateValuesDV.java

@@ -113,7 +113,7 @@ public class StateValuesDV implements StateValues
 	 * @param dd the double vector
 	 * @param model the underlying model
 	 */
-	public StateValuesDV(JDDNode dd, Model model)
+	public StateValuesDV(JDDNode dd, Model model) throws PrismException
 	{
 		// TODO: Enforce/check that dd is zero for all non-reachable states
 		this(new DoubleVector(dd, model.getAllDDRowVars(), model.getODD()), model);

prism/src/prism/StateValuesMTBDD.java

@@ -104,7 +104,7 @@ public class StateValuesMTBDD implements StateValues
 	// CONVERSION METHODS
 	
 	@Override
-	public StateValuesDV convertToStateValuesDV()
+	public StateValuesDV convertToStateValuesDV() throws PrismException
 	{
 		// convert to StateValuesDV, destroy (clear) old vector
 		StateValuesDV res = new StateValuesDV(values, model);