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

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

prism/src/parser/ast/SystemBrackets.java

@@ -93,6 +93,12 @@ public class SystemBrackets extends SystemDefn
 		operand.getSynchs(v, modulesFile);
 	}
 	
+	@Override
+	public void getReferences(Vector<String> v)
+	{
+		operand.getReferences(v);
+	}
+	
 	// Methods required for ASTElement:
 	
 	@Override

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<String> v, ModulesFile modulesFile);
+
+	/**
+	 * Get list of all references to other SystemDefns (recursively, but not following references).
+	 */
+	public abstract void getReferences(Vector<String> v);
 }
 
 //------------------------------------------------------------------------------

prism/src/parser/ast/SystemFullParallel.java

@@ -115,6 +115,15 @@ public class SystemFullParallel extends SystemDefn
 		}
 	}
 	
+	@Override
+	public void getReferences(Vector<String> v)
+	{
+		int n = getNumOperands();
+		for (int i = 0; i < n; i++) {
+			getOperand(i).getReferences(v);
+		}
+	}
+	
 	// Methods required for ASTElement:
 	
 	@Override

prism/src/parser/ast/SystemHide.java

@@ -120,6 +120,12 @@ public class SystemHide extends SystemDefn
 		operand.getSynchs(v, modulesFile);
 	}
 	
+	@Override
+	public void getReferences(Vector<String> v)
+	{
+		operand.getReferences(v);
+	}
+	
 	// Methods required for ASTElement:
 	
 	@Override

prism/src/parser/ast/SystemInterleaved.java

@@ -115,6 +115,15 @@ public class SystemInterleaved extends SystemDefn
 		}
 	}
 	
+	@Override
+	public void getReferences(Vector<String> v)
+	{
+		int n = getNumOperands();
+		for (int i = 0; i < n; i++) {
+			getOperand(i).getReferences(v);
+		}
+	}
+	
 	// Methods required for ASTElement:
 	
 	@Override

prism/src/parser/ast/SystemModule.java

@@ -87,6 +87,12 @@ public class SystemModule extends SystemDefn
 		// do nothing
 	}
 	
+	@Override
+	public void getReferences(Vector<String> v)
+	{
+		// do nothing
+	}
+	
 	// Methods required for ASTElement:
 	
 	@Override

prism/src/parser/ast/SystemParallel.java

@@ -134,6 +134,13 @@ public class SystemParallel extends SystemDefn
 		operand2.getSynchs(v, modulesFile);
 	}
 	
+	@Override
+	public void getReferences(Vector<String> v)
+	{
+		operand1.getReferences(v);
+		operand2.getReferences(v);
+	}
+	
 	// Methods required for ASTElement:
 	
 	@Override

prism/src/parser/ast/SystemReference.java

@@ -91,6 +91,13 @@ public class SystemReference extends SystemDefn
 		}
 	}
 	
+	@Override
+	public void getReferences(Vector<String> v)
+	{
+		if (!v.contains(name))
+			v.add(name);
+	}
+	
 	// Methods required for ASTElement:
 	
 	@Override

prism/src/parser/ast/SystemRename.java

@@ -102,9 +102,8 @@ public class SystemRename extends SystemDefn
 		i = from.indexOf(s);
 		if (i == -1) {
 			return s;
-		}
-		else {
-			return (String)to.elementAt(i);
+		} else {
+			return (String) to.elementAt(i);
 		}
 	}
 
@@ -136,7 +135,8 @@ public class SystemRename extends SystemDefn
 		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
@@ -155,13 +155,20 @@ public class SystemRename extends SystemDefn
 		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<String> v)
+	{
+		operand.getReferences(v);
+	}
+
 	// Methods required for ASTElement:
 
 	@Override
@@ -178,11 +185,11 @@ public class SystemRename extends SystemDefn
 
 		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 + "}";