Formulas used in properties are left unexpanded for legibility.

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

prism/src/parser/ast/ASTElement.java

@@ -202,10 +202,23 @@ public abstract class ASTElement
 
 	/**
 	 * Expand all formulas, return result.
+	 * @param formulaList: The FormulaList for formula definitions
 	 */
 	public ASTElement expandFormulas(FormulaList formulaList) throws PrismLangException
 	{
-		ExpandFormulas visitor = new ExpandFormulas(formulaList);
+		return expandFormulas(formulaList, true);
+	}
+
+	/**
+	 * Expand all formulas, return result.
+	 * @param formulaList: The FormulaList for formula definitions
+	 * @param replace: Whether to replace formulas outright with their definition
+	 * (true for use in models since they may be subjected to renaming afterwards;
+	 * false for properties since it is cleaner just to have the name there when displayed)
+	 */
+	public ASTElement expandFormulas(FormulaList formulaList, boolean replace) throws PrismLangException
+	{
+		ExpandFormulas visitor = new ExpandFormulas(formulaList, replace);
 		return (ASTElement) accept(visitor);
 	}
 

prism/src/parser/ast/ExpressionFormula.java

@@ -33,6 +33,7 @@ import prism.PrismLangException;
 public class ExpressionFormula extends Expression
 {
 	String name;
+	Expression definition;
 	
 	// Constructors
 	
@@ -43,6 +44,7 @@ public class ExpressionFormula extends Expression
 	public ExpressionFormula(String n)
 	{
 		name = n;
+		definition = null;
 	}
 			
 	// Set method
@@ -52,6 +54,11 @@ public class ExpressionFormula extends Expression
 		name = n;
 	}
 	
+	public void setDefinition(Expression definition) 
+	{
+		this.definition = definition;
+	}
+	
 	// Get method
 	
 	public String getName()
@@ -59,6 +66,11 @@ public class ExpressionFormula extends Expression
 		return name;
 	}
 	
+	public Expression getDefinition()
+	{
+		return definition;
+	}
+	
 	// Methods required for Expression:
 	
 	/**
@@ -66,8 +78,8 @@ public class ExpressionFormula extends Expression
 	 */
 	public boolean isConstant()
 	{
-		// Don't know - err on the side of caution
-		return false;
+		// Unless defined, don't know so err on the side of caution
+		return definition == null ? false : definition.isConstant();
 	}
 
 	/**
@@ -76,8 +88,11 @@ public class ExpressionFormula extends Expression
 	 */
 	public Object evaluate(EvaluateContext ec) throws PrismLangException
 	{
-		// Should never be called
-		throw new PrismLangException("Could not evaluate formula", this);
+		// Should only be called (if at all) after definition has been set
+		if (definition == null)
+			throw new PrismLangException("Could not evaluate formula", this);
+		else
+			return definition.evaluate(ec);
 	}
 
 	// Methods required for ASTElement:
@@ -103,7 +118,8 @@ public class ExpressionFormula extends Expression
 	 */
 	public Expression deepCopy()
 	{
-		Expression ret = new ExpressionFormula(name);
+		ExpressionFormula ret = new ExpressionFormula(name);
+		ret.setDefinition(definition == null ? null : definition.deepCopy());
 		ret.setPosition(this);
 		return ret;
 	}

prism/src/parser/ast/PropertiesFile.java

@@ -118,11 +118,13 @@ public class PropertiesFile extends ASTElement
 		// Find all instances of formulas (i.e. locate idents which are formulas),
 		// check for any cyclic dependencies in the formula list and then expand all formulas.
 		// Note: We have to look for formulas defined both here and in the model.
+		// Note also that we opt not to do actual replacement of formulas in calls to exandFormulas
+		// (to improve legebility of properties)
 		findAllFormulas(modulesFile.getFormulaList());
 		findAllFormulas(formulaList);
 		formulaList.findCycles();
-		expandFormulas(modulesFile.getFormulaList());
-		expandFormulas(formulaList);
+		expandFormulas(modulesFile.getFormulaList(), false);
+		expandFormulas(formulaList, false);
 		
 		// Check label identifiers
 		checkLabelIdents();

prism/src/parser/visitor/ASTTraverse.java

@@ -437,6 +437,7 @@ public class ASTTraverse implements ASTVisitor
 	public Object visit(ExpressionFormula e) throws PrismLangException
 	{
 		visitPre(e);
+		if (e.getDefinition() != null) e.getDefinition().accept(this);
 		visitPost(e);
 		return null;
 	}

