Property references can appear in properties (still a few TODOs though).

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

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).

prism/src/parser/ast/ExpressionProp.java

@@ -0,0 +1,111 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (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;
+	}
+}
+
+//------------------------------------------------------------------------------

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();
 

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

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
 	{

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
 	{

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;

prism/src/parser/visitor/FindAllProps.java

@@ -0,0 +1,68 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (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;
+	}
+}
+

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