diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index 8a8345cd..4198306f 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/prism/src/parser/ast/ASTElement.java @@ -357,6 +357,17 @@ public abstract class ASTElement return (ASTElement) accept(visitor); } + /** + * Get all references to properties (by name) (i.e. ExpressionProp objects), store names in set. + */ + public Vector getAllProps() throws PrismLangException + { + Vector v = new Vector(); + GetAllProps visitor = new GetAllProps(v); + accept(visitor); + return v; + } + /** * Find all references to action labels, check they exist and, if required, * store their index locally (as defined by the containing ModuleFile). diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index b61bd6a6..1da798e3 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -38,22 +38,22 @@ public class PropertiesFile extends ASTElement { // Associated ModulesFile (for constants, ...) private ModulesFile modulesFile; - + // Components private FormulaList formulaList; private LabelList labelList; private LabelList combinedLabelList; // Labels from both model/here private ConstantList constantList; private Vector properties; // Properties - + // list of all identifiers used private Vector allIdentsUsed; - + // actual values of (some or all) constants private Values constantValues; - + // Constructor - + public PropertiesFile(ModulesFile mf) { setModulesFile(mf); @@ -65,32 +65,50 @@ public class PropertiesFile extends ASTElement allIdentsUsed = new Vector(); constantValues = null; } - + // Set methods - + /** Attach to a ModulesFile (so can access labels/constants etc.) */ - public void setModulesFile(ModulesFile mf) { this.modulesFile = mf; } - - public void setFormulaList(FormulaList fl) { formulaList = fl; } - - public void setLabelList(LabelList ll) { labelList = ll; } - - public void setConstantList(ConstantList cl) { constantList = cl; } - + public void setModulesFile(ModulesFile mf) + { + this.modulesFile = mf; + } + + public void setFormulaList(FormulaList fl) + { + formulaList = fl; + } + + public void setLabelList(LabelList ll) + { + labelList = ll; + } + + public void setConstantList(ConstantList cl) + { + constantList = cl; + } + public void addProperty(Property prop) { properties.add(prop); } - + public void addProperty(Expression p, String c) { properties.addElement(new Property(p, null, c)); } - - public void setPropertyObject(int i, Property prop) { properties.set(i, prop); } - - public void setPropertyExpression(int i, Expression p) { properties.get(i).setExpression(p); } - + + public void setPropertyObject(int i, Property prop) + { + properties.set(i, prop); + } + + public void setPropertyExpression(int i, Expression p) + { + properties.get(i).setExpression(p); + } + /** * Insert the contents of another PropertiesFile (just a shallow copy). */ @@ -122,27 +140,54 @@ public class PropertiesFile extends ASTElement // Need to re-tidy (some checks should be re-done, some new info created) tidyUp(); } - + // Get methods - public FormulaList getFormulaList() { return formulaList; } - - public LabelList getLabelList() { return labelList; } - - public LabelList getCombinedLabelList() { return combinedLabelList; } - - public ConstantList getConstantList() { return constantList; } - - public int getNumProperties() { return properties.size(); } - - public Property getPropertyObject(int i) { return properties.get(i); } - - public Expression getProperty(int i) { return properties.get(i).getExpression(); } - - public String getPropertyName(int i) { return properties.get(i).getName(); } - - public String getPropertyComment(int i) { return properties.get(i).getComment(); } - + public FormulaList getFormulaList() + { + return formulaList; + } + + public LabelList getLabelList() + { + return labelList; + } + + public LabelList getCombinedLabelList() + { + return combinedLabelList; + } + + public ConstantList getConstantList() + { + return constantList; + } + + public int getNumProperties() + { + return properties.size(); + } + + public Property getPropertyObject(int i) + { + return properties.get(i); + } + + public Expression getProperty(int i) + { + return properties.get(i).getExpression(); + } + + public String getPropertyName(int i) + { + return properties.get(i).getName(); + } + + public String getPropertyComment(int i) + { + return properties.get(i).getComment(); + } + /** * Look up a property by name from those listed in this properties file. * (Use {@link #lookUpPropertyObjectByName} to search model file too) @@ -159,7 +204,23 @@ public class PropertiesFile extends ASTElement } return null; } - + + /** + * Look up the index of a property by name from those listed in this properties file. + * Returns -1 if not found. + */ + public int getPropertyIndexByName(String name) + { + int i, n; + n = getNumProperties(); + for (i = 0; i < n; i++) { + if (name.equals(getPropertyName(i))) { + return i; + } + } + return -1; + } + /** * Look up a property by name, currently just locally like {@link #getPropertyObjectByName}. * Returns null if not found. @@ -168,7 +229,7 @@ public class PropertiesFile extends ASTElement { return getPropertyObjectByName(name); } - + /** * Check if an identifier is used by this properties file * (as a formula or constant) @@ -179,13 +240,13 @@ public class PropertiesFile extends ASTElement } // method to tidy up (called after parsing) - + public void tidyUp() throws PrismLangException { // Clear lists that will generated by this method // (in case it has already been called previously). allIdentsUsed.clear(); - + // Check formula identifiers checkFormulaIdents(); // Find all instances of formulas (i.e. locate idents which are formulas), @@ -198,41 +259,42 @@ public class PropertiesFile extends ASTElement formulaList.findCycles(); expandFormulas(modulesFile.getFormulaList(), false); expandFormulas(formulaList, false); - + // Check label identifiers checkLabelIdents(); - + // Check constant identifiers checkConstantIdents(); // Find all instances of constants (i.e. locate idents which are constants). // Note: We have to look in both constant lists findAllConstants(modulesFile.getConstantList()); findAllConstants(constantList); - // check constants for cyclic dependencies constantList.findCycles(); - + // Check property names checkPropertyNames(); - + // Find all instances of variables (i.e. locate idents which are variables). findAllVars(modulesFile.getVarNames(), modulesFile.getVarTypes()); - + // Find all instances of property refs findAllProps(null, this); + // Check property references for cyclic dependencies + findCyclesInPropertyReferences(); // Various semantic checks semanticCheck(modulesFile, this); // Type checking typeCheck(this); - + // Set up some values for constants // (without assuming any info about undefined constants) setSomeUndefinedConstants(null); } // check formula identifiers - + private void checkFormulaIdents() throws PrismLangException { int i, n; @@ -244,11 +306,9 @@ public class PropertiesFile extends ASTElement // 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)) { + } else if (isIdentUsed(s)) { throw new PrismLangException("Duplicated identifier \"" + s + "\"", formulaList.getFormulaNameIdent(i)); - } - else { + } else { allIdentsUsed.add(s); } } @@ -256,14 +316,14 @@ public class PropertiesFile extends ASTElement // check label identifiers // also check reference to these identifiers in properties - + 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) @@ -294,12 +354,12 @@ public class PropertiesFile extends ASTElement } // check constant identifiers - + private void checkConstantIdents() throws PrismLangException { int i, n; String s; - + // go thru constants n = constantList.size(); for (i = 0; i < n; i++) { @@ -307,11 +367,9 @@ public class PropertiesFile extends ASTElement // 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)) { + } else if (isIdentUsed(s)) { throw new PrismLangException("Duplicated identifier \"" + s + "\"", constantList.getConstantNameIdent(i)); - } - else { + } else { allIdentsUsed.add(s); } } @@ -326,7 +384,7 @@ public class PropertiesFile extends ASTElement String s; Vector propNames; LabelList mfLabels; - + // get label list from model file mfLabels = modulesFile.getLabelList(); // Go thru properties @@ -355,6 +413,73 @@ public class PropertiesFile extends ASTElement } } + /** + * Find cyclic dependencies in property references. + */ + public void findCyclesInPropertyReferences() throws PrismLangException + { + int i, j, k, l, n, firstCycle = -1; + Vector v; + boolean matrix[][]; + boolean foundCycle = false; + Expression e; + + // initialise boolean matrix + n = properties.size(); + matrix = new boolean[n][n]; + for (i = 0; i < n; i++) { + for (j = 0; j < n; j++) { + matrix[i][j] = false; + } + } + + // determine which properties reference which other properties + // and store this info in boolean matrix + for (i = 0; i < n; i++) { + e = properties.get(i).getExpression(); + v = e.getAllProps(); + for (j = 0; j < v.size(); j++) { + k = getPropertyIndexByName(v.elementAt(j)); + if (k != -1) { + matrix[i][k] = true; + } + } + } + + // check for dependencies + // (loop a maximum of n times) + // (n = max length of possible cycle) + for (i = 0; i < n; i++) { + // see if there is a cycle yet + for (j = 0; j < n; j++) { + if (matrix[j][j]) { + foundCycle = true; + firstCycle = j; + break; + } + } + // if so, stop + if (foundCycle) + break; + // extend dependencies + for (j = 0; j < n; j++) { + for (k = 0; k < n; k++) { + if (matrix[j][k]) { + for (l = 0; l < n; l++) { + matrix[j][l] |= matrix[k][l]; + } + } + } + } + } + + // report dependency + if (foundCycle) { + String s = "Cyclic dependency in property references from property \"" + getPropertyName(firstCycle) + "\""; + throw new PrismLangException(s, getPropertyObject(firstCycle)); + } + } + /** * Get a list of all undefined constants in the properties files * ("const int x;" rather than "const int x = 1;") @@ -363,7 +488,7 @@ public class PropertiesFile extends ASTElement { return constantList.getUndefinedConstants(); } - + /** * Get a list of undefined (properties file) constants appearing in labels of the properties file * (including those that appear in definitions of other needed constants) @@ -387,7 +512,7 @@ public class PropertiesFile extends ASTElement } return consts; } - + /** * Get a list of undefined (properties file) constants used in a property * (including those that appear in definitions of other needed constants and labels/properties) @@ -397,13 +522,13 @@ public class PropertiesFile extends ASTElement { return prop.getExpression().getAllUndefinedConstantsRecursively(constantList, combinedLabelList, this); } - + /** * Get a list of undefined (properties file) constants used in a list of properties * (including those that appear in definitions of other needed constants and labels/properties) * (undefined constants are those of form "const int x;" rather than "const int x = 1;") */ - public Vector getUndefinedConstantsUsedInProperties(List props) + public Vector getUndefinedConstantsUsedInProperties(List props) { Vector consts, tmp; consts = new Vector(); @@ -417,7 +542,7 @@ public class PropertiesFile extends ASTElement } return consts; } - + /** * Set values for *all* undefined constants and then evaluate all constants. * If there are no undefined constants, {@code someValues} can be null. @@ -432,7 +557,7 @@ public class PropertiesFile extends ASTElement // This will usually be done on a per-property basis later // (and sometimes we don't want to have to define all constants) } - + /** * Set values for *some* undefined constants and then evaluate all constants where possible. * If there are no undefined constants, {@code someValues} can be null. @@ -447,7 +572,7 @@ public class PropertiesFile extends ASTElement // This will usually be done on a per-property basis later // (and sometimes we don't want to have to define all constants) } - + /** * Check if {@code name} is a *defined* constant in the properties file, * i.e. a constant whose value was *not* left unspecified. @@ -456,7 +581,7 @@ public class PropertiesFile extends ASTElement { return constantList.isDefinedConstant(name); } - + /** * Get access to the values for all constants in the properties file, including the * undefined constants set previously via the method {@link #setUndefinedConstants(Values)} @@ -469,7 +594,7 @@ public class PropertiesFile extends ASTElement } // Methods required for ASTElement: - + /** * Visitor method. */ @@ -477,7 +602,7 @@ public class PropertiesFile extends ASTElement { return v.visit(this); } - + /** * Convert to string. */ @@ -485,28 +610,32 @@ public class PropertiesFile extends ASTElement { String s = "", tmp; int i, n; - + tmp = "" + formulaList; - if (tmp.length() > 0) tmp += "\n"; + if (tmp.length() > 0) + tmp += "\n"; s += tmp; - + tmp = "" + labelList; - if (tmp.length() > 0) tmp += "\n"; + if (tmp.length() > 0) + tmp += "\n"; s += tmp; - + tmp = "" + constantList; - if (tmp.length() > 0) tmp += "\n"; + if (tmp.length() > 0) + tmp += "\n"; s += tmp; - + n = getNumProperties(); for (i = 0; i < n; i++) { s += getPropertyObject(i) + ";\n"; - if (i < n-1) s += "\n"; + if (i < n - 1) + s += "\n"; } - + return s; } - + /** * Perform a deep copy. */ @@ -527,9 +656,9 @@ public class PropertiesFile extends ASTElement ret.addProperty((Property) getPropertyObject(i).deepCopy()); } // Copy other (generated) info - ret.allIdentsUsed = (allIdentsUsed == null) ? null : (Vector)allIdentsUsed.clone(); + ret.allIdentsUsed = (allIdentsUsed == null) ? null : (Vector) allIdentsUsed.clone(); ret.constantValues = (constantValues == null) ? null : new Values(constantValues); - + return ret; } } diff --git a/prism/src/parser/visitor/GetAllProps.java b/prism/src/parser/visitor/GetAllProps.java new file mode 100644 index 00000000..fcba8599 --- /dev/null +++ b/prism/src/parser/visitor/GetAllProps.java @@ -0,0 +1,53 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// 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.visitor; + +import java.util.Vector; + +import parser.ast.*; +import prism.PrismLangException; + +/** + * Get all references to properties (by name) (i.e. ExpressionProp objects), store names in set. + */ +public class GetAllProps extends ASTTraverse +{ + private Vector v; + + public GetAllProps(Vector v) + { + this.v = v; + } + + public void visitPost(ExpressionProp e) throws PrismLangException + { + if (!v.contains(e.getName())) { + v.addElement(e.getName()); + } + } +} +