diff --git a/prism/src/parser/ast/ASTElement.java b/prism/src/parser/ast/ASTElement.java index ad89daaf..a00471b0 100644 --- a/prism/src/parser/ast/ASTElement.java +++ b/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); } diff --git a/prism/src/parser/ast/ExpressionFormula.java b/prism/src/parser/ast/ExpressionFormula.java index 1bfeb73e..c151cbc7 100644 --- a/prism/src/parser/ast/ExpressionFormula.java +++ b/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; } diff --git a/prism/src/parser/ast/PropertiesFile.java b/prism/src/parser/ast/PropertiesFile.java index 25bae2ac..78cef5a1 100644 --- a/prism/src/parser/ast/PropertiesFile.java +++ b/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(); diff --git a/prism/src/parser/visitor/ASTTraverse.java b/prism/src/parser/visitor/ASTTraverse.java index 2d9a74ac..e4845f2d 100644 --- a/prism/src/parser/visitor/ASTTraverse.java +++ b/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; } diff --git a/prism/src/parser/visitor/ASTTraverseModify.java b/prism/src/parser/visitor/ASTTraverseModify.java index b40d4679..ed940797 100644 --- a/prism/src/parser/visitor/ASTTraverseModify.java +++ b/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; } diff --git a/prism/src/parser/visitor/ExpandFormulas.java b/prism/src/parser/visitor/ExpandFormulas.java index d55aa0ab..3ecff782 100644 --- a/prism/src/parser/visitor/ExpandFormulas.java +++ b/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. diff --git a/prism/src/parser/visitor/SemanticCheck.java b/prism/src/parser/visitor/SemanticCheck.java index 95fe2427..96b97894 100644 --- a/prism/src/parser/visitor/SemanticCheck.java +++ b/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 diff --git a/prism/src/parser/visitor/TypeCheck.java b/prism/src/parser/visitor/TypeCheck.java index 04049d84..1fecc27b 100644 --- a/prism/src/parser/visitor/TypeCheck.java +++ b/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 diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index 47979eb2..3bc89472 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/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) {