From b30c5ac74a91a34c1f2973731f943e65e6243353 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 9 Aug 2011 21:33:46 +0000 Subject: [PATCH] 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 | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/prism/src/prism/UndefinedConstants.java b/prism/src/prism/UndefinedConstants.java index c03ff737..2cbd77e4 100644 --- a/prism/src/prism/UndefinedConstants.java +++ b/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"); + } } }