diff --git a/prism/src/parser/IdentUsage.java b/prism/src/parser/IdentUsage.java new file mode 100644 index 00000000..9823fcbd --- /dev/null +++ b/prism/src/parser/IdentUsage.java @@ -0,0 +1,114 @@ +//============================================================================== +// +// Copyright (c) 2021- +// Authors: +// * Dave Parker (University of Birmingham) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package parser; + +import java.util.HashMap; + +import parser.ast.ASTElement; +import prism.PrismLangException; + +/** + * Helper class to keep track of a set of identifiers that have been used. + */ +public class IdentUsage +{ + // Where identifiers were declared (AST element) + private HashMap identDecls; + // Uses of identifiers (e.g. "constant") + private HashMap identUses; + // Location of identifiers (e.g. "the model") + private HashMap identLocs; + + public IdentUsage() + { + identDecls = new HashMap<>(); + identUses = new HashMap<>(); + identLocs = new HashMap<>(); + } + + public void clear() + { + identDecls.clear(); + identUses.clear(); + identLocs.clear(); + } + + /** + * Check if an identifier is already used somewhere + * 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 in the model + * @param use Optionally, the identifier's usage (e.g. "constant") + * @param loc Optionally, the identifier's location (e.g. "the model") + */ + public void checkAndAddIdentifier(String ident, ASTElement decl, String use, String loc) throws PrismLangException + { + checkIdent(ident, decl, use); + identDecls.put(ident, decl); + identUses.put(ident, use); + identLocs.put(ident, loc); + } + + /** + * Check if an identifier is already used somewhere + * @param ident The name of the identifier to check + */ + public boolean isIdentUsed(String ident) + { + return identDecls.containsKey(ident); + } + + /** + * Check if an identifier is already used somewhere + * 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 void checkIdent(String ident, ASTElement decl, String use) throws PrismLangException + { + ASTElement existing = identDecls.get(ident); + if (existing != null) { + // Construct error message if identifier exists already + String identStr = use != null ? ("Name of " + use) : "Identifier"; + identStr += " " + ident + ""; + String existingUse = identUses.get(ident); + existingUse = (existingUse == null) ? "" : " for a " + existingUse; + String existingLoc = identLocs.get(ident); + existingLoc = (existingLoc == null) ? "" : " in " + existingLoc; + throw new PrismLangException(identStr + " is already used" + existingUse + existingLoc, decl); + } + } + + @SuppressWarnings("unchecked") + public IdentUsage deepCopy() + { + IdentUsage ret = new IdentUsage(); + ret.identDecls = (HashMap) identDecls.clone(); + return ret; + } +} diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 4a20463a..18182e58 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -27,12 +27,12 @@ package parser.ast; import java.util.ArrayList; -import java.util.HashMap; import java.util.HashSet; import java.util.List; import java.util.Vector; import param.BigRational; +import parser.IdentUsage; import parser.State; import parser.Values; import parser.VarList; @@ -71,8 +71,8 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato private boolean hasObservables; // Observables info private List obsVars; - // Lists of all identifiers used and where - private HashMap identUsage; + // Info about all identifiers used + private IdentUsage identUsage; // List of all module names private String[] moduleNames; // List of synchronising actions @@ -105,7 +105,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato initStates = null; hasObservables = false; obsVars = new ArrayList(); - identUsage = new HashMap<>(); + identUsage = new IdentUsage(); varDecls = new Vector(); varNames = new Vector(); varTypes = new Vector(); @@ -580,24 +580,28 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato * (as a formula, constant or variable) * and throw an exception if it is. Otherwise, add it to the list. * @param ident The name of the (new) identifier - * @param e Where the identifier is declared in the model + * @param decl Where the identifier is declared in the model + * @param use Optionally, the identifier's usage (e.g. "constant") */ - private void checkAndAddIdentifier(String ident, ASTElement e) throws PrismLangException + private void checkAndAddIdentifier(String ident, ASTElement decl, String use) throws PrismLangException { - ASTElement existing = identUsage.get(ident); - if (existing != null) { - throw new PrismLangException("Identifier \"" + ident + "\" is already used in the model", e); - } - identUsage.put(ident, e); + identUsage.checkAndAddIdentifier(ident, decl, use, "the model"); } - /** - * Check if an identifier is already used somewhere in the model - * (as a formula, constant or variable) - */ + @Override public boolean isIdentUsed(String ident) { - return identUsage.containsKey(ident); + // Goes beyond default implementation in ModelInfo: + // also looks at formulas + return identUsage.isIdentUsed(ident); + } + + @Override + public void checkIdent(String ident, ASTElement decl, String use) throws PrismLangException + { + // Goes beyond default implementation in ModelInfo: + // also looks at formulas, and produces better error messages + identUsage.checkIdent(ident, decl, use); } // get individual module name @@ -841,7 +845,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato int n = formulaList.size(); for (int i = 0; i < n; i++) { String s = formulaList.getFormulaName(i); - checkAndAddIdentifier(s, formulaList.getFormulaNameIdent(i)); + checkAndAddIdentifier(s, formulaList.getFormulaNameIdent(i), "formula"); } } @@ -988,7 +992,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato int n = constantList.size(); for (int i = 0; i < n; i++) { String s = constantList.getConstantName(i); - checkAndAddIdentifier(s, constantList.getConstantNameIdent(i)); + checkAndAddIdentifier(s, constantList.getConstantNameIdent(i), "constant"); } } @@ -1003,7 +1007,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato int n = getNumGlobals(); for (int i = 0; i < n; i++) { String s = getGlobal(i).getName(); - checkAndAddIdentifier(s, getGlobal(i)); + checkAndAddIdentifier(s, getGlobal(i), "variable"); varDecls.add(getGlobal(i)); varNames.add(s); varTypes.add(getGlobal(i).getType()); @@ -1017,7 +1021,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato int numLocals = module.getNumDeclarations(); for (int j = 0; j < numLocals; j++) { String s = module.getDeclaration(j).getName(); - checkAndAddIdentifier(s, module.getDeclaration(j)); + checkAndAddIdentifier(s, module.getDeclaration(j), "variable"); varDecls.add(module.getDeclaration(j)); varNames.add(s); varTypes.add(module.getDeclaration(j).getType()); @@ -1522,7 +1526,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato for (String ov : obsVars) ret.addObservableVar(ov); // Copy other (generated) info - ret.identUsage = (identUsage == null) ? null : (HashMap) identUsage.clone(); + ret.identUsage = (identUsage == null) ? null : identUsage.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 0ff51f7a..35dacfc3 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -49,8 +49,8 @@ public class PropertiesFile extends ASTElement private ConstantList constantList; private Vector properties; // Properties - // Lists of all identifiers used and where - private HashMap identUsage; + // Info about all identifiers used + private IdentUsage identUsage; // Values set for undefined constants (null if none) private Values undefinedConstantValues; @@ -67,7 +67,7 @@ public class PropertiesFile extends ASTElement combinedLabelList = new LabelList(); constantList = new ConstantList(); properties = new Vector(); - identUsage = new HashMap<>(); + identUsage = new IdentUsage(); undefinedConstantValues = null; constantValues = null; } @@ -253,21 +253,15 @@ public class PropertiesFile extends ASTElement * (as a formula, constant or variable) * and throw an exception if it is. Otherwise, add it to the list. * @param ident The name of the (new) identifier - * @param e Where the identifier is declared in the model + * @param decl Where the identifier is declared + * @param use Optionally, the identifier's usage (e.g. "constant") */ - private void checkAndAddIdentifier(String ident, ASTElement e) throws PrismLangException + private void checkAndAddIdentifier(String ident, ASTElement decl, String use) throws PrismLangException { - // Check model file first - if (modulesFile.isIdentUsed(ident)) { - throw new PrismLangException("Identifier \"" + ident + "\" is already used in the model file", e); - } - // Then check here in the properties file - ASTElement existing = identUsage.get(ident); - if (existing != null) { - throw new PrismLangException("Identifier \"" + ident + "\" is already used", e); - } - // Finally, add - identUsage.put(ident, e); + // Check model first + modelInfo.checkIdent(ident, decl, use); + // Then check/add here in the properties file + identUsage.checkAndAddIdentifier(ident, decl, use, "the properties"); } /** @@ -276,7 +270,7 @@ public class PropertiesFile extends ASTElement */ public boolean isIdentUsed(String ident) { - return identUsage.containsKey(ident); + return identUsage.isIdentUsed(ident); } // method to tidy up (called after parsing) @@ -343,7 +337,7 @@ public class PropertiesFile extends ASTElement int n = formulaList.size(); for (int i = 0; i < n; i++) { String s = formulaList.getFormulaName(i); - checkAndAddIdentifier(s, formulaList.getFormulaNameIdent(i)); + checkAndAddIdentifier(s, formulaList.getFormulaNameIdent(i), "formula"); } } @@ -395,7 +389,7 @@ public class PropertiesFile extends ASTElement int n = constantList.size(); for (int i = 0; i < n; i++) { String s = constantList.getConstantName(i); - checkAndAddIdentifier(s, constantList.getConstantNameIdent(i)); + checkAndAddIdentifier(s, constantList.getConstantNameIdent(i), "constant"); } } @@ -674,7 +668,6 @@ public class PropertiesFile extends ASTElement /** * Perform a deep copy. */ - @SuppressWarnings("unchecked") public ASTElement deepCopy() { int i, n; @@ -691,7 +684,7 @@ public class PropertiesFile extends ASTElement ret.addProperty((Property) getPropertyObject(i).deepCopy()); } // Copy other (generated) info - ret.identUsage = (identUsage == null) ? null : (HashMap) identUsage.clone(); + ret.identUsage = (identUsage == null) ? null : identUsage.deepCopy(); ret.constantValues = (constantValues == null) ? null : new Values(constantValues); return ret; diff --git a/prism/src/prism/ModelInfo.java b/prism/src/prism/ModelInfo.java index 171e7335..9c0851bc 100644 --- a/prism/src/prism/ModelInfo.java +++ b/prism/src/prism/ModelInfo.java @@ -32,6 +32,7 @@ import java.util.List; import parser.Values; import parser.VarList; +import parser.ast.ASTElement; import parser.ast.DeclarationBool; import parser.ast.DeclarationIntUnbounded; import parser.ast.DeclarationType; @@ -284,4 +285,36 @@ public interface ModelInfo // Default implementation just extracts from getLabelNames() return getLabelNames().indexOf(name); } + + /** + * Check if an identifier is used in the model + * (e.g., as a constant or variable) + */ + public default boolean isIdentUsed(String ident) + { + // Default implementation looks up any vars/consts + if (getVarIndex(ident) != -1) { + return true; + } + Values v = getConstantValues(); + if (v != null & v.contains(ident)) { + return true; + } + return false; + } + + /** + * Check if an identifier is already used in the model + * (e.g., as a constant or variable) 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 checkIdent(String ident, ASTElement decl, String use) throws PrismLangException + { + // Default implementation via isIdentUsed + if (isIdentUsed(ident)) { + throw new PrismLangException("Identifier " + ident + " is already used in the model", decl); + } + } }