From 8611094d95aef5830d0f3c7c0ed6971a2adefd44 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 26 Jun 2014 09:05:29 +0000 Subject: [PATCH] Check for cyclic dependencies in system...endsystem references. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8602 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/ModulesFile.java | 62 +++++++++++++---- prism/src/parser/ast/SystemBrackets.java | 6 ++ prism/src/parser/ast/SystemDefn.java | 5 ++ prism/src/parser/ast/SystemFullParallel.java | 9 +++ prism/src/parser/ast/SystemHide.java | 6 ++ prism/src/parser/ast/SystemInterleaved.java | 9 +++ prism/src/parser/ast/SystemModule.java | 6 ++ prism/src/parser/ast/SystemParallel.java | 7 ++ prism/src/parser/ast/SystemReference.java | 7 ++ prism/src/parser/ast/SystemRename.java | 71 +++++++++++--------- 10 files changed, 144 insertions(+), 44 deletions(-) diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 6b14dd0c..479d8cff 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -32,6 +32,7 @@ import parser.*; import parser.visitor.*; import prism.PrismLangException; import prism.ModelType; +import prism.PrismUtils; import parser.type.*; // Class representing parsed model file @@ -337,20 +338,30 @@ public class ModulesFile extends ASTElement } /** - * Get a "system...endsystem" construct by its name. + * Get the index of a "system...endsystem" construct by its name (indexed from 0). * Passing null for the name looks up an un-named construct. * Returns null if the requested construct does not exist. */ - public SystemDefn getSystemDefnByName(String name) + public int getSystemDefnIndex(String name) { - int i, n; - n = systemDefns.size(); - for (i = 0; i < n; i++) { + int n = systemDefns.size(); + for (int i = 0; i < n; i++) { String s = systemDefnNames.get(i); if ((s == null && name == null) || (s != null && s.equals(name))) - return systemDefns.get(i); + return i; } - return null; + return -1; + } + + /** + * Get a "system...endsystem" construct by its name. + * Passing null for the name looks up an un-named construct. + * Returns null if the requested construct does not exist. + */ + public SystemDefn getSystemDefnByName(String name) + { + int i = getSystemDefnIndex(name); + return i == -1 ? null : getSystemDefn(i); } /** @@ -580,11 +591,6 @@ public class ModulesFile extends ASTElement // Check module names checkModuleNames(); - // Get synchronising action names - getSynchNames(); - // Then identify/check any references to action names - findAllActions(synchs); - // Check constant identifiers checkConstantIdents(); // Find all instances of constants @@ -608,6 +614,12 @@ public class ModulesFile extends ASTElement // Check "system...endsystem" constructs checkSystemDefns(); + // Get synchronising action names + // (NB: Do this *after* checking for cycles in system defns above) + getSynchNames(); + // Then identify/check any references to action names + findAllActions(synchs); + // Various semantic checks semanticCheck(this); // Type checking @@ -860,6 +872,9 @@ public class ModulesFile extends ASTElement private void checkSystemDefns() throws PrismLangException { int n = systemDefns.size(); + + // Check there is a most one un-named system...endsystem... + // None is ok if (n == 0) return; @@ -878,6 +893,29 @@ public class ModulesFile extends ASTElement if (numUnnamed > 1) throw new PrismLangException("There can be at most one un-named system...endsystem construct", getSystemDefn(i)); } + + // Check for cyclic dependencies... + + // Create boolean matrix of dependencies + // (matrix[i][j] is true if prop i contains a ref to prop j) + boolean matrix[][] = new boolean[n][n]; + for (int i = 0; i < n; i++) { + SystemDefn sys = systemDefns.get(i); + Vector v = new Vector<>(); + sys.getReferences(v); + for (int j = 0; j < v.size(); j++) { + int k = getSystemDefnIndex(v.elementAt(j)); + if (k != -1) { + matrix[i][k] = true; + } + } + } + // Check for and report dependencies + int firstCycle = PrismUtils.findCycle(matrix); + if (firstCycle != -1) { + String s = "Cyclic dependency from references in system...endsystem definition \"" + getSystemDefnName(firstCycle) + "\""; + throw new PrismLangException(s, getSystemDefn(firstCycle)); + } } /** diff --git a/prism/src/parser/ast/SystemBrackets.java b/prism/src/parser/ast/SystemBrackets.java index e8102d93..abd1ceea 100644 --- a/prism/src/parser/ast/SystemBrackets.java +++ b/prism/src/parser/ast/SystemBrackets.java @@ -93,6 +93,12 @@ public class SystemBrackets extends SystemDefn operand.getSynchs(v, modulesFile); } + @Override + public void getReferences(Vector v) + { + operand.getReferences(v); + } + // Methods required for ASTElement: @Override diff --git a/prism/src/parser/ast/SystemDefn.java b/prism/src/parser/ast/SystemDefn.java index 5485b92b..e52938dc 100644 --- a/prism/src/parser/ast/SystemDefn.java +++ b/prism/src/parser/ast/SystemDefn.java @@ -64,6 +64,11 @@ public abstract class SystemDefn extends ASTElement * Get list of all synchronising actions _introduced_ (recursively, including descent into references). */ public abstract void getSynchs(Vector v, ModulesFile modulesFile); + + /** + * Get list of all references to other SystemDefns (recursively, but not following references). + */ + public abstract void getReferences(Vector v); } //------------------------------------------------------------------------------ diff --git a/prism/src/parser/ast/SystemFullParallel.java b/prism/src/parser/ast/SystemFullParallel.java index 140a7c15..8b4ef701 100644 --- a/prism/src/parser/ast/SystemFullParallel.java +++ b/prism/src/parser/ast/SystemFullParallel.java @@ -115,6 +115,15 @@ public class SystemFullParallel extends SystemDefn } } + @Override + public void getReferences(Vector v) + { + int n = getNumOperands(); + for (int i = 0; i < n; i++) { + getOperand(i).getReferences(v); + } + } + // Methods required for ASTElement: @Override diff --git a/prism/src/parser/ast/SystemHide.java b/prism/src/parser/ast/SystemHide.java index 8d0e1c38..c8931b65 100644 --- a/prism/src/parser/ast/SystemHide.java +++ b/prism/src/parser/ast/SystemHide.java @@ -120,6 +120,12 @@ public class SystemHide extends SystemDefn operand.getSynchs(v, modulesFile); } + @Override + public void getReferences(Vector v) + { + operand.getReferences(v); + } + // Methods required for ASTElement: @Override diff --git a/prism/src/parser/ast/SystemInterleaved.java b/prism/src/parser/ast/SystemInterleaved.java index 41a40b15..193a916e 100644 --- a/prism/src/parser/ast/SystemInterleaved.java +++ b/prism/src/parser/ast/SystemInterleaved.java @@ -115,6 +115,15 @@ public class SystemInterleaved extends SystemDefn } } + @Override + public void getReferences(Vector v) + { + int n = getNumOperands(); + for (int i = 0; i < n; i++) { + getOperand(i).getReferences(v); + } + } + // Methods required for ASTElement: @Override diff --git a/prism/src/parser/ast/SystemModule.java b/prism/src/parser/ast/SystemModule.java index 70085c5f..b5d40aa0 100644 --- a/prism/src/parser/ast/SystemModule.java +++ b/prism/src/parser/ast/SystemModule.java @@ -87,6 +87,12 @@ public class SystemModule extends SystemDefn // do nothing } + @Override + public void getReferences(Vector v) + { + // do nothing + } + // Methods required for ASTElement: @Override diff --git a/prism/src/parser/ast/SystemParallel.java b/prism/src/parser/ast/SystemParallel.java index 9ed0d52e..383a242c 100644 --- a/prism/src/parser/ast/SystemParallel.java +++ b/prism/src/parser/ast/SystemParallel.java @@ -134,6 +134,13 @@ public class SystemParallel extends SystemDefn operand2.getSynchs(v, modulesFile); } + @Override + public void getReferences(Vector v) + { + operand1.getReferences(v); + operand2.getReferences(v); + } + // Methods required for ASTElement: @Override diff --git a/prism/src/parser/ast/SystemReference.java b/prism/src/parser/ast/SystemReference.java index 5ba1a3f5..1312ab5b 100644 --- a/prism/src/parser/ast/SystemReference.java +++ b/prism/src/parser/ast/SystemReference.java @@ -91,6 +91,13 @@ public class SystemReference extends SystemDefn } } + @Override + public void getReferences(Vector v) + { + if (!v.contains(name)) + v.add(name); + } + // Methods required for ASTElement: @Override diff --git a/prism/src/parser/ast/SystemRename.java b/prism/src/parser/ast/SystemRename.java index d7f92065..ce03b9c7 100644 --- a/prism/src/parser/ast/SystemRename.java +++ b/prism/src/parser/ast/SystemRename.java @@ -38,78 +38,77 @@ public class SystemRename extends SystemDefn // Vectors for pairs of actions to be renamed private Vector from; private Vector to; - + // Constructors - + public SystemRename() { from = new Vector(); to = new Vector(); } - + public SystemRename(SystemDefn s) { operand = s; from = new Vector(); to = new Vector(); } - + // Set methods - + public void setOperand(SystemDefn s) { operand = s; } - + public void addRename(String s1, String s2) { from.addElement(s1); to.addElement(s2); } - + public void setRename(int i, String s1, String s2) { from.setElementAt(s1, i); to.setElementAt(s2, i); } - + // Get methods - + public SystemDefn getOperand() { return operand; } - + public int getNumRenames() { return from.size(); } - + public String getFrom(int i) { return from.elementAt(i); } - + public String getTo(int i) { return to.elementAt(i); } - + public String getNewName(String s) { int i; - + i = from.indexOf(s); if (i == -1) { return s; - } - else { - return (String)to.elementAt(i); + } else { + return (String) to.elementAt(i); } } - + // Methods required for SystemDefn (all subclasses should implement): - + @Override @SuppressWarnings("deprecation") public void getModules(Vector v) @@ -129,16 +128,17 @@ public class SystemRename extends SystemDefn { int i, n; String s; - + // add action names in renames // (only look in 'to' vector because we're only // interested in actions _introduced_) n = getNumRenames(); for (i = 0; i < n; i++) { s = getTo(i); - if (!(v.contains(s))) v.addElement(s); + if (!(v.contains(s))) + v.addElement(s); } - + // recurse operand.getSynchs(v); } @@ -148,47 +148,54 @@ public class SystemRename extends SystemDefn { int i, n; String s; - + // add action names in renames // (only look in 'to' vector because we're only // interested in actions _introduced_) n = getNumRenames(); for (i = 0; i < n; i++) { s = getTo(i); - if (!(v.contains(s))) v.addElement(s); + if (!(v.contains(s))) + v.addElement(s); } - + // recurse operand.getSynchs(v, modulesFile); } + @Override + public void getReferences(Vector v) + { + operand.getReferences(v); + } + // Methods required for ASTElement: - + @Override public Object accept(ASTVisitor v) throws PrismLangException { return v.visit(this); } - + @Override public String toString() { int i, n; String s = ""; - + s = s + operand + "{"; n = getNumRenames(); - for (i = 0; i < n-1; i++) { + for (i = 0; i < n - 1; i++) { s = s + getFrom(i) + "<-" + getTo(i) + ","; } if (n > 0) { - s = s + getFrom(n-1) + "<-" + getTo(n-1); + s = s + getFrom(n - 1) + "<-" + getTo(n - 1); } s = s + "}"; - + return s; } - + @Override public SystemDefn deepCopy() {