prism/src/parser/visitor/ASTTraverseModify.java

@@ -438,6 +438,7 @@ public class ASTTraverseModify implements ASTVisitor
 	public Object visit(ExpressionFormula e) throws PrismLangException
 	{
 		visitPre(e);
+		if (e.getDefinition() != null) e.setDefinition((Expression)(e.getDefinition().accept(this)));
 		visitPost(e);
 		return e;
 	}

prism/src/parser/visitor/ExpandFormulas.java

@@ -35,11 +35,17 @@ import prism.PrismLangException;
  */
 public class ExpandFormulas extends ASTTraverseModify
 {
+	// The FormulaList for formula definitions
 	private FormulaList formulaList;
+	 // Whether to replace formulas outright with their definition
+	 // (true for use in models since they may be subjected to renaming afterwards;
+	 // false for properties since it is cleaner just to have the name there when displayed)
+	private boolean replace;
 	
-	public ExpandFormulas(FormulaList formulaList)
+	public ExpandFormulas(FormulaList formulaList, boolean replace)
 	{
 		this.formulaList = formulaList;
+		this.replace = replace;
 	}
 	
 	public Object visit(ExpressionFormula e) throws PrismLangException
@@ -55,7 +61,7 @@ public class ExpandFormulas extends ASTTraverseModify
 			expr = formulaList.getFormula(i);
 			// But also recursively expand that
 			// (don't clone it to avoid duplication of work)
-			expr = (Expression)expr.expandFormulas(formulaList);
+			expr = (Expression)expr.expandFormulas(formulaList, replace);
 			// Put in brackets so precedence is preserved
 			// (for display purposes only; in case of re-parse)
 			expr = Expression.Parenth(expr);
@@ -65,7 +71,13 @@ public class ExpandFormulas extends ASTTraverseModify
 			expr = Expression.Parenth(expr);
 			expr.setType(t);
 			// Return replacement expression
-			return expr;
+			// (or just set definition and return)
+			if (replace) {
+				return expr;
+			} else {
+				e.setDefinition(expr);
+				return e;
+			}
 		}
 		
 		// Couldn't find definition - leave unchanged.

prism/src/parser/visitor/SemanticCheck.java

@@ -359,8 +359,9 @@ public class SemanticCheck extends ASTTraverse
 
 	public void visitPost(ExpressionFormula e) throws PrismLangException
 	{
-		// This should have been expanded by now
-		throw new PrismLangException("Unexpanded formula", e);
+		// 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

prism/src/parser/visitor/TypeCheck.java

@@ -234,6 +234,8 @@ public class TypeCheck extends ASTTraverse
 	public void visitPost(ExpressionBinaryOp e) throws PrismLangException
 	{
 		Type t1 = e.getOperand1().getType();
+		if (t1 == null)
+			e.getOperand1().getType();
 		Type t2 = e.getOperand2().getType();
 		boolean ok;
 
@@ -449,8 +451,12 @@ public class TypeCheck extends ASTTraverse
 
 	public void visitPost(ExpressionFormula e) throws PrismLangException
 	{
-		// Should never happpen
-		throw new PrismLangException("Cannot determine type of formulas", e);
+		// This should have been defined or expanded by now.
+		// If so, just set type to that of the definition; otherwise error
+		if (e.getDefinition() != null)
+			e.setType(e.getDefinition().getType());
+		else
+			throw new PrismLangException("Cannot determine type of formula", e);
 	}
 
 	public void visitPost(ExpressionVar e) throws PrismLangException

prism/src/prism/StateModelChecker.java

@@ -516,8 +516,11 @@ public class StateModelChecker implements ModelChecker
 		}
 		// Formulas
 		else if (expr instanceof ExpressionFormula) {
-			// Should never happen
-			throw new PrismException("Unexpanded formula \"" + ((ExpressionFormula) expr).getName() + "\"");
+			// This should have been defined or expanded by now.
+			if (((ExpressionFormula) expr).getDefinition() != null)
+				return checkExpression(((ExpressionFormula) expr).getDefinition());
+			else
+				throw new PrismException("Unexpanded formula \"" + ((ExpressionFormula) expr).getName() + "\"");
 		}
 		// Variables
 		else if (expr instanceof ExpressionVar) {