From acee7edc5cd608c9a3196284812cf8df7fc6ba4f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 10 Sep 2018 12:52:55 +0100 Subject: [PATCH] Refactoring of code to store/check identifiers used in model/properties files. --- prism/src/parser/ast/ModulesFile.java | 138 +++++++++++------------ prism/src/parser/ast/PropertiesFile.java | 72 ++++++------ 2 files changed, 100 insertions(+), 110 deletions(-) diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 900496f4..dddb09e8 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -26,19 +26,26 @@ package parser.ast; -import java.util.*; +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.*; -import parser.visitor.*; +import parser.State; +import parser.Values; +import parser.VarList; +import parser.type.Type; +import parser.visitor.ASTVisitor; +import parser.visitor.ModulesFileSemanticCheck; +import parser.visitor.ModulesFileSemanticCheckAfterConstants; import prism.ModelInfo; +import prism.ModelType; import prism.PrismException; import prism.PrismLangException; -import prism.ModelType; import prism.PrismUtils; import prism.RewardGenerator; -import prism.RewardGenerator.RewardLookup; -import parser.type.*; // Class representing parsed model file @@ -61,10 +68,8 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato private List rewardStructNames; // Names of reward structures private Expression initStates; // Initial states specification - // Lists of all identifiers used - private Vector formulaIdents; - private Vector constantIdents; - private Vector varIdents; // TODO: don't need? + // Lists of all identifiers used and where + private HashMap identUsage; // List of all module names private String[] moduleNames; // List of synchronising actions @@ -94,9 +99,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato rewardStructs = new ArrayList(); rewardStructNames = new ArrayList(); initStates = null; - formulaIdents = new Vector(); - constantIdents = new Vector(); - varIdents = new Vector(); + identUsage = new HashMap<>(); varDecls = new Vector(); varNames = new Vector(); varTypes = new Vector(); @@ -541,12 +544,28 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato } /** - * Check if an identifier is used by this model - * (as a formula, constant, or variable) + * Check if an identifier is already used somewhere in the model + * (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 + */ + private void checkAndAddIdentifier(String ident, ASTElement e) 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); + } + + /** + * Check if an identifier is already used somewhere in the model + * (as a formula, constant or variable) */ public boolean isIdentUsed(String ident) { - return formulaIdents.contains(ident) || constantIdents.contains(ident) || varIdents.contains(ident); + return identUsage.containsKey(ident); } // get individual module name @@ -669,11 +688,9 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato */ public void tidyUp() throws PrismLangException { - // Clear lists that will generated by this method + // Clear data that will be generated by this method // (in case it has already been called previously). - formulaIdents.clear(); - constantIdents.clear(); - varIdents.clear(); + identUsage.clear(); varDecls.clear(); varNames.clear(); varTypes.clear(); @@ -753,17 +770,10 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato private void checkFormulaIdents() throws PrismLangException { - int i, n; - String s; - - n = formulaList.size(); - for (i = 0; i < n; i++) { - s = formulaList.getFormulaName(i); - if (isIdentUsed(s)) { - throw new PrismLangException("Duplicated identifier \"" + s + "\"", formulaList.getFormulaNameIdent(i)); - } else { - formulaIdents.add(s); - } + int n = formulaList.size(); + for (int i = 0; i < n; i++) { + String s = formulaList.getFormulaName(i); + checkAndAddIdentifier(s, formulaList.getFormulaNameIdent(i)); } } @@ -907,18 +917,10 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato private void checkConstantIdents() throws PrismLangException { - int i, n; - String s; - - n = constantList.size(); - for (i = 0; i < n; i++) { - s = constantList.getConstantName(i); - if (isIdentUsed(s)) { - throw new PrismLangException("Duplicated identifier \"" + s + "\"", constantList - .getConstantNameIdent(i)); - } else { - constantIdents.add(s); - } + int n = constantList.size(); + for (int i = 0; i < n; i++) { + String s = constantList.getConstantName(i); + checkAndAddIdentifier(s, constantList.getConstantNameIdent(i)); } } @@ -926,42 +928,30 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato private void checkVarNames() throws PrismLangException { - int i, j, n, m; - Module module; - String s; - // compile list of all var names // and check as we go through // globals - n = getNumGlobals(); - for (i = 0; i < n; i++) { - s = getGlobal(i).getName(); - if (isIdentUsed(s)) { - throw new PrismLangException("Duplicated identifier \"" + s + "\"", getGlobal(i)); - } else { - varIdents.add(s); - varDecls.add(getGlobal(i)); - varNames.add(s); - varTypes.add(getGlobal(i).getType()); - } + int n = getNumGlobals(); + for (int i = 0; i < n; i++) { + String s = getGlobal(i).getName(); + checkAndAddIdentifier(s, getGlobal(i)); + varDecls.add(getGlobal(i)); + varNames.add(s); + varTypes.add(getGlobal(i).getType()); } // locals - n = modules.size(); - for (i = 0; i < n; i++) { - module = getModule(i); - m = module.getNumDeclarations(); - for (j = 0; j < m; j++) { - s = module.getDeclaration(j).getName(); - if (isIdentUsed(s)) { - throw new PrismLangException("Duplicated identifier \"" + s + "\"", module.getDeclaration(j)); - } else { - varIdents.add(s); - varDecls.add(module.getDeclaration(j)); - varNames.add(s); - varTypes.add(module.getDeclaration(j).getType()); - } + int numModules = modules.size(); + for (int i = 0; i < numModules; i++) { + Module module = getModule(i); + int numLocals = module.getNumDeclarations(); + for (int j = 0; j < numLocals; j++) { + String s = module.getDeclaration(j).getName(); + checkAndAddIdentifier(s, module.getDeclaration(j)); + varDecls.add(module.getDeclaration(j)); + varNames.add(s); + varTypes.add(module.getDeclaration(j).getType()); } } @@ -1393,9 +1383,7 @@ public class ModulesFile extends ASTElement implements ModelInfo, RewardGenerato if (initStates != null) ret.setInitialStates(initStates.deepCopy()); // Copy other (generated) info - ret.formulaIdents = (formulaIdents == null) ? null : (Vector)formulaIdents.clone(); - ret.constantIdents = (constantIdents == null) ? null : (Vector)constantIdents.clone(); - ret.varIdents = (varIdents == null) ? null : (Vector)varIdents.clone(); + ret.identUsage = (identUsage == null) ? null : (HashMap) identUsage.clone(); 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 f110870f..0ff51f7a 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 - // list of all identifiers used - private Vector allIdentsUsed; + // Lists of all identifiers used and where + private HashMap 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(); - allIdentsUsed = new Vector(); + identUsage = new HashMap<>(); undefinedConstantValues = null; constantValues = null; } @@ -248,22 +248,44 @@ public class PropertiesFile extends ASTElement return getPropertyObjectByName(name); } + /** + * Check if an identifier is already used somewhere here or in the model + * (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 + */ + private void checkAndAddIdentifier(String ident, ASTElement e) 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 if an identifier is used by this properties file * (as a formula or constant) */ public boolean isIdentUsed(String ident) { - return allIdentsUsed.contains(ident); + return identUsage.containsKey(ident); } // method to tidy up (called after parsing) public void tidyUp() throws PrismLangException { - // Clear lists that will generated by this method + // Clear data that will generated by this method // (in case it has already been called previously). - allIdentsUsed.clear(); + identUsage.clear(); // Check formula identifiers checkFormulaIdents(); @@ -318,20 +340,10 @@ public class PropertiesFile extends ASTElement private void checkFormulaIdents() throws PrismLangException { - int i, n; - String s; - - n = formulaList.size(); - for (i = 0; i < n; i++) { - s = formulaList.getFormulaName(i); - // see if ident has been used elsewhere - if (modulesFile.isIdentUsed(s)) { - throw new PrismLangException("Identifier \"" + s + "\" already used in model file", formulaList.getFormulaNameIdent(i)); - } else if (isIdentUsed(s)) { - throw new PrismLangException("Duplicated identifier \"" + s + "\"", formulaList.getFormulaNameIdent(i)); - } else { - allIdentsUsed.add(s); - } + int n = formulaList.size(); + for (int i = 0; i < n; i++) { + String s = formulaList.getFormulaName(i); + checkAndAddIdentifier(s, formulaList.getFormulaNameIdent(i)); } } @@ -379,21 +391,11 @@ public class PropertiesFile extends ASTElement private void checkConstantIdents() throws PrismLangException { - int i, n; - String s; - // go thru constants - n = constantList.size(); - for (i = 0; i < n; i++) { - s = constantList.getConstantName(i); - // see if ident has been used elsewhere - if (modulesFile.isIdentUsed(s)) { - throw new PrismLangException("Identifier \"" + s + "\" already used in model file", constantList.getConstantNameIdent(i)); - } else if (isIdentUsed(s)) { - throw new PrismLangException("Duplicated identifier \"" + s + "\"", constantList.getConstantNameIdent(i)); - } else { - allIdentsUsed.add(s); - } + int n = constantList.size(); + for (int i = 0; i < n; i++) { + String s = constantList.getConstantName(i); + checkAndAddIdentifier(s, constantList.getConstantNameIdent(i)); } } @@ -689,7 +691,7 @@ public class PropertiesFile extends ASTElement ret.addProperty((Property) getPropertyObject(i).deepCopy()); } // Copy other (generated) info - ret.allIdentsUsed = (allIdentsUsed == null) ? null : (Vector) allIdentsUsed.clone(); + ret.identUsage = (identUsage == null) ? null : (HashMap) identUsage.clone(); ret.constantValues = (constantValues == null) ? null : new Values(constantValues); return ret;