MTBDD model checking: Harden against missing ODD

We want to allow MTBDD engine model checking without having an ODD
to encode the BDD state to index information. This allows to deal
with models where the state space is too big for the ODD index type (2^63).

Here, we harden all the places where the ODD information is accessed
to gracefully handle the abscence of the ODD:

* When trying to convert from MTBDD to explicit vector, a
  missing ODD is fatal
* When printing state values or a state list, index information is
  not available and thus omitted
* For the hybrid and sparse engine, the odd index checks (whether
  the number of states fit into an int32_t) are now done using
  helper functions that handle both null ODD and out-of-range values.

prism/src/dv/DoubleVector.java

@@ -109,12 +109,10 @@ public class DoubleVector
 	 */
 	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");
-		}
+		ODDUtils.checkInt(odd, "Can not create DoubleVector");
+
 		v = DV_ConvertMTBDD(dd.ptr(), vars.array(), vars.n(), odd.ptr());
-		n = (int)numStates;
+		n = (int)odd.getNumStates();
 	}
 	
 	private native long DV_ConvertMTBDD(long dd, long vars, int num_vars, long odd);

prism/src/dv/IntegerVector.java

@@ -94,12 +94,10 @@ public class IntegerVector
 	 */
 	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");
-		}
+		ODDUtils.checkInt(odd, "Can not create IntegerVector");
+
 		v = IV_ConvertMTBDD(dd.ptr(), vars.array(), vars.n(), odd.ptr());
-		n = (int)numStates;
+		n = (int)odd.getNumStates();
 	}
 	
 	private native long IV_ConvertMTBDD(long dd, long vars, int num_vars, long odd);

prism/src/hybrid/PrismHybrid.java

@@ -79,10 +79,7 @@ public class PrismHybrid
 	{
 		// currently, the hybrid engine internally uses int (signed 32bit) index values
 		// so, if the number of states is larger than Integer.MAX_VALUE, there is a problem
-		long n = odd.getEOff() + odd.getTOff();
-		if (n >= Integer.MAX_VALUE) {
-			throw new PrismNotSupportedException("The hybrid engine can currently only handle up to " + Integer.MAX_VALUE + " reachable states, model has " + n + " states");
-		}
+		ODDUtils.checkInt(odd, "Currently, the hybrid engine cannot handle models");
 	}
 
 	//------------------------------------------------------------------------------

prism/src/odd/ODDNode.java

@@ -55,6 +55,17 @@ public class ODDNode
 		return ODDUtils.ODD_GetEOff(ptr);
 	}
 
