From cd73222bbadaddaac81eb23333e2c05f1e0c61ef Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 5 Apr 2006 16:09:05 +0000
Subject: [PATCH] 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   | 8 ++++----
 prism/src/prism/Explicit2MTBDD.java | 7 ++++++-
 2 files changed, 10 insertions(+), 5 deletions(-)

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();