diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index 4f59bc7b..6c79c74b 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/prism/src/parser/ast/ASTElement.java @@ -328,6 +328,15 @@ public abstract class ASTElement return (ASTElement) accept(visitor); } + /** + * Find all references to properties (by name), replace the ExpressionLabels with ExpressionProps. + */ + public ASTElement findAllProps(ModulesFile mf, PropertiesFile pf) throws PrismLangException + { + FindAllProps visitor = new FindAllProps(mf, pf); + return (ASTElement) accept(visitor); + } + /** * Find all references to action labels, check they exist and, if required, * store their index locally (as defined by the containing ModuleFile). diff --git a/prism/src/parser/ast/ExpressionProp.java b/prism/src/parser/ast/ExpressionProp.java new file mode 100644 index 00000000..d8989264 --- /dev/null +++ b/prism/src/parser/ast/ExpressionProp.java @@ -0,0 +1,111 @@ +//============================================================================== +// +// 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.ast; + +import parser.*; +import parser.type.Type; +import parser.visitor.*; +import prism.PrismLangException; + +/** + * An expression "prop", representing a reference to another property. + */ +public class ExpressionProp extends Expression +{ + private String name; + + // Constructor + + public ExpressionProp(String s, Type t) + { + name = s; + setType(t); + } + + // Get Method + + public String getName() + { + return name; + } + + // Methods required for Expression: + + /** + * Is this expression constant? + */ + public boolean isConstant() + { + // Don't know - err on the side of caution + return false; + } + + /** + * Evaluate this expression, return result. + * Note: assumes that type checking has been done already. + */ + public Object evaluate(EvaluateContext ec) throws PrismLangException + { + throw new PrismLangException("Cannot evaluate property references", this); + } + + @Override + public boolean returnsSingleValue() + { + return false; + } + + // Methods required for ASTElement: + + /** + * Visitor method. + */ + public Object accept(ASTVisitor v) throws PrismLangException + { + return v.visit(this); + } + + /** + * Convert to string. + */ + public String toString() + { + return "\"" + name + "\""; + } + + /** + * Perform a deep copy. + */ + public Expression deepCopy() + { + ExpressionProp expr = new ExpressionProp(name, type); + expr.setPosition(this); + return expr; + } +} + +//------------------------------------------------------------------------------ diff --git a/prism/src/parser/ast/ModulesFile.java b/prism/src/parser/ast/ModulesFile.java index 64fbff26..842933cf 100644 --- a/prism/src/parser/ast/ModulesFile.java +++ b/prism/src/parser/ast/ModulesFile.java @@ -321,6 +321,16 @@ public class ModulesFile extends ASTElement return initStates; } + /** + * Look up a property by name. + * Returns null if not found. + * Currently only exists for forwards compatibility. + */ + public Property getPropertyByName(String name) + { + return null; + } + /** * Check if an identifier is used by this model * (as a formula, constant, or variable) @@ -475,6 +485,9 @@ public class ModulesFile extends ASTElement // Also check variables valid, store indices, etc. findAllVars(varNames, varTypes); + // Find all instances of property refs + findAllProps(this, null); + // Check reward structure names checkRewardStructNames(); diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 03fae5aa..713951e1 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/prism/src/parser/ast/PropertiesFile.java @@ -214,6 +214,9 @@ public class PropertiesFile extends ASTElement // Find all instances of variables (i.e. locate idents which are variables). findAllVars(modulesFile.getVarNames(), modulesFile.getVarTypes()); + // Find all instances of property refs + findAllProps(null, this); + // Various semantic checks semanticCheck(modulesFile, this); // Type checking diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index 08eba4a2..ea3e86c2 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/prism/src/parser/visitor/ASTTraverse.java @@ -532,6 +532,15 @@ public class ASTTraverse implements ASTVisitor } public void visitPost(ExpressionLabel e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- + public void visitPre(ExpressionProp e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(ExpressionProp e) throws PrismLangException + { + visitPre(e); + visitPost(e); + return null; + } + public void visitPost(ExpressionProp e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- public void visitPre(ExpressionFilter e) throws PrismLangException { defaultVisitPre(e); } public Object visit(ExpressionFilter e) throws PrismLangException { diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index 17b319cd..59826150 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/prism/src/parser/visitor/ASTTraverseModify.java @@ -541,6 +541,15 @@ public class ASTTraverseModify implements ASTVisitor } public void visitPost(ExpressionLabel e) throws PrismLangException { defaultVisitPost(e); } // ----------------------------------------------------------------------------------- + public void visitPre(ExpressionProp e) throws PrismLangException { defaultVisitPre(e); } + public Object visit(ExpressionProp e) throws PrismLangException + { + visitPre(e); + visitPost(e); + return e; + } + public void visitPost(ExpressionProp e) throws PrismLangException { defaultVisitPost(e); } + // ----------------------------------------------------------------------------------- public void visitPre(ExpressionFilter e) throws PrismLangException { defaultVisitPre(e); } public Object visit(ExpressionFilter e) throws PrismLangException { diff --git a/prism/src/parser/visitor/ASTVisitor.java b/prism/src/parser/visitor/ASTVisitor.java index c833454c..6e8b1620 100644 --- a/prism/src/parser/visitor/ASTVisitor.java +++ b/prism/src/parser/visitor/ASTVisitor.java @@ -75,6 +75,7 @@ public interface ASTVisitor public Object visit(ExpressionExists e) throws PrismLangException; public Object visit(ExpressionForAll e) throws PrismLangException; public Object visit(ExpressionLabel e) throws PrismLangException; + public Object visit(ExpressionProp e) throws PrismLangException; public Object visit(ExpressionFilter e) throws PrismLangException; // ASTElement classes (misc.) public Object visit(Filter e) throws PrismLangException; diff --git a/prism/src/parser/visitor/FindAllProps.java b/prism/src/parser/visitor/FindAllProps.java new file mode 100644 index 00000000..5a39bc73 --- /dev/null +++ b/prism/src/parser/visitor/FindAllProps.java @@ -0,0 +1,68 @@ +//============================================================================== +// +// 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 parser.ast.*; +import prism.PrismLangException; + +/** + * Find all references to properties (by name), replace the ExpressionLabels with ExpressionProps. + */ +public class FindAllProps extends ASTTraverseModify +{ + private ModulesFile mf; + private PropertiesFile pf; + + public FindAllProps(ModulesFile mf, PropertiesFile pf) + { + this.mf = mf; + this.pf = pf; + } + + public Object visit(ExpressionLabel e) throws PrismLangException + { + String name; + Property prop = null; + // See if identifier corresponds to a property + name = e.getName(); + if (mf != null) { + prop = mf.getPropertyByName(name); + } + if (prop == null && pf != null) { + prop = pf.getPropertyObjectByName(name); + } + if (prop != null) { + // If so, replace it with an ExpressionProp object + ExpressionProp expr = new ExpressionProp(e.getName(), prop.getType()); + expr.setPosition(e); + return expr; + } + // Otherwise, leave it unchanged + return e; + } +} + diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index accfb1c8..4f6f68e2 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -262,6 +262,10 @@ public class StateModelChecker implements ModelChecker else if (expr instanceof ExpressionLabel) { res = checkExpressionLabel((ExpressionLabel) expr); } + // Property refs + else if (expr instanceof ExpressionProp) { + res = checkExpressionProp((ExpressionProp) expr); + } // Filter else if (expr instanceof ExpressionFilter) { res = checkExpressionFilter((ExpressionFilter) expr); @@ -990,6 +994,20 @@ public class StateModelChecker implements ModelChecker } } + // Check property ref + + protected StateValues checkExpressionProp(ExpressionProp expr) throws PrismException + { + // Look up property and check recursively + Property prop = propertiesFile.lookUpPropertyObjectByName(expr.getName()); + if (prop != null) { + mainLog.println("\nModel checking : " + prop); + return checkExpression(prop.getExpression()); + } else { + throw new PrismException("Unknown property reference " + expr); + } + } + // Check filter protected StateValues checkExpressionFilter(ExpressionFilter expr) throws PrismException