Bug fix for explicit import when some variables have zero range.

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

prism/src/parser/ModulesFile.java

@@ -679,12 +679,12 @@ public class ModulesFile
 			}
 			// check range is valid
 			if (high - low <= 0) {
-				String s = "Invalid range for variable " + name;
+				String s = "Invalid range (" + low + "-" + high + ") for variable " + name;
 				throw new PrismException(s);
 			}
 			// check start is valid
 			if (start < low || start > high) {
-				String s = "Invalid initial value for variable " + name;
+				String s = "Invalid initial value (" + start + ") for variable " + name;
 				throw new PrismException(s);
 			}
 			varList.addVar(name, low, high, start, -1, decl.getType());
@@ -717,12 +717,12 @@ public class ModulesFile
 				}
 				// check range is valid
 				if (high - low <= 0) {
-					String s = "Invalid range for variable " + name;
+					String s = "Invalid range (" + low + "-" + high + ") for variable " + name;
 					throw new PrismException(s);
 				}
 				// check start is valid
 				if (start < low || start > high) {
-					String s = "Invalid initial value for variable " + name;
+					String s = "Invalid initial value (" + start + ") for variable " + name;
 					throw new PrismException(s);
 				}
 				varList.addVar(name, low, high, start, i, decl.getType());

prism/src/prism/Explicit2MTBDD.java

@@ -262,8 +262,13 @@ public class Explicit2MTBDD
 				}
 				s = in.readLine(); lineNum++;
 			}
+			// compute variable ranges
 			for (i = 0; i < numVars; i++) {
-				if (varTypes[i] == Expression.INT) varRanges[i] = varMaxs[i] - varMins[i];
+				if (varTypes[i] == Expression.INT) {
+					varRanges[i] = varMaxs[i] - varMins[i];
+					// if range = 0, increment maximum - we don't allow zero-range variables
+					if (varRanges[i] == 0) varMaxs[i]++;
+				}
 			}
 			// close file
 			in.close();