Refactor/improve processing of quoted identifiers (labels/prop names) too.

prism/src/parser/IdentUsage.java

@@ -36,6 +36,9 @@ import prism.PrismLangException;
  */
 public class IdentUsage
 {
+	// Are these identifiers used in (double) quotes?
+	private boolean quoted = false;
+	
 	// Where identifiers were declared (AST element)
 	private HashMap<String, ASTElement> identDecls;
 	// Uses of identifiers (e.g. "constant")
@@ -45,6 +48,15 @@ public class IdentUsage
 
 	public IdentUsage()
 	{
+		this(false);
+	}
+	
+	/**
+	 * @param quoted Are these identifiers used in (double) quotes?
+	 */
+	public IdentUsage(boolean quoted)
+	{
+		this.quoted = quoted;
 		identDecls = new HashMap<>();
 		identUses = new HashMap<>();
 		identLocs = new HashMap<>();
@@ -95,7 +107,8 @@ public class IdentUsage
 		if (existing != null) {
 			// Construct error message if identifier exists already
 			String identStr = use != null ? ("Name of " + use) : "Identifier";
-			identStr += " " + ident + "";
+			String qu = quoted ? "\"" : "";
+			identStr += " " + qu + ident + qu;
 			String existingUse = identUses.get(ident);
 			existingUse = (existingUse == null) ? "" : " for a " + existingUse;
 			String existingLoc = identLocs.get(ident);
@@ -107,7 +120,7 @@ public class IdentUsage
 	@SuppressWarnings("unchecked")
 	public IdentUsage deepCopy()
 	{
-		IdentUsage ret = new IdentUsage();
+		IdentUsage ret = new IdentUsage(quoted);
 		ret.identDecls = (HashMap<String, ASTElement>) identDecls.clone();
 		return ret;
 	}

prism/src/parser/ast/ModulesFile.java

@@ -73,6 +73,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 
 	// Info about all identifiers used
 	private IdentUsage identUsage;
+	private IdentUsage quotedIdentUsage;
 	// List of all module names
 	private String[] moduleNames;
 	// List of synchronising actions
@@ -106,6 +107,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		hasObservables = false;
 		obsVars = new ArrayList<String>();
 		identUsage = new IdentUsage();
+		quotedIdentUsage = new IdentUsage(true);
 		varDecls = new Vector<Declaration>();
 		varNames = new Vector<String>();
 		varTypes = new Vector<Type>();
@@ -604,6 +606,33 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		identUsage.checkIdent(ident, decl, use);
 	}
 
+	/**
+	 * Check if a quoted identifier is already used somewhere in the model
+	 * (as a label)
+	 * and throw an exception if it is. Otherwise, add it to the list.
+	 * @param ident The name of the (new) identifier, without quotes
+	 * @param decl Where the identifier is declared in the model
+	 * @param use Optionally, the identifier's usage (e.g. "label")
+	 */
+	private void checkAndAddQuotedIdentifier(String ident, ASTElement decl, String use) throws PrismLangException
+	{
+		quotedIdentUsage.checkAndAddIdentifier(ident, decl, use, "the model");
+	}
+	
+	@Override
+	public boolean isQuotedIdentUsed(String ident)
+	{
+		return quotedIdentUsage.isIdentUsed(ident);
+	}
+
+	@Override
+	public void checkQuotedIdent(String ident, ASTElement decl, String use) throws PrismLangException
+	{
+		// Goes beyond default implementation in ModelInfo:
+		// produces better error messages
+		quotedIdentUsage.checkIdent(ident, decl, use);
+	}
+
 	// get individual module name
 	public String getModuleName(int i)
 	{
@@ -760,6 +789,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 		// Clear data that will be generated by this method 
 		// (in case it has already been called previously).
 		identUsage.clear();
+		quotedIdentUsage.clear();
 		varDecls.clear();
 		varNames.clear();
 		varTypes.clear();
@@ -902,21 +932,10 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 
 	private void checkLabelIdents() throws PrismLangException
 	{
-		int i, n;
-		String s;
-		Vector<String> labelIdents;
-
-		// go thru labels
-		n = labelList.size();
-		labelIdents = new Vector<String>();
-		for (i = 0; i < n; i++) {
-			s = labelList.getLabelName(i);
-			// see if ident has been used already for a label
-			if (labelIdents.contains(s)) {
-				throw new PrismLangException("Duplicated label name \"" + s + "\"", labelList.getLabelNameIdent(i));
-			} else {
-				labelIdents.add(s);
-			}
+		int n = labelList.size();
+		for (int i = 0; i < n; i++) {
+			String s = labelList.getLabelName(i);
+			checkAndAddQuotedIdentifier(s, labelList.getLabelNameIdent(i), "label");
 		}
 	}
 
@@ -1527,6 +1546,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato
 			ret.addObservableVar(ov);
 		// Copy other (generated) info
 		ret.identUsage = (identUsage == null) ? null : identUsage.deepCopy();
+		ret.quotedIdentUsage = (quotedIdentUsage == null) ? null : quotedIdentUsage.deepCopy();
 		ret.moduleNames = (moduleNames == null) ? null : moduleNames.clone();
 		ret.synchs = (synchs == null) ? null : (Vector<String>)synchs.clone();
 		if (varDecls != null) {

prism/src/parser/ast/PropertiesFile.java

@@ -51,6 +51,7 @@ public class PropertiesFile extends ASTElement
 
 	// Info about all identifiers used
 	private IdentUsage identUsage;
+	private IdentUsage quotedIdentUsage;
 
 	// Values set for undefined constants (null if none)
 	private Values undefinedConstantValues;
@@ -68,6 +69,7 @@ public class PropertiesFile extends ASTElement
 		constantList = new ConstantList();
 		properties = new Vector<Property>();
 		identUsage = new IdentUsage();
+		quotedIdentUsage = new IdentUsage(true);
 		undefinedConstantValues = null;
 		constantValues = null;
 	}
@@ -273,6 +275,22 @@ public class PropertiesFile extends ASTElement
 		return identUsage.isIdentUsed(ident);
 	}
 
+	/**
+	 * Check if a quoted identifier is already used somewhere here or in the model
+	 * (as a label or property name)
+	 * and throw an exception if it is. Otherwise, add it to the list.
+	 * @param ident The name of the (new) identifier
+	 * @param decl Where the identifier is declared
+	 * @param use Optionally, the identifier's usage (e.g. "constant")
+	 */
+	private void checkAndAddQuotedIdentifier(String ident, ASTElement decl, String use) throws PrismLangException
+	{
+		// Check model first
+		modelInfo.checkQuotedIdent(ident, decl, use);
+		// Then check/add here in the properties file
+		quotedIdentUsage.checkAndAddIdentifier(ident, decl, use, "the properties");
+	}
+	
 	// method to tidy up (called after parsing)
 
 	public void tidyUp() throws PrismLangException
@@ -346,38 +364,25 @@ public class PropertiesFile extends ASTElement
 
 	private void checkLabelIdents() throws PrismLangException
 	{
-		int i, n;
-		String s;
-		Vector<String> labelIdents;
-		LabelList mfLabels;
-
-		// get label list from model file
-		mfLabels = modulesFile.getLabelList();
-		// add model file labels to combined label list (cloning them just for good measure)
+		// check for identifier clashes
+		int n = labelList.size();
+		for (int i = 0; i < n; i++) {
+			String s = labelList.getLabelName(i);
+			checkAndAddQuotedIdentifier(s, labelList.getLabelNameIdent(i), "label");
+		}
+		
+		// build combined label list
 		combinedLabelList = new LabelList();
+		// first add model file labels to combined label list (cloning them just for good measure)
+		LabelList mfLabels = modulesFile.getLabelList();
 		n = mfLabels.size();
-		for (i = 0; i < n; i++) {
+		for (int i = 0; i < n; i++) {
 			combinedLabelList.addLabel(mfLabels.getLabelNameIdent(i), mfLabels.getLabel(i).deepCopy());
 		}
-		// go thru labels
+		// then add labels from here
 		n = labelList.size();
-		labelIdents = new Vector<String>();
-		for (i = 0; i < n; i++) {
-			s = labelList.getLabelName(i);
-			// see if ident has been used already for a label in model file
-			if (mfLabels.getLabelIndex(s) != -1) {
-				throw new PrismLangException("Label \"" + s + "\" already defined in model file", labelList.getLabelNameIdent(i));
-			}
-			// see if ident has been used already for a label
-			if (labelIdents.contains(s)) {
-				throw new PrismLangException("Duplicated label name \"" + s + "\"", labelList.getLabelNameIdent(i));
-			}
-			// store identifier
-			// and add label to combined list
-			else {
-				labelIdents.addElement(s);
-				combinedLabelList.addLabel(labelList.getLabelNameIdent(i), labelList.getLabel(i));
-			}
+		for (int i = 0; i < n; i++) {
+			combinedLabelList.addLabel(labelList.getLabelNameIdent(i), labelList.getLabel(i));
 		}
 	}
 
@@ -398,35 +403,11 @@ public class PropertiesFile extends ASTElement
 	 */
 	private void checkPropertyNames() throws PrismLangException
 	{
-		int i, n;
-		String s;
-		Vector<String> propNames;
-		LabelList mfLabels;
-
-		// get label list from model file
-		mfLabels = modulesFile.getLabelList();
-		// Go thru properties
-		n = properties.size();
-		propNames = new Vector<String>();
-		for (i = 0; i < n; i++) {
-			s = properties.get(i).getName();
-			if (s == null)
-				continue;
-			// see if ident has been used already for a label in model file
-			if (mfLabels.getLabelIndex(s) != -1) {
-				throw new PrismLangException("Property name \"" + s + "\" clashes with label in model file", getPropertyObject(i));
-			}
-			// see if ident has been used already for a label in properties file
-			if (labelList.getLabelIndex(s) != -1) {
-				throw new PrismLangException("Property name \"" + s + "\" clashes with label", getPropertyObject(i));
-			}
-			// see if ident has been used already for a property name
-			if (propNames.contains(s)) {
-				throw new PrismLangException("Duplicated property name \"" + s + "\"", getPropertyObject(i));
-			}
-			// store identifier
-			else {
-				propNames.addElement(s);
+		int n = properties.size();
+		for (int i = 0; i < n; i++) {
+			String s = properties.get(i).getName();
+			if (s != null) {
+				checkAndAddQuotedIdentifier(s, getPropertyObject(i), "property");
 			}
 		}
 	}

prism/src/prism/ModelInfo.java

@@ -317,4 +317,32 @@ public interface ModelInfo
 			throw new PrismLangException("Identifier " + ident + " is already used in the model", decl);
 		}
 	}
+	
+	/**
+	 * Check if an identifier (in double quotes) is used in the model
+	 * (e.g., as a label)
+	 */
+	public default boolean isQuotedIdentUsed(String ident)
+	{
+		// Default implementation looks up any labels
+		if (getLabelIndex(ident) != -1) {
+			return true;
+		}
+		return false;
+	}
+
+	/**
+	 * Check if an identifier (in double quotes) is already used in the model
+	 * (e.g., as a label) and throw an exception if it is.
+	 * @param ident The name of the identifier to check
+	 * @param decl Where the identifier is declared in the model (for the error message)
+	 * @param use Optionally, the identifier's usage (e.g. "constant")
+	 */
+	public default void checkQuotedIdent(String ident, ASTElement decl, String use) throws PrismLangException
+	{
+		// Default implementation via isQuotedIdentUsed
+		if (isQuotedIdentUsed(ident)) {
+			throw new PrismLangException("Identifier \"" + ident + "\" is already used in the model", decl);
+		}
+	}
 }