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

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
master
Dave Parker 12 years ago
parent
9e2c117954
commit
3ef803f384
4 changed files with 75 additions and 153 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. 64
      prism/src/parser/ast/ConstantList.java
  2. 62
      prism/src/parser/ast/FormulaList.java
  3. 65
      prism/src/parser/ast/PropertiesFile.java
  4. 37
      prism/src/prism/PrismUtils.java

64
prism/src/parser/ast/ConstantList.java
View File

@ -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<String> 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<String> 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));
}

62
prism/src/parser/ast/FormulaList.java
View File

@ -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<String> 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<String> 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));
}

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

@ -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<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.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<String> 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));
}

37
prism/src/prism/PrismUtils.java
View File

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