From 07baeb554eac0ee2040fe50592c3ebb1636f0c81 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 27 Mar 2006 10:37:29 +0000 Subject: [PATCH] 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 | 16 ++++++++++++ prism/src/parser/Module.java | 28 ++++++++++++++++++++ prism/src/parser/ModulesFile.java | 19 +++++++++++--- prism/src/parser/Update.java | 43 +++++++++++++++++++++++++++++-- prism/src/parser/Updates.java | 3 ++- 5 files changed, 103 insertions(+), 6 deletions(-) diff --git a/prism/src/parser/Command.java b/prism/src/parser/Command.java index 4ba96fe2..a5b350d5 100644 --- a/prism/src/parser/Command.java +++ b/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 @@ -66,6 +72,11 @@ public class Command updates = u; u.setParent(this); } + + public void setParent(Module m) + { + parent = m; + } // get methods @@ -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 diff --git a/prism/src/parser/Module.java b/prism/src/parser/Module.java index 12e605a3..870c7162 100644 --- a/prism/src/parser/Module.java +++ b/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; @@ -101,6 +118,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) diff --git a/prism/src/parser/ModulesFile.java b/prism/src/parser/ModulesFile.java index 09e35eaa..ba01f316 100644 --- a/prism/src/parser/ModulesFile.java +++ b/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); } } diff --git a/prism/src/parser/Update.java b/prism/src/parser/Update.java index 4643784a..6b06fc9a 100644 --- a/prism/src/parser/Update.java +++ b/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) + ")\""); } } } diff --git a/prism/src/parser/Updates.java b/prism/src/parser/Updates.java index cb47bc92..01e135af 100644 --- a/prism/src/parser/Updates.java +++ b/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; }