Check for cyclic dependencies in property references.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4501 bbc10eb1-c90d-0410-af57-cb519fbb1720

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<String> getAllProps() throws PrismLangException
+	{
+		Vector<String> v = new Vector<String>();
+		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).

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<Property> properties; // Properties
-	
+
 	// list of all identifiers used
 	private Vector<String> 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<String>();
 		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<String> 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<String> 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<String> 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<String> getUndefinedConstantsUsedInProperties(List <Property> props)
+	public Vector<String> getUndefinedConstantsUsedInProperties(List<Property> props)
 	{
 		Vector<String> consts, tmp;
 		consts = new Vector<String>();
@@ -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<String>)allIdentsUsed.clone();
+		ret.allIdentsUsed = (allIdentsUsed == null) ? null : (Vector<String>) allIdentsUsed.clone();
 		ret.constantValues = (constantValues == null) ? null : new Values(constantValues);
-		
+
 		return ret;
 	}
 }

prism/src/parser/visitor/GetAllProps.java

@@ -0,0 +1,53 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (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<String> v;
+	
+	public GetAllProps(Vector<String> v)
+	{
+		this.v = v;
+	}
+	
+	public void visitPost(ExpressionProp e) throws PrismLangException
+	{
+		if (!v.contains(e.getName())) {
+			v.addElement(e.getName());
+		}
+	}
+}
+