Added parse-time checks for illegal updates (synch+global or non-local).

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

prism/src/parser/Command.java

@@ -29,10 +29,16 @@ import apmc.*;
 
 public class Command
 {
+	// action label
 	String synch;
+	// reward (defunct)
 	Expression reward;
+	// guard
 	Expression guard;
+	// list of updates
 	Updates updates;
+	// parent Module
+	Module parent;
 	
 	// constructor
 	
@@ -67,6 +73,11 @@ public class Command
 		u.setParent(this);
 	}
 	
+	public void setParent(Module m)
+	{
+		parent = m;
+	}
+
 	// get methods
 
 	public String getSynch()
@@ -89,6 +100,11 @@ public class Command
 		return updates;
 	}
 	
+	public Module getParent()
+	{
+		return parent;
+	}
+	
 	// find all formulas (i.e. locate idents which are formulas)
 	
 	public void findAllFormulas(FormulaList formulaList) throws PrismException

prism/src/parser/Module.java

@@ -29,9 +29,15 @@ import apmc.*;
 
 public class Module
 {
+	// module name
 	private String name;
+	// local variables
 	private Vector decls;
+	// commands
 	private Vector commands;
+	// parent ModulesFile
+	private ModulesFile parent;
+	// list of all action labels used
 	private Vector allSynchs;
 
 	// constructor
@@ -63,6 +69,12 @@ public class Module
 		commands.addElement(c);
 		s = c.getSynch();
 		if (!s.equals("")) if (!allSynchs.contains(s)) allSynchs.add(s);
+		c.setParent(this);
+	}
+	
+	public void setParent(ModulesFile mf)
+	{
+		parent = mf;
 	}
 
 	// get methods
@@ -92,6 +104,11 @@ public class Module
 		return (Command)commands.elementAt(i);
 	}
 	
+	public ModulesFile getParent()
+	{
+		return parent;
+	}
+	
 	public Vector getAllSynchs()
 	{
 		return allSynchs;
@@ -102,6 +119,17 @@ public class Module
 		return allSynchs.contains(s);
 	}
 	
+	public boolean isLocalVariable(String s)
+	{
+		int i, n;
+		
+		n = getNumDeclarations();
+		for (i = 0; i < n; i++) {
+			if (getDeclaration(i).getName().equals(s)) return true;
+		}
+		return false;
+	}
+
 	// find all formulas (i.e. locate idents which are formulas)
 	
 	public void findAllFormulas(FormulaList formulaList) throws PrismException

prism/src/parser/ModulesFile.java

@@ -90,7 +90,7 @@ public class ModulesFile
 	
 	public void addGlobal(Declaration d) { globals.addElement(d); }
 	
-	public void addModule(Module m) { modules.addElement(m); }
+	public void addModule(Module m) { modules.addElement(m); m.setParent(this); }
 	
 	public void addRenamedModule(RenamedModule m) { modules.addElement(m); }
 	
@@ -163,6 +163,17 @@ public class ModulesFile
 	
 	public Vector getVarTypes() { return varTypes; }
 	
+	public boolean isGlobalVariable(String s)
+	{
+		int i, n;
+		
+		n = getNumGlobals();
+		for (i = 0; i < n; i++) {
+			if (getGlobal(i).getName().equals(s)) return true;
+		}
+		return false;
+	}
+
 	// method to tidy up
 	// (called after parsing to do some checks and extract some information)
 	
@@ -297,7 +308,7 @@ public class ModulesFile
 	{
 		int i, j, n;
 		RenamedModule module;
-		Module baseModule;
+		Module baseModule, newModule;
 		String s;
 		Object o;
 		
@@ -316,7 +327,9 @@ public class ModulesFile
 			}
 			baseModule = getModule(j);
 			// then do renaming and replace with new module
-			modules.setElementAt(baseModule.rename(module), i);
+			newModule = baseModule.rename(module);
+			modules.setElementAt(newModule, i);
+			newModule.setParent(this);
 		}
 	}
 	

prism/src/parser/Update.java

@@ -29,9 +29,12 @@ import apmc.*;
 
 public class Update
 {
+	// list of variable/expression pairs (and types)
 	Vector vars;
 	Vector exprs;
 	Vector types;
+	// parent Updates object
+	Updates parent;
 	
 	// constructor
 	
@@ -50,6 +53,13 @@ public class Update
 		exprs.addElement(e);
 	}
 	
+	// set parent
+	
+	public void setParent(Updates u)
+	{
+		parent = u;
+	}
+	
 	// get methods
 	
 	public int getNumElements()
@@ -72,6 +82,11 @@ public class Update
 		return ((Integer)types.elementAt(i)).intValue();
 	}
 	
+	public Updates getParent()
+	{
+		return parent;
+	}
+	
 	// find all formulas (i.e. locate idents which are formulas)
 	
 	public void findAllFormulas(FormulaList formulaList) throws PrismException
@@ -160,16 +175,40 @@ public class Update
 	public void check() throws PrismException
 	{
 		int i, n;
+		String s;
 		Expression e;
+		Command c;
+		Module m;
+		ModulesFile mf;
+		boolean isLocal, isGlobal;
+		String var;
+		
+		c = getParent().getParent();
+		m = c.getParent();
+		mf = m.getParent();
 		
 		n = getNumElements();
 		for (i = 0; i < n; i++) {
-			e = getExpression(i);
+			// check that the update is allowed to modify this variable
+			var = getVar(i);
+			isLocal = m.isLocalVariable(var);
+			isGlobal = isLocal ? false : mf.isGlobalVariable(var);
+			if (!isLocal && !isGlobal) {
+				s = "Module " + m.getName() + " is not allowed to modify variable " + var;
+				s += " which belongs to another module";
+				throw new PrismException(s);
+			}
+			if (isGlobal && !c.getSynch().equals("")) {
+				s = "Synchronous command (" + c.getSynch() + ") in module " + m.getName();
+				s += " is not allowed to modify global variable " + var;
+				throw new PrismException(s);
+			}
 			// check expression
+			e = getExpression(i);
 			e.check();
 			// check evaluates to correct type
 			if (!Expression.canAssignTypes(getType(i), e.getType())) {
-				throw new PrismException("Type error in update \"(" + getVar(i) + "'=" + getExpression(i) + ")\"");
+				throw new PrismException("Type error in update \"(" + var + "'=" + getExpression(i) + ")\"");
 			}
 		}
 	}

prism/src/parser/Updates.java

@@ -48,6 +48,7 @@ public class Updates
 	{
 		probs.addElement(p);
 		updates.addElement(u);
+		u.setParent(this);
 	}
 
 	// set methods
@@ -55,6 +56,7 @@ public class Updates
 	public void setUpdate(int i, Update u)
 	{
 		updates.setElementAt(u, i);
+		u.setParent(this);
 	}
 	
 	public void setProbability(int i, Expression p)
@@ -132,7 +134,6 @@ public class Updates
 		for (i = 0; i < n; i++)  {
 			u.addUpdate(getProbability(i).rename(rm), getUpdate(i).rename(rm));
 		}
-		u.setParent(parent);
 		
 		return u;
 	}