Error message if user attempts to define a constant that is already defined.

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

prism/src/prism/UndefinedConstants.java

@@ -377,8 +377,17 @@ public class UndefinedConstants
 				pfConsts[index].define(sl, sh, ss);
 			}
 			else {
+				// If we are required to use all supplied const values, check for this
+				// (by default we don't care about un-needed or non-existent const values)
 				if (useAll)
 					throw new PrismException("\"" + name + "\" is not an undefined constant");
+				// But if an unused supplied value clashes with a defined constant, we complain
+				if (modulesFile != null && modulesFile.isDefinedConstant(name)) {
+					throw new PrismException("Constant \"" + name + "\" has already been defined in the model");
+				}
+				if (propertiesFile != null && propertiesFile.isDefinedConstant(name)) {
+					throw new PrismException("Constant \"" + name + "\" has already been defined");
+				}
 			}
 		}