From 26541255319a7466bde477988f9b138fd004eec7 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 7 Jul 2011 22:09:39 +0000 Subject: [PATCH] * Check added to catch if the same variable is set twice in the same update * New class of semantic checks created that are only done after constant definitions git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3231 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/ASTElement.java | 17 +++- prism/src/parser/ast/ModulesFile.java | 1 + prism/src/parser/ast/PropertiesFile.java | 1 + prism/src/parser/visitor/SemanticCheck.java | 1 + .../visitor/SemanticCheckAfterConstants.java | 89 +++++++++++++++++++ 5 files changed, 106 insertions(+), 3 deletions(-) create mode 100644 prism/src/parser/visitor/SemanticCheckAfterConstants.java diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index 6c79c74b..c0d5beb6 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/prism/src/parser/ast/ASTElement.java @@ -373,9 +373,9 @@ public abstract class ASTElement } /** - * Perform any required semantic checks. Optionally pass in parent - * ModulesFile and PropertiesFile for some additional checks (or leave - * null); + * Perform any required semantic checks. Optionally pass in parent ModulesFile + * and PropertiesFile for some additional checks (or leave null); + * These checks are done *before* any undefined constants have been defined. */ public void semanticCheck(ModulesFile modulesFile, PropertiesFile propertiesFile) throws PrismLangException { @@ -383,6 +383,17 @@ public abstract class ASTElement accept(visitor); } + /** + * Perform further semantic checks that can only be done once values + * for any undefined constants have been defined. Optionally pass in parent + * ModulesFile and PropertiesFile for some additional checks (or leave null); + */ + public void semanticCheckAfterConstants(ModulesFile modulesFile, PropertiesFile propertiesFile) throws PrismLangException + { + SemanticCheckAfterConstants visitor = new SemanticCheckAfterConstants(modulesFile, propertiesFile); + accept(visitor); + } + /** * Evaluate partially: replace some constants and variables with actual values. */ diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index be1083a4..2a680f2c 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -763,6 +763,7 @@ public class ModulesFile extends ASTElement public void setUndefinedConstants(Values someValues) throws PrismLangException { constantValues = constantList.evaluateConstants(someValues, null); + semanticCheckAfterConstants(this, null); } /** diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 44c4a7fc..68b5167d 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -371,6 +371,7 @@ public class PropertiesFile extends ASTElement { // might need values for ModulesFile constants too constantValues = constantList.evaluateConstants(someValues, modulesFile.getConstantValues()); + semanticCheckAfterConstants(modulesFile, this); } /** diff --git a/prism/src/parser/visitor/SemanticCheck.java b/prism/src/parser/visitor/SemanticCheck.java index b0431e3b..35aa868e 100644 --- a/prism/src/parser/visitor/SemanticCheck.java +++ b/prism/src/parser/visitor/SemanticCheck.java @@ -36,6 +36,7 @@ import prism.PrismLangException; /** * Perform any required semantic checks. Optionally pass in parent ModulesFile * and PropertiesFile for some additional checks (or leave null); + * These checks are done *before* any undefined constants have been defined. */ public class SemanticCheck extends ASTTraverse { diff --git a/prism/src/parser/visitor/SemanticCheckAfterConstants.java b/prism/src/parser/visitor/SemanticCheckAfterConstants.java new file mode 100644 index 00000000..6a95d1b0 --- /dev/null +++ b/prism/src/parser/visitor/SemanticCheckAfterConstants.java @@ -0,0 +1,89 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Oxford) +// +//------------------------------------------------------------------------------ +// +// This file is part of PRISM. +// +// PRISM is free software; you can redistribute it and/or modify +// it under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// PRISM is distributed in the hope that it will be useful, +// but WITHOUT ANY WARRANTY; without even the implied warranty of +// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +// GNU General Public License for more details. +// +// You should have received a copy of the GNU General Public License +// along with PRISM; if not, write to the Free Software Foundation, +// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +// +//============================================================================== + +package parser.visitor; + +import java.util.Vector; + +import parser.ast.*; +import prism.PrismLangException; + +/** + * Perform further semantic checks that can only be done once values + * for any undefined constants have been defined. Optionally pass in parent + * ModulesFile and PropertiesFile for some additional checks (or leave null); + */ +public class SemanticCheckAfterConstants extends ASTTraverse +{ + private ModulesFile modulesFile; + private PropertiesFile propertiesFile; + + public SemanticCheckAfterConstants() + { + this(null, null); + } + + public SemanticCheckAfterConstants(ModulesFile modulesFile) + { + this(modulesFile, null); + } + + public SemanticCheckAfterConstants(ModulesFile modulesFile, PropertiesFile propertiesFile) + { + setModulesFile(modulesFile); + setPropertiesFile(propertiesFile); + } + + public void setModulesFile(ModulesFile modulesFile) + { + this.modulesFile = modulesFile; + } + + public void setPropertiesFile(PropertiesFile propertiesFile) + { + this.propertiesFile = propertiesFile; + } + + public void visitPost(Update e) throws PrismLangException + { + int i, n; + String var; + Vector varsUsed = new Vector(); + + // Check that no variables are set twice in the same update + // Currently, could do this *before* constants are defined, + // but one day we might need to worry about e.g. array indices... + n = e.getNumElements(); + for (i = 0; i < n; i++) { + var = e.getVar(i); + if (varsUsed.contains(var)) { + throw new PrismLangException("Variable \"" + var + "\" is set twice in the same update", e.getVarIdent(i)); + } + varsUsed.add(var); + } + varsUsed.clear(); + } +}