Add property reference support to PTA ans approx model checking.

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

prism/CHANGELOG.txt

@@ -17,12 +17,12 @@ Changes:
 * GUI on Macs uses Cmd, not Ctrl
 * Added prominence given to log warning messages in command-line/GUI
 * Command-line scripts can signal termination via growlnotify/notify-send 
+* Properties can be named, by prefixing with "name":, and reference each other
 
 Ongoing changes:
 
 * Need to decide on switch options format for -exportresults
 * Handling of verbosity in log: PrismLog updated, not used yet
-* Properties can be named, by prefixing with "name":, and reference each other
 * CTL AG/EF
 
 -----------------------------------------------------------------------------

prism/src/parser/ast/ASTElement.java

@@ -379,6 +379,19 @@ public abstract class ASTElement
 		return v;
 	}
 
+	/**
+	 * Expand property references and labels, return result.
+	 * Property expansion is done recursively.
+	 * Special labels "deadlock", "init" and any not in label list are left.
+	 * @param propertiesFile The PropertiesFile for property lookup
+	 * @param labelList The LabelList for label definitions
+	 */
+	public ASTElement expandPropRefsAndLabels(PropertiesFile propertiesFile, LabelList labelList) throws PrismLangException
+	{
+		ExpandPropRefsAndLabels visitor = new ExpandPropRefsAndLabels(propertiesFile, labelList);
+		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/visitor/ExpandPropRefsAndLabels.java

@@ -0,0 +1,110 @@
+//==============================================================================
+//	
+//	Copyright (c) 2002-
+//	Authors:
+//	* Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford, formerly University of Birmingham)
+//	
+//------------------------------------------------------------------------------
+//	
+//	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 parser.type.*;
+import prism.PrismLangException;
+
+/**
+	 * Expand property references and labels, return result.
+	 * Property expansion is done recursively.
+	 * Special labels "deadlock", "init" and any not in label list are left.
+ */
+public class ExpandPropRefsAndLabels extends ASTTraverseModify
+{
+	// The PropertiesFile for property lookup
+	private PropertiesFile propertiesFile;
+	// The LabelList for label definitions
+	private LabelList labelList;
+	
+	public ExpandPropRefsAndLabels(PropertiesFile propertiesFile, LabelList labelList)
+	{
+		this.propertiesFile = propertiesFile;
+		this.labelList = labelList;
+	}
+	
+	public Object visit(ExpressionLabel e) throws PrismLangException
+	{
+		int i;
+		Type t;
+		Expression expr;
+		
+		// See if identifier corresponds to a label
+		i = labelList.getLabelIndex(e.getName());
+		if (i != -1) {
+			// If so, replace it with (a copy of) the corresponding expression
+			expr = labelList.getLabel(i).deepCopy();
+			// But also recursively expand that
+			// (nested labels not currently supported but may be one day)
+			// (don't clone it to avoid duplication of work)
+			expr = (Expression)expr.expandLabels(labelList);
+			// Put in brackets so precedence is preserved
+			// (for display purposes only; in case of re-parse)
+			// Also, preserve type (this is probably being done before
+			// type-checking so unnecessary, but do so just in case)
+			t = expr.getType();
+			expr = Expression.Parenth(expr);
+			expr.setType(t);
+			// Return replacement expression
+			return expr;
+		}
+		
+		// Couldn't find definition - leave unchanged.
+		return e;
+	}
+
+	public Object visit(ExpressionProp e) throws PrismLangException
+	{
+		Property prop;
+		Type t;
+		Expression expr;
+		
+		// See if name corresponds to a property
+		prop = propertiesFile.lookUpPropertyObjectByName(e.getName());
+		if (prop != null) {
+			// If so, replace it with (a copy of) the corresponding expression
+			expr = prop.getExpression().deepCopy();
+			// But also recursively expand that
+			// (don't clone it to avoid duplication of work)
+			expr = (Expression)expr.expandPropRefsAndLabels(propertiesFile, labelList);
+			// Put in brackets so precedence is preserved
+			// (for display purposes only; in case of re-parse)
+			// Also, preserve type (this is probably being done before
+			// type-checking so unnecessary, but do so just in case)
+			t = expr.getType();
+			expr = Expression.Parenth(expr);
+			expr.setType(t);
+			// Return replacement expression
+			return expr;
+		}
+		
+		// Couldn't find definition - leave unchanged.
+		return e;
+	}
+}
+

prism/src/pta/PTAModelChecker.java

@@ -133,8 +133,8 @@ public class PTAModelChecker
 		
 		// Take a copy of property, since will modify
 		expr = expr.deepCopy();
-		// Remove labels from property, using combined label list 
-		expr = (Expression) expr.expandLabels(labelList);
+		// Remove property refs ands labels from property 
+		expr = (Expression) expr.expandPropRefsAndLabels(propertiesFile, labelList);
 		// Evaluate constants in property (easier to do now)
 		expr = (Expression) expr.replaceConstants(constantValues);
 		// Also simplify expression to optimise model checking

prism/src/simulator/SimulatorEngine.java

@@ -530,9 +530,9 @@ public class SimulatorEngine
 	{
 		// Take a copy
 		Expression propNew = prop.deepCopy();
-		// Combine label lists from model/property file, then remove labels from property 
+		// Combine label lists from model/property file, then expand property refs/labels in property 
 		LabelList combinedLabelList = (pf == null) ? modulesFile.getLabelList() : pf.getCombinedLabelList();
-		propNew = (Expression) propNew.expandLabels(combinedLabelList);
+		propNew = (Expression) propNew.expandPropRefsAndLabels(pf, combinedLabelList);
 		// Then get rid of any constants and simplify
 		propNew = (Expression) propNew.replaceConstants(mfConstants);
 		if (pf != null) {