+	/**
+	 * Returns the number of states for this ODD node.
+	 * Throws an arithmetic exception if the number of states
+	 * does not fit in a Java long (should not occur as that is
+	 * caught during ODD construction).
+	 */
+	public long getNumStates()
+	{
+		return Math.addExact(getTOff(), getEOff());
+	}
+
 	public ODDNode getThen()
 	{
 		return new ODDNode(ODDUtils.ODD_GetThen(ptr));

prism/src/odd/ODDUtils.java

@@ -28,6 +28,7 @@ package odd;
 
 import jdd.*;
 import prism.PrismException;
+import prism.PrismNotSupportedException;
 
 public class ODDUtils
 {
@@ -121,7 +122,57 @@ public class ODDUtils
 	{
 		return JDD.ptrToNode(ODD_SingleIndexToDD(i, odd.ptr(), vars.array(), vars.n()));
 	}
-	
+
+	/**
+	 * Checks that the given ODD has indices that can be represented by
+	 * Java integers. If that is not the case, or the ODD is {@code null},
+	 * a PrismNotSupportedException is thrown.
+	 * @param odd the ODD (may be {@code null})
+	 * @param msg Initial part of error message, will be extended with
+	 *        " with more than X states, have Y states"
+	 */
+	public static void checkInt(ODDNode odd, String msg) throws PrismNotSupportedException
+	{
+		if (odd != null) {
+			try {
+				long numStates = odd.getNumStates();
+				if (numStates > Integer.MAX_VALUE) {
+					// number of states fit in long, but not in int
+					throw new PrismNotSupportedException(msg + " with more than " + Integer.MAX_VALUE + " states, have " + numStates + " states");
+				} else {
+					// everything is fine
+					return;
+				}
+			} catch (ArithmeticException e) {
+				// number of states does not fit into long, ignore here, handled below
+			}
+		}
+
+		// we either have no ODD or eoff + toff does not fit into long
+		throw new PrismNotSupportedException(msg + " with more than " + Integer.MAX_VALUE + " states, have at least " + Long.MAX_VALUE + " states");
+	}
+
+	/**
+	 * Returns true if the given ODD has indices that can be represented by
+	 * Java integers. If the odd is {@code null}, returns false as well.
+	 * @param odd the ODD (may be {@code null})
+	 */
+	public static boolean hasIntValue(ODDNode odd)
+	{
+		if (odd == null)
+			return false;
+
+		try {
+			long numStates = odd.getNumStates();
+			if (numStates <= Integer.MAX_VALUE) {
+				return true;
+			}
+		} catch (ArithmeticException e) {
+			// number of states does not fit into long, ignore here, handled below
+		}
+		return false;
+	}
+
 	//------------------------------------------------------------------------------
 	// ODDNode methods
 	//------------------------------------------------------------------------------

prism/src/prism/Model.java

@@ -100,7 +100,7 @@ public interface Model
 	String globalToLocal(long x);
 	int globalToLocal(long x, int l);
 	State convertBddToState(JDDNode dd);
-	int convertBddToIndex(JDDNode dd);
+	int convertBddToIndex(JDDNode dd) throws PrismNotSupportedException;
 
 	StateList getReachableStates();
 	

prism/src/prism/ProbModel.java

@@ -1150,11 +1150,13 @@ public class ProbModel implements Model
 	 * Convert a BDD (over model row variables) representing a single state
 	 * to a (reachable) state index. 
 	 */
-	public int convertBddToIndex(JDDNode dd)
+	public int convertBddToIndex(JDDNode dd) throws PrismNotSupportedException
 	{
 		JDDNode ptr;
 		ODDNode oddPtr;
 		int i, n, index;
+
+		ODDUtils.checkInt(odd, "Cannot convert Bdd to index in model");
 		// Traverse BDD and ODD simultaneously to compute index
 		ptr = dd;
 		oddPtr = odd;

prism/src/prism/StateList.java

@@ -71,7 +71,7 @@ public interface StateList
 	/**
 	 * Print the states to a log, in Dot format.
 	 */
-	void printDot(PrismLog log);
+	void printDot(PrismLog log) throws PrismException;
 
 	/**
 	 * Format the list of states as a list of strings.
@@ -99,7 +99,7 @@ public interface StateList
 	 * Get the index of a state in the list, specified as a State object.
 	 * Returns -1 if the state is not on the list or there is a problem with the lookup. 
 	 */
-	int getIndexOfState(State state);
+	int getIndexOfState(State state) throws PrismNotSupportedException;
 
 	/**
 	 * Free any memory associated with storing this list of states.

prism/src/prism/StateListMTBDD.java

@@ -188,11 +188,15 @@ public class StateListMTBDD implements StateList
 	}
 	
 	@Override
-	public void printDot(PrismLog log)
+	public void printDot(PrismLog log) throws PrismException
 	{
 		outputFormat = OutputFormat.DOT;
 		limit = false;
 		outputLog = log;
+
+		if (odd == null) {
+			throw new PrismNotSupportedException("Cannot export state list as DOT, too many states");
+		}
 		doPrint();
 	}
 	
@@ -245,9 +249,19 @@ public class StateListMTBDD implements StateList
 		if (level == numVars) {
 			
 			switch (outputFormat) {
-			case NORMAL: outputLog.print(n + ":("); break;
+			case NORMAL:
+				if (o != null) {
+					outputLog.print(n + ":(");
+				} else {
+					// we have no index
+					outputLog.print("(");
+				}
+				break;
 			case MATLAB: break;
-			case DOT: outputLog.print(n + " [label=\"" + n + "\\n("); break;
+			case DOT:
+				assert(o != null);  // should not happen, missing ODD is caught before
+				outputLog.print(n + " [label=\"" + n + "\\n(");
+				break;
 			case STRINGS: break;
 			}
 			j = varList.getNumVars();
@@ -282,14 +296,18 @@ public class StateListMTBDD implements StateList
 			e = dd.getElse();
 			t = dd.getThen();
 		}
-		
+
+		ODDNode oe = (o != null ? o.getElse() : null);
+		ODDNode ot = (o != null ? o.getThen() : null);
+		long eoff = (o != null ? o.getEOff() : 0);
+
 		// then recurse...
 		currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; }
-		printRec(e, level+1, o.getElse(), n);
+		printRec(e, level+1, oe, n);
 		currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; }
 		varValues[currentVar] += (1 << (varSizes[currentVar]-1-currentVarLevel));
 		currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; }
-		printRec(t, level+1, o.getThen(), n+o.getEOff());
+		printRec(t, level+1, ot, n + eoff);
 		currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; }
 		varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel));
 	}
@@ -374,11 +392,14 @@ public class StateListMTBDD implements StateList
 	}
 
 	@Override
-	public int getIndexOfState(State state)
+	public int getIndexOfState(State state) throws PrismNotSupportedException
 	{
 		// Traverse BDD/ODD, top to bottom, computing index
 		JDDNode ptr = states;
 		ODDNode o = odd;
+
+		ODDUtils.checkInt(odd, "Cannot get index of state in model");
+
 		int level = 0;
 		int index = 0;
 		// Iterate through variables

prism/src/prism/StateModelChecker.java

@@ -1150,7 +1150,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 
 		// For some types of filter, store info that may be used to optimise model checking
 		FilterOperator op = expr.getOperatorType();
-		if (op == FilterOperator.STATE) {
+		if (op == FilterOperator.STATE && ODDUtils.hasIntValue(odd)) {
 			// Check filter satisfied by exactly one state
 			if (statesFilter.size() != 1) {
 				String s = "Filter should be satisfied in exactly 1 state";
@@ -1158,9 +1158,9 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 				throw new PrismException(s);
 			}
 			currentFilter = new Filter(Filter.FilterOperator.STATE, ODDUtils.GetIndexOfFirstFromDD(ddFilter, odd, allDDRowVars));
-		} else if (op == FilterOperator.FORALL && filterInit && filterInitSingle) {
+		} else if (op == FilterOperator.FORALL && filterInit && filterInitSingle && ODDUtils.hasIntValue(odd)) {
 			currentFilter = new Filter(Filter.FilterOperator.STATE, ODDUtils.GetIndexOfFirstFromDD(ddFilter, odd, allDDRowVars));
-		} else if (op == FilterOperator.FIRST && filterInit && filterInitSingle) {
+		} else if (op == FilterOperator.FIRST && filterInit && filterInitSingle && ODDUtils.hasIntValue(odd)) {
 			currentFilter = new Filter(Filter.FilterOperator.STATE, ODDUtils.GetIndexOfFirstFromDD(ddFilter, odd, allDDRowVars));
 		} else {
 			currentFilter = null;

prism/src/prism/StateValues.java

@@ -167,7 +167,7 @@ public interface StateValues extends StateVector
 	StateValues sumOverDDVars(JDDVars sumVars, Model newModel) throws PrismException;
 
 	/** Returns an Object with the value of the i-th entry in this vector. */
-	Object getValue(int i);
+	Object getValue(int i) throws PrismNotSupportedException;
 
 	/**
 	 * Generate BDD for states in the given interval

prism/src/prism/StateValuesMTBDD.java

@@ -134,12 +134,14 @@ public class StateValuesMTBDD implements StateValues
 	/**
 	 * Set element i of this vector to value d. 
 	 */
-	public void setElement(int i, double d)
+	public void setElement(int i, double d) throws PrismNotSupportedException
 	{
 		ODDNode ptr;
 		JDDNode dd;
 		int j, k;
-		
+
+		ODDUtils.checkInt(odd, "Cannot set element via index for model");
+
 		// Use ODD to build BDD for state index i
 		dd = JDD.Constant(1);
 		ptr = odd;
@@ -287,9 +289,12 @@ public class StateValuesMTBDD implements StateValues
 	}
 
 	@Override
-	public Object getValue(int i)
+	public Object getValue(int i) throws PrismNotSupportedException
 	{
 		JDDNode dd = values;
+
+		ODDUtils.checkInt(odd, "Cannot get value for state index in model");
+
 		ODDNode ptr = odd;
 		int o = 0;
 		for (int k = 0; k < numVars; k++) {
@@ -653,7 +658,13 @@ public class StateValuesMTBDD implements StateValues
 		// base case - at bottom (nonzero terminal)
 		if (level == numVars) {
 		
-			outputLog.print(n + ":(");
+			if (o != null) {
+				outputLog.print(n + ":(");
+			} else {
+				// we have no index
+				outputLog.print("(");
+			}
+
 			j = varList.getNumVars();
 			for (i = 0; i < j; i++) {
 				// integer variable
@@ -666,6 +677,7 @@ public class StateValuesMTBDD implements StateValues
 				}
 				if (i < j-1) outputLog.print(",");
 			}
+
 			outputLog.print(")=" + dd.getValue());
 			outputLog.println();
 			return;
@@ -680,13 +692,17 @@ public class StateValuesMTBDD implements StateValues
 			t = dd.getThen();
 		}
 
+		ODDNode oe = (o != null ? o.getElse() : null);
+		ODDNode ot = (o != null ? o.getThen() : null);
+		long eoff = (o != null ? o.getEOff() : 0);
+
 		// then recurse...
 		currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; }
-		printRec(e, level+1, o.getElse(), n);
+		printRec(e, level+1, oe, n);
 		currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; }
 		varValues[currentVar] += (1 << (varSizes[currentVar]-1-currentVarLevel));
 		currentVarLevel++; if (currentVarLevel == varSizes[currentVar]) { currentVar++; currentVarLevel=0; }
-		printRec(t, level+1, o.getThen(), n+o.getEOff());
+		printRec(t, level+1, ot, n + eoff);
 		currentVarLevel--; if (currentVarLevel == -1) { currentVar--; currentVarLevel=varSizes[currentVar]-1; }
 		varValues[currentVar] -= (1 << (varSizes[currentVar]-1-currentVarLevel));
 	}

prism/src/prism/StateVector.java

@@ -39,7 +39,7 @@ public interface StateVector
 	/**
 	 * Get the value of the ith element of the vector, as an Object.
 	 */
-	public Object getValue(int i);
+	public Object getValue(int i) throws PrismNotSupportedException;
 	
 	/**
 	 * Clear the vector, i.e. free any used memory.

prism/src/sparse/PrismSparse.java

@@ -33,6 +33,7 @@ import jdd.JDD;
 import jdd.JDDNode;
 import jdd.JDDVars;
 import odd.ODDNode;
+import odd.ODDUtils;
 import prism.NativeIntArray;
 import prism.OpsAndBoundsList;
 import prism.PrismException;
@@ -89,10 +90,7 @@ public class PrismSparse
 	{
 		// currently, the sparse engine internally uses int (signed 32bit) index values
 		// so, if the number of states is larger than Integer.MAX_VALUE, there is a problem
-		long n = odd.getEOff() + odd.getTOff();
-		if (n >= Integer.MAX_VALUE) {
-			throw new PrismNotSupportedException("The sparse engine can currently only handle up to " + Integer.MAX_VALUE + " reachable states, model has " + n + " states");
-		}
+		ODDUtils.checkInt(odd, "Currently, the sparse engine cannot handle models");
 	}
 
 	//----------------------------------------------------------------------------------------------