From 3ef803f384085fe1170cad037757f2c80b456ecf Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 25 Jun 2014 21:19:57 +0000 Subject: [PATCH] Re-factor code to detect cycles in dependencies. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8600 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/ConstantList.java | 64 +++++------------------ prism/src/parser/ast/FormulaList.java | 62 +++++----------------- prism/src/parser/ast/PropertiesFile.java | 65 +++++------------------- prism/src/prism/PrismUtils.java | 37 ++++++++++++++ 4 files changed, 75 insertions(+), 153 deletions(-) diff --git a/prism/src/parser/ast/ConstantList.java b/prism/src/parser/ast/ConstantList.java index 57f097fd..533c1d7c 100644 --- a/prism/src/parser/ast/ConstantList.java +++ b/prism/src/parser/ast/ConstantList.java @@ -31,6 +31,7 @@ import java.util.Vector; import parser.*; import parser.visitor.*; import prism.PrismLangException; +import prism.PrismUtils; import parser.type.*; /** @@ -112,64 +113,25 @@ public class ConstantList extends ASTElement */ public void findCycles() throws PrismLangException { - int i, j, k, l, n, firstCycle = -1; - Vector v; - boolean matrix[][]; - boolean foundCycle = false; - Expression e; - - // initialise boolean matrix - n = constants.size(); - matrix = new boolean[n][n]; - for (i = 0; i < n; i++) { - for (j = 0; j < n; j++) { - matrix[i][j] = false; - } - } - - // determine which constants contain which other constants - // and store this info in boolean matrix - for (i = 0; i < n; i++) { - e = getConstant(i); + // Create boolean matrix of dependencies + // (matrix[i][j] is true if constant i contains constant j) + int n = constants.size(); + boolean matrix[][] = new boolean[n][n]; + for (int i = 0; i < n; i++) { + Expression e = getConstant(i); if (e != null) { - v = e.getAllConstants(); - for (j = 0; j < v.size(); j++) { - k = getConstantIndex(v.elementAt(j)); + Vector v = e.getAllConstants(); + for (int j = 0; j < v.size(); j++) { + int k = getConstantIndex(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) { + // Check for and report dependencies + int firstCycle = PrismUtils.findCycle(matrix); + if (firstCycle != -1) { String s = "Cyclic dependency in definition of constant \"" + getConstantName(firstCycle) + "\""; throw new PrismLangException(s, getConstant(firstCycle)); } diff --git a/prism/src/parser/ast/FormulaList.java b/prism/src/parser/ast/FormulaList.java index 20e06145..f7cd1550 100644 --- a/prism/src/parser/ast/FormulaList.java +++ b/prism/src/parser/ast/FormulaList.java @@ -30,6 +30,7 @@ import java.util.Vector; import parser.visitor.*; import prism.PrismLangException; +import prism.PrismUtils; // class to store list of formulas @@ -106,61 +107,22 @@ public class FormulaList extends ASTElement */ public void findCycles() throws PrismLangException { - int i, j, k, l, n, firstCycle = -1; - Vector v; - boolean matrix[][]; - boolean foundCycle = false; - - // initialise boolean matrix - n = size(); - matrix = new boolean[n][n]; - for (i = 0; i < n; i++) { - for (j = 0; j < n; j++) { - matrix[i][j] = false; - } - } - - // determine which formulas contain which other formulas - // and store this info in boolean matrix - for (i = 0; i < n; i++) { - v = getFormula(i).getAllFormulas(); - for (j = 0; j < v.size(); j++) { - k = getFormulaIndex((String) v.elementAt(j)); + // Create boolean matrix of dependencies + // (matrix[i][j] is true if formula i contains formula j) + int n = size(); + boolean matrix[][] = new boolean[n][n]; + for (int i = 0; i < n; i++) { + Vector v = getFormula(i).getAllFormulas(); + for (int j = 0; j < v.size(); j++) { + int k = getFormulaIndex((String) 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) { + // Check for and report dependencies + int firstCycle = PrismUtils.findCycle(matrix); + if (firstCycle != -1) { String s = "Cyclic dependency in definition of formula \"" + getFormulaName(firstCycle) + "\""; throw new PrismLangException(s, getFormula(firstCycle)); } diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 996a53f6..6694c367 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -31,6 +31,7 @@ import java.util.*; import parser.*; import parser.visitor.*; import prism.PrismLangException; +import prism.PrismUtils; // Class representing parsed properties file/list @@ -418,63 +419,23 @@ public class PropertiesFile extends ASTElement */ 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.getAllPropRefs(); - for (j = 0; j < v.size(); j++) { - k = getPropertyIndexByName(v.elementAt(j)); + // Create boolean matrix of dependencies + // (matrix[i][j] is true if prop i contains a ref to prop j) + int n = properties.size(); + boolean matrix[][] = new boolean[n][n]; + for (int i = 0; i < n; i++) { + Expression e = properties.get(i).getExpression(); + Vector v = e.getAllPropRefs(); + for (int j = 0; j < v.size(); j++) { + int 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) { + // Check for and report dependencies + int firstCycle = PrismUtils.findCycle(matrix); + if (firstCycle != -1) { String s = "Cyclic dependency in property references from property \"" + getPropertyName(firstCycle) + "\""; throw new PrismLangException(s, getPropertyObject(firstCycle)); } diff --git a/prism/src/prism/PrismUtils.java b/prism/src/prism/PrismUtils.java index d42d7e69..7f7e2649 100644 --- a/prism/src/prism/PrismUtils.java +++ b/prism/src/prism/PrismUtils.java @@ -246,6 +246,43 @@ public class PrismUtils } return s; } + + /** + * Check for any cycles in an 2D boolean array representing a graph. + * Useful for checking for cyclic dependencies in connected definitions. + * Returns the lowest index of a node contained in a cycle, if there is one, -1 if not. + * @param matrix Square matrix of connections: {@code matr[i][j] == true} iff + * there is a connection from {@code i} to {@code j}. + */ + public static int findCycle(boolean matrix[][]) + { + int n = matrix.length; + int firstCycle = -1; + // Go through nodes + for (int i = 0; i < n; i++) { + // See if there is a cycle yet + for (int j = 0; j < n; j++) { + if (matrix[j][j]) { + firstCycle = j; + break; + } + } + // If so, stop + if (firstCycle != -1) + break; + // Extend dependencies + for (int j = 0; j < n; j++) { + for (int k = 0; k < n; k++) { + if (matrix[j][k]) { + for (int l = 0; l < n; l++) { + matrix[j][l] |= matrix[k][l]; + } + } + } + } + } + return firstCycle; + } } //------------------------------------------------------------------------------