s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Refactoring of code to store/check identifiers used in model/properties files.

accumulation-v4.7
Dave Parker 7 years ago
parent
4fd6dfa7c7
commit
acee7edc5c
2 changed files with 100 additions and 110 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 138
      prism/src/parser/ast/ModulesFile.java
  2. 72
      prism/src/parser/ast/PropertiesFile.java

138
prism/src/parser/ast/ModulesFile.java
View File

@ -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<String> rewardStructNames; // Names of reward structures
private Expression initStates; // Initial states specification
// Lists of all identifiers used
private Vector<String> formulaIdents;
private Vector<String> constantIdents;
private Vector<String> varIdents; // TODO: don't need?
// Lists of all identifiers used and where
private HashMap<String, ASTElement> 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<RewardStruct>();
rewardStructNames = new ArrayList<String>();
initStates = null;
formulaIdents = new Vector<String>();
constantIdents = new Vector<String>();
varIdents = new Vector<String>();
identUsage = new HashMap<>();
varDecls = new Vector<Declaration>();
varNames = new Vector<String>();
varTypes = new Vector<Type>();
@ -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<String>)formulaIdents.clone();
ret.constantIdents = (constantIdents == null) ? null : (Vector<String>)constantIdents.clone();
ret.varIdents = (varIdents == null) ? null : (Vector<String>)varIdents.clone();
ret.identUsage = (identUsage == null) ? null : (HashMap<String, ASTElement>) identUsage.clone();
ret.moduleNames = (moduleNames == null) ? null : moduleNames.clone();
ret.synchs = (synchs == null) ? null : (Vector<String>)synchs.clone();
if (varDecls != null) {

72
prism/src/parser/ast/PropertiesFile.java
View File

@ -49,8 +49,8 @@ public class PropertiesFile extends ASTElement
private ConstantList constantList;
private Vector<Property> properties; // Properties
// list of all identifiers used
private Vector<String> allIdentsUsed;
// Lists of all identifiers used and where
private HashMap<String, ASTElement> 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<Property>();
allIdentsUsed = new Vector<String>();
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<String>) allIdentsUsed.clone();
ret.identUsage = (identUsage == null) ? null : (HashMap<String, ASTElement>) identUsage.clone();
ret.constantValues = (constantValues == null) ? null : new Values(constantValues);
return ret;

Write Preview
Loading…
Cancel
Save