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

Refactor/improve processing of identifier usage in model/properties. 

Implementation pushed into a helper class IdentUsage,
used in both ModulesFile and PropertiesFile.

Also, slightly improve error messages for identifier clashes
(say where the original use was, e.g. "constant").

Also, add isIdentUsed and checkIdent to ModelInfo, with default implementations.
This removes another dependency of PropertiesFile on ModulesFile.
accumulation-v4.7
Dave Parker 5 years ago
parent
2cea964adf
commit
616dd47fb2
4 changed files with 186 additions and 42 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. 114
      prism/src/parser/IdentUsage.java
  2. 46
      prism/src/parser/ast/ModulesFile.java
  3. 35
      prism/src/parser/ast/PropertiesFile.java
  4. 33
      prism/src/prism/ModelInfo.java

114
prism/src/parser/IdentUsage.java
View File

@ -0,0 +1,114 @@
//==============================================================================
//
// Copyright (c) 2021-
// Authors:
// * Dave Parker <d.a.parker@cs.bham.ac.uk> (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<String, ASTElement> identDecls;
// Uses of identifiers (e.g. "constant")
private HashMap<String, String> identUses;
// Location of identifiers (e.g. "the model")
private HashMap<String, String> 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<String, ASTElement>) identDecls.clone();
return ret;
}
}

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

@ -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<String> obsVars;
// Lists of all identifiers used and where
private HashMap<String, ASTElement> 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<String>();
identUsage = new HashMap<>();
identUsage = new IdentUsage();
varDecls = new Vector<Declaration>();
varNames = new Vector<String>();
varTypes = new Vector<Type>();
@ -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<String, ASTElement>) identUsage.clone();
ret.identUsage = (identUsage == null) ? null : identUsage.deepCopy();
ret.moduleNames = (moduleNames == null) ? null : moduleNames.clone();
ret.synchs = (synchs == null) ? null : (Vector<String>)synchs.clone();
if (varDecls != null) {

35
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
// Lists of all identifiers used and where
private HashMap<String, ASTElement> 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<Property>();
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<String, ASTElement>) identUsage.clone();
ret.identUsage = (identUsage == null) ? null : identUsage.deepCopy();
ret.constantValues = (constantValues == null) ? null : new Values(constantValues);
return ret;

33
prism/src/prism/ModelInfo.java
View File

@ -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);
}
}
}
Write Preview
Loading…
Cancel
Save