diff --git a/prism/src/parser/IdentUsage.java b/prism/src/parser/IdentUsage.java index 9823fcbd..6a8f5d7f 100644 --- a/prism/src/parser/IdentUsage.java +++ b/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 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) identDecls.clone(); return ret; } diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 18182e58..ce7dd652 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/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(); identUsage = new IdentUsage(); + quotedIdentUsage = new IdentUsage(true); varDecls = new Vector(); varNames = new Vector(); varTypes = new Vector(); @@ -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 labelIdents; - - // go thru labels - n = labelList.size(); - labelIdents = new Vector(); - 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)synchs.clone(); if (varDecls != null) { diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 35dacfc3..fea022f5 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/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(); 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 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(); - 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 propNames; - LabelList mfLabels; - - // get label list from model file - mfLabels = modulesFile.getLabelList(); - // Go thru properties - n = properties.size(); - propNames = new Vector(); - 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"); } } } diff --git a/prism/src/prism/ModelInfo.java b/prism/src/prism/ModelInfo.java index 9c0851bc..f0bfb172 100644 --- a/prism/src/prism/ModelInfo.java +++ b/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); + } + } }