From 17087eee26981e8e9f9af25f68b1befb32f66ee0 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 3 Dec 2015 02:41:43 +0000 Subject: [PATCH] Decompose semantics checks (into expressions, models, properties). This will facilitate later attempts to make model checking less tied to ModulesFile specifically, rather than other model sources. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10963 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/ASTElement.java | 36 +-- prism/src/parser/ast/ModulesFile.java | 27 ++- prism/src/parser/ast/PropertiesFile.java | 12 +- ...eck.java => ModulesFileSemanticCheck.java} | 183 +-------------- ...dulesFileSemanticCheckAfterConstants.java} | 29 +-- .../visitor/PropertiesSemanticCheck.java | 218 ++++++++++++++++++ 6 files changed, 276 insertions(+), 229 deletions(-) rename prism/src/parser/visitor/{SemanticCheck.java => ModulesFileSemanticCheck.java} (63%) rename prism/src/parser/visitor/{SemanticCheckAfterConstants.java => ModulesFileSemanticCheckAfterConstants.java} (70%) create mode 100644 prism/src/parser/visitor/PropertiesSemanticCheck.java diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index a35e3104..49f03601 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/prism/src/parser/ast/ASTElement.java @@ -435,40 +435,14 @@ public abstract class ASTElement } /** - * Perform any required semantic checks. - */ - public void semanticCheck() throws PrismLangException - { - semanticCheck(null, null); - } - - /** - * Perform any required semantic checks. - */ - public void semanticCheck(ModulesFile modulesFile) throws PrismLangException - { - semanticCheck(modulesFile, null); - } - - /** - * Perform any required semantic checks. Optionally pass in parent ModulesFile - * and PropertiesFile for some additional checks (or leave null); + * Perform any required semantic checks. These are just simple checks on expressions, mostly. + * For semantic checks on models and properties, specifically, see: + * {@link parser.visitor.ModulesFileSemanticCheck} and {@link parser.visitor.PropertiesSemanticCheck}. * These checks are done *before* any undefined constants have been defined. */ - public void semanticCheck(ModulesFile modulesFile, PropertiesFile propertiesFile) throws PrismLangException - { - SemanticCheck visitor = new SemanticCheck(modulesFile, propertiesFile); - 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 + public void semanticCheck() throws PrismLangException { - SemanticCheckAfterConstants visitor = new SemanticCheckAfterConstants(modulesFile, propertiesFile); + SemanticCheck visitor = new SemanticCheck(); accept(visitor); } diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 965389b2..a0613efb 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -624,7 +624,7 @@ public class ModulesFile extends ASTElement findAllActions(synchs); // Various semantic checks - semanticCheck(this); + doSemanticChecks(); // Type checking typeCheck(); @@ -921,6 +921,27 @@ public class ModulesFile extends ASTElement } } + /** + * Perform any required semantic checks. + * These checks are done *before* any undefined constants have been defined. + */ + private void doSemanticChecks() throws PrismLangException + { + ModulesFileSemanticCheck visitor = new ModulesFileSemanticCheck(this); + accept(visitor); + + } + + /** + * Perform further semantic checks that can only be done once values + * for any undefined constants have been defined. + */ + public void doSemanticChecksAfterConstants() throws PrismLangException + { + ModulesFileSemanticCheckAfterConstants visitor = new ModulesFileSemanticCheckAfterConstants(this); + accept(visitor); + } + /** * Get a list of constants in the model that are undefined * ("const int x;" rather than "const int x = 1;") @@ -942,7 +963,7 @@ public class ModulesFile extends ASTElement { undefinedConstantValues = someValues == null ? null : new Values(someValues); constantValues = constantList.evaluateConstants(someValues, null); - semanticCheckAfterConstants(this, null); + doSemanticChecksAfterConstants(); } /** @@ -955,7 +976,7 @@ public class ModulesFile extends ASTElement { undefinedConstantValues = someValues == null ? null : new Values(someValues); constantValues = constantList.evaluateSomeConstants(someValues, null); - semanticCheckAfterConstants(this, null); + doSemanticChecksAfterConstants(); } /** diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 6694c367..3fc8006a 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -285,7 +285,7 @@ public class PropertiesFile extends ASTElement findCyclesInPropertyReferences(); // Various semantic checks - semanticCheck(modulesFile, this); + doSemanticChecks(); // Type checking typeCheck(this); @@ -441,6 +441,16 @@ public class PropertiesFile extends ASTElement } } + /** + * Perform any required semantic checks. + * These checks are done *before* any undefined constants have been defined. + */ + private void doSemanticChecks() throws PrismLangException + { + PropertiesSemanticCheck visitor = new PropertiesSemanticCheck(this, modulesFile); + accept(visitor); + } + /** * Get a list of all undefined constants in the properties files * ("const int x;" rather than "const int x = 1;") diff --git a/prism/src/parser/visitor/SemanticCheck.java b/prism/src/parser/visitor/ModulesFileSemanticCheck.java similarity index 63% rename from prism/src/parser/visitor/SemanticCheck.java rename to prism/src/parser/visitor/ModulesFileSemanticCheck.java index 59e4320c..cb3d259d 100644 --- a/prism/src/parser/visitor/SemanticCheck.java +++ b/prism/src/parser/visitor/ModulesFileSemanticCheck.java @@ -34,62 +34,29 @@ import prism.ModelType; import prism.PrismLangException; /** - * Perform any required semantic checks. Optionally pass in parent ModulesFile - * and PropertiesFile for some additional checks (or leave null); + * Perform any required semantic checks on a ModulesFile (or parts of it). * These checks are done *before* any undefined constants have been defined. */ -public class SemanticCheck extends ASTTraverse +public class ModulesFileSemanticCheck extends SemanticCheck { private ModulesFile modulesFile; - private PropertiesFile propertiesFile; // Sometimes we need to keep track of parent (ancestor) objects - private ModulesFile inModulesFile = null; - private Module inModule = null; + //private Module inModule = null; private Expression inInvariant = null; private Expression inGuard = null; - private Update inUpdate = null; + //private Update inUpdate = null; - public SemanticCheck() - { - this(null, null); - } - - public SemanticCheck(ModulesFile modulesFile) - { - this(modulesFile, null); - } - - public SemanticCheck(ModulesFile modulesFile, PropertiesFile propertiesFile) - { - setModulesFile(modulesFile); - setPropertiesFile(propertiesFile); - } - - public void setModulesFile(ModulesFile modulesFile) + public ModulesFileSemanticCheck(ModulesFile modulesFile) { this.modulesFile = modulesFile; } - public void setPropertiesFile(PropertiesFile propertiesFile) - { - this.propertiesFile = propertiesFile; - } - - public void visitPre(ModulesFile e) throws PrismLangException - { - // Register the fact we are entering a model - inModulesFile = e; - } - public void visitPost(ModulesFile e) throws PrismLangException { int i, j, n, n2; Module m; Vector v; - // Register the fact we are leaving a model - inModulesFile = null; - // Check for use of init...endinit _and_ var initial values if (e.getInitialStates() != null) { n = e.getNumGlobals(); @@ -210,7 +177,7 @@ public class SemanticCheck extends ASTTraverse public void visitPre(Module e) throws PrismLangException { // Register the fact we are entering a module - inModule = e; + //inModule = e; } public Object visit(Module e) throws PrismLangException @@ -237,7 +204,7 @@ public class SemanticCheck extends ASTTraverse public void visitPost(Module e) throws PrismLangException { // Register the fact we are leaving a module - inModule = null; + //inModule = null; } public Object visit(Command e) throws PrismLangException @@ -255,7 +222,7 @@ public class SemanticCheck extends ASTTraverse public void visitPre(Update e) throws PrismLangException { // Register the fact we are entering an update - inUpdate = e; + //inUpdate = e; } public void visitPost(Update e) throws PrismLangException @@ -264,23 +231,21 @@ public class SemanticCheck extends ASTTraverse String s, var; Command c; Module m; - ModulesFile mf; boolean isLocal, isGlobal; // Register the fact we are leaving an update - inUpdate = null; + //inUpdate = null; // Determine containing command/module/model // (mf should coincide with the stored modulesFile) c = e.getParent().getParent(); m = c.getParent(); - mf = m.getParent(); n = e.getNumElements(); for (i = 0; i < n; i++) { // Check that the update is allowed to modify this variable var = e.getVar(i); isLocal = m.isLocalVariable(var); - isGlobal = isLocal ? false : mf.isGlobalVariable(var); + isGlobal = isLocal ? false : modulesFile.isGlobalVariable(var); if (!isLocal && !isGlobal) { s = "Module \"" + m.getName() + "\" is not allowed to modify variable \"" + var + "\""; throw new PrismLangException(s, e.getVarIdent(i)); @@ -360,64 +325,6 @@ public class SemanticCheck extends ASTTraverse } } - public void visitPost(ExpressionTemporal e) throws PrismLangException - { - int op = e.getOperator(); - Expression operand1 = e.getOperand1(); - Expression operand2 = e.getOperand2(); - Expression lBound = e.getLowerBound(); - Expression uBound = e.getUpperBound(); - if (lBound != null && !lBound.isConstant()) { - throw new PrismLangException("Lower bound in " + e.getOperatorSymbol() + " operator is not constant", lBound); - } - if (uBound != null && !uBound.isConstant()) { - throw new PrismLangException("Upper bound in " + e.getOperatorSymbol() + " operator is not constant", uBound); - } - // Other checks (which parser should never allow to occur anyway) - if (op == ExpressionTemporal.P_X && (operand1 != null || operand2 == null || lBound != null || uBound != null)) { - throw new PrismLangException("Cannot attach bounds to " + e.getOperatorSymbol() + " operator", e); - } - if (op == ExpressionTemporal.R_C && (operand1 != null || operand2 != null || lBound != null)) { - // NB: upper bound is optional (e.g. multi-objective allows R...[C] operator) - throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e); - } - if (op == ExpressionTemporal.R_I && (operand1 != null || operand2 != null || lBound != null || uBound == null)) { - throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e); - } - if (op == ExpressionTemporal.R_S && (operand1 != null || operand2 != null || lBound != null || uBound != null)) { - throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e); - } - } - - public void visitPost(ExpressionFunc e) throws PrismLangException - { - // Check function name is valid - if (e.getNameCode() == -1) { - throw new PrismLangException("Unknown function \"" + e.getName() + "\"", e); - } - // Check num arguments - if (e.getNumOperands() < e.getMinArity()) { - throw new PrismLangException("Not enough arguments to \"" + e.getName() + "\" function", e); - } - if (e.getMaxArity() != -1 && e.getNumOperands() > e.getMaxArity()) { - throw new PrismLangException("Too many arguments to \"" + e.getName() + "\" function", e); - } - } - - public void visitPost(ExpressionIdent e) throws PrismLangException - { - // By the time the expression is checked, this should - // have been converted to an ExpressionVar/ExpressionConstant/... - throw new PrismLangException("Undeclared identifier", e); - } - - public void visitPost(ExpressionFormula e) throws PrismLangException - { - // This should have been defined or expanded by now - if (e.getDefinition() == null) - throw new PrismLangException("Unexpanded formula", e); - } - public void visitPost(ExpressionVar e) throws PrismLangException { // For PTAs, references to variables in modules have to be local @@ -429,75 +336,17 @@ public class SemanticCheck extends ASTTraverse }*/ // Clock references, in models, can only appear in invariants and guards // (Note: type checking has not been done, but we know types for ExpressionVars) - if (e.getType() instanceof TypeClock && inModulesFile != null) { + if (e.getType() instanceof TypeClock) { if (inInvariant == null && inGuard == null) { throw new PrismLangException("Reference to a clock variable cannot appear here", e); } } } - public void visitPost(ExpressionProb e) throws PrismLangException - { - if (e.getModifier() != null) { - throw new PrismLangException("Modifier \"" + e.getModifier() + "\" not supported for P operator"); - } - if (e.getProb() != null && !e.getProb().isConstant()) { - throw new PrismLangException("P operator probability bound is not constant", e.getProb()); - } - } - - public void visitPost(ExpressionReward e) throws PrismLangException - { - if (e.getModifier() != null) { - throw new PrismLangException("Modifier \"" + e.getModifier() + "\" not supported for R operator"); - } - if (e.getRewardStructIndex() != null) { - if (e.getRewardStructIndex() instanceof Expression) { - Expression rsi = (Expression) e.getRewardStructIndex(); - if (!(rsi.isConstant())) { - throw new PrismLangException("R operator reward struct index is not constant", rsi); - } - } else if (e.getRewardStructIndex() instanceof String) { - String s = (String) e.getRewardStructIndex(); - if (modulesFile != null && modulesFile.getRewardStructIndex(s) == -1) { - throw new PrismLangException("R operator reward struct index \"" + s + "\" does not exist", e); - } - } - } - if (e.getRewardStructIndexDiv() != null) { - if (e.getRewardStructIndexDiv() instanceof Expression) { - Expression rsi = (Expression) e.getRewardStructIndexDiv(); - if (!(rsi.isConstant())) { - throw new PrismLangException("R operator reward struct index is not constant", rsi); - } - } else if (e.getRewardStructIndexDiv() instanceof String) { - String s = (String) e.getRewardStructIndexDiv(); - if (modulesFile != null && modulesFile.getRewardStructIndex(s) == -1) { - throw new PrismLangException("R operator reward struct index \"" + s + "\" does not exist", e); - } - } - } - if (e.getReward() != null && !e.getReward().isConstant()) { - throw new PrismLangException("R operator reward bound is not constant", e.getReward()); - } - } - - public void visitPost(ExpressionSS e) throws PrismLangException - { - if (e.getModifier() != null) { - throw new PrismLangException("Modifier \"" + e.getModifier() + "\" not supported for S operator"); - } - if (e.getProb() != null && !e.getProb().isConstant()) { - throw new PrismLangException("S operator probability bound is not constant", e.getProb()); - } - } - public void visitPost(ExpressionLabel e) throws PrismLangException { LabelList labelList; - if (propertiesFile != null) - labelList = propertiesFile.getCombinedLabelList(); - else if (modulesFile != null) + if (modulesFile != null) labelList = modulesFile.getLabelList(); else throw new PrismLangException("Undeclared label", e); @@ -510,12 +359,4 @@ public class SemanticCheck extends ASTTraverse throw new PrismLangException("Undeclared label", e); } } - - public void visitPost(ExpressionFilter e) throws PrismLangException - { - // Check filter type is valid - if (e.getOperatorType() == null) { - throw new PrismLangException("Unknown filter type \"" + e.getOperatorName() + "\"", e); - } - } } diff --git a/prism/src/parser/visitor/SemanticCheckAfterConstants.java b/prism/src/parser/visitor/ModulesFileSemanticCheckAfterConstants.java similarity index 70% rename from prism/src/parser/visitor/SemanticCheckAfterConstants.java rename to prism/src/parser/visitor/ModulesFileSemanticCheckAfterConstants.java index 0cb80957..f6494273 100644 --- a/prism/src/parser/visitor/SemanticCheckAfterConstants.java +++ b/prism/src/parser/visitor/ModulesFileSemanticCheckAfterConstants.java @@ -2,7 +2,7 @@ // // Copyright (c) 2002- // Authors: -// * Dave Parker (University of Oxford) +// * Dave Parker (University of Birmingham/Oxford) // //------------------------------------------------------------------------------ // @@ -32,29 +32,17 @@ import parser.ast.*; import prism.PrismLangException; /** - * Perform further semantic checks that can only be done once values - * for (at least some) undefined constants have been defined. Optionally pass in parent - * ModulesFile and PropertiesFile for some additional checks (or leave null); + * Perform further semantic checks on a ModulesFile (or parts of it) + * that can only be done once values for (at least some) undefined constants have been defined. */ -public class SemanticCheckAfterConstants extends ASTTraverse +public class ModulesFileSemanticCheckAfterConstants extends ASTTraverse { + @SuppressWarnings("unused") private ModulesFile modulesFile; - private PropertiesFile propertiesFile; - public SemanticCheckAfterConstants() - { - this(null, null); - } - - public SemanticCheckAfterConstants(ModulesFile modulesFile) - { - this(modulesFile, null); - } - - public SemanticCheckAfterConstants(ModulesFile modulesFile, PropertiesFile propertiesFile) + public ModulesFileSemanticCheckAfterConstants(ModulesFile modulesFile) { setModulesFile(modulesFile); - setPropertiesFile(propertiesFile); } public void setModulesFile(ModulesFile modulesFile) @@ -62,11 +50,6 @@ public class SemanticCheckAfterConstants extends ASTTraverse this.modulesFile = modulesFile; } - public void setPropertiesFile(PropertiesFile propertiesFile) - { - this.propertiesFile = propertiesFile; - } - public void visitPost(Update e) throws PrismLangException { int i, n; diff --git a/prism/src/parser/visitor/PropertiesSemanticCheck.java b/prism/src/parser/visitor/PropertiesSemanticCheck.java new file mode 100644 index 00000000..a3c38bf2 --- /dev/null +++ b/prism/src/parser/visitor/PropertiesSemanticCheck.java @@ -0,0 +1,218 @@ +//============================================================================== +// +// Copyright (c) 2002- +// Authors: +// * Dave Parker (University of Birmingham/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 parser.ast.ConstantList; +import parser.ast.Expression; +import parser.ast.ExpressionFilter; +import parser.ast.ExpressionLabel; +import parser.ast.ExpressionProb; +import parser.ast.ExpressionReward; +import parser.ast.ExpressionSS; +import parser.ast.ExpressionTemporal; +import parser.ast.FormulaList; +import parser.ast.LabelList; +import parser.ast.ModulesFile; +import parser.ast.PropertiesFile; +import prism.PrismLangException; + +/** + * Perform any required semantic checks on a PropertiesFile (or parts of it). + * These checks are done *before* any undefined constants have been defined. + * Optionally pass in parent ModulesFile (or leave null); + */ +public class PropertiesSemanticCheck extends SemanticCheck +{ + private PropertiesFile propertiesFile; + private ModulesFile modulesFile; + + public PropertiesSemanticCheck(PropertiesFile propertiesFile) + { + this(propertiesFile, null); + } + + public PropertiesSemanticCheck(PropertiesFile propertiesFile, ModulesFile modulesFile) + { + setPropertiesFile(propertiesFile); + setModulesFile(modulesFile); + } + + public void setPropertiesFile(PropertiesFile propertiesFile) + { + this.propertiesFile = propertiesFile; + } + + public void setModulesFile(ModulesFile modulesFile) + { + this.modulesFile = modulesFile; + } + + public Object visit(FormulaList e) throws PrismLangException + { + // Override - don't need to do any semantic checks on formulas + // (they will have been expanded in place, where needed) + // (and we shouldn't check them - e.g. clock vars appearing in errors would show as an error) + return null; + } + + public void visitPost(LabelList e) throws PrismLangException + { + int i, n; + String s; + n = e.size(); + for (i = 0; i < n; i++) { + s = e.getLabelName(i); + if ("deadlock".equals(s)) + throw new PrismLangException("Cannot define a label called \"deadlock\" - this is a built-in label", e.getLabel(i)); + if ("init".equals(s)) + throw new PrismLangException("Cannot define a label called \"init\" - this is a built-in label", e.getLabel(i)); + } + } + + public void visitPost(ConstantList e) throws PrismLangException + { + int i, n; + n = e.size(); + for (i = 0; i < n; i++) { + if (e.getConstant(i) != null && !e.getConstant(i).isConstant()) { + throw new PrismLangException("Definition of constant \"" + e.getConstantName(i) + "\" is not constant", e.getConstant(i)); + } + } + } + + public void visitPost(ExpressionTemporal e) throws PrismLangException + { + int op = e.getOperator(); + Expression operand1 = e.getOperand1(); + Expression operand2 = e.getOperand2(); + Expression lBound = e.getLowerBound(); + Expression uBound = e.getUpperBound(); + if (lBound != null && !lBound.isConstant()) { + throw new PrismLangException("Lower bound in " + e.getOperatorSymbol() + " operator is not constant", lBound); + } + if (uBound != null && !uBound.isConstant()) { + throw new PrismLangException("Upper bound in " + e.getOperatorSymbol() + " operator is not constant", uBound); + } + // Other checks (which parser should never allow to occur anyway) + if (op == ExpressionTemporal.P_X && (operand1 != null || operand2 == null || lBound != null || uBound != null)) { + throw new PrismLangException("Cannot attach bounds to " + e.getOperatorSymbol() + " operator", e); + } + if (op == ExpressionTemporal.R_C && (operand1 != null || operand2 != null || lBound != null)) { + // NB: upper bound is optional (e.g. multi-objective allows R...[C] operator) + throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e); + } + if (op == ExpressionTemporal.R_I && (operand1 != null || operand2 != null || lBound != null || uBound == null)) { + throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e); + } + if (op == ExpressionTemporal.R_S && (operand1 != null || operand2 != null || lBound != null || uBound != null)) { + throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e); + } + } + + public void visitPost(ExpressionProb e) throws PrismLangException + { + if (e.getModifier() != null) { + throw new PrismLangException("Modifier \"" + e.getModifier() + "\" not supported for P operator"); + } + if (e.getProb() != null && !e.getProb().isConstant()) { + throw new PrismLangException("P operator probability bound is not constant", e.getProb()); + } + } + + public void visitPost(ExpressionReward e) throws PrismLangException + { + if (e.getModifier() != null) { + throw new PrismLangException("Modifier \"" + e.getModifier() + "\" not supported for R operator"); + } + if (e.getRewardStructIndex() != null) { + if (e.getRewardStructIndex() instanceof Expression) { + Expression rsi = (Expression) e.getRewardStructIndex(); + if (!(rsi.isConstant())) { + throw new PrismLangException("R operator reward struct index is not constant", rsi); + } + } else if (e.getRewardStructIndex() instanceof String) { + String s = (String) e.getRewardStructIndex(); + if (modulesFile != null && modulesFile.getRewardStructIndex(s) == -1) { + throw new PrismLangException("R operator reward struct index \"" + s + "\" does not exist", e); + } + } + } + if (e.getRewardStructIndexDiv() != null) { + if (e.getRewardStructIndexDiv() instanceof Expression) { + Expression rsi = (Expression) e.getRewardStructIndexDiv(); + if (!(rsi.isConstant())) { + throw new PrismLangException("R operator reward struct index is not constant", rsi); + } + } else if (e.getRewardStructIndexDiv() instanceof String) { + String s = (String) e.getRewardStructIndexDiv(); + if (modulesFile != null && modulesFile.getRewardStructIndex(s) == -1) { + throw new PrismLangException("R operator reward struct index \"" + s + "\" does not exist", e); + } + } + } + if (e.getReward() != null && !e.getReward().isConstant()) { + throw new PrismLangException("R operator reward bound is not constant", e.getReward()); + } + } + + public void visitPost(ExpressionSS e) throws PrismLangException + { + if (e.getModifier() != null) { + throw new PrismLangException("Modifier \"" + e.getModifier() + "\" not supported for S operator"); + } + if (e.getProb() != null && !e.getProb().isConstant()) { + throw new PrismLangException("S operator probability bound is not constant", e.getProb()); + } + } + + public void visitPost(ExpressionLabel e) throws PrismLangException + { + LabelList labelList; + if (propertiesFile != null) + labelList = propertiesFile.getCombinedLabelList(); + else if (modulesFile != null) + labelList = modulesFile.getLabelList(); + else + throw new PrismLangException("Undeclared label", e); + String name = e.getName(); + // Allow special cases + if ("deadlock".equals(name) || "init".equals(name)) + return; + // Otherwise check list + if (labelList == null || labelList.getLabelIndex(name) == -1) { + throw new PrismLangException("Undeclared label", e); + } + } + + public void visitPost(ExpressionFilter e) throws PrismLangException + { + // Check filter type is valid + if (e.getOperatorType() == null) { + throw new PrismLangException("Unknown filter type \"" + e.getOperatorName() + "\"", e); + } + } +}