Check for unbounded variables in ModelGenerator2MTBDD.

prism/src/prism/ModelGenerator2MTBDD.java

@@ -35,6 +35,9 @@ import jdd.JDDVars;
 import parser.State;
 import parser.Values;
 import parser.VarList;
+import parser.ast.DeclarationClock;
+import parser.ast.DeclarationIntUnbounded;
+import parser.ast.DeclarationType;
 
 /**
  * Class to construct a symbolic representation from a ModelGenerator object.
@@ -234,7 +237,7 @@ public class ModelGenerator2MTBDD
 	 * allocate DD vars for system
 	 * i.e. decide on variable ordering and request variables from CUDD
 	 */
-	private void allocateDDVars()
+	private void allocateDDVars() throws PrismNotSupportedException
 	{
 		JDDNode vr, vc;
 		int i, j, n;
@@ -268,6 +271,10 @@ public class ModelGenerator2MTBDD
 		// go through all vars in order (incl. global variables)
 		// so overall ordering can be specified by ordering in the input file
 		for (i = 0; i < numVars; i++) {
+			DeclarationType declType = varList.getDeclaration(i).getDeclType();
+			if (declType instanceof DeclarationClock || declType instanceof DeclarationIntUnbounded) {
+				throw new PrismNotSupportedException("Cannot build a model that contains a variable with unbounded range (try the explicit engine instead)");
+			}
 			// get number of dd variables needed
 			// (ceiling of log2 of range of variable)
 			n = varList.getRangeLogTwo(i);