diff --git a/prism/src/parser/ModulesFile.java b/prism/src/parser/ModulesFile.java index ba01f316..64e3d4f4 100644 --- a/prism/src/parser/ModulesFile.java +++ b/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()); diff --git a/prism/src/prism/Explicit2MTBDD.java b/prism/src/prism/Explicit2MTBDD.java index a14d3df5..315be806 100644 --- a/prism/src/prism/Explicit2MTBDD.java +++ b/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();