From 1801fcba702791a2d0f4654bd1ac2327f1b9bc72 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 13 Oct 2017 15:37:35 +0200 Subject: [PATCH] (exact / parametric) ParamModelChecker: fix missing support for formula references in properties E.g., 'formula foo = (state = 1)' in model file, use in property 'P=?[ F foo ]'. Analogous to how it's done in explicit / symbolic StateModelCheckers. --- prism/src/param/ParamModelChecker.java | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/prism/src/param/ParamModelChecker.java b/prism/src/param/ParamModelChecker.java index a7f03dab..d3e88a0e 100644 --- a/prism/src/param/ParamModelChecker.java +++ b/prism/src/param/ParamModelChecker.java @@ -68,6 +68,7 @@ import parser.ast.ExpressionExists; import parser.ast.ExpressionFilter; import parser.ast.ExpressionFilter.FilterOperator; import parser.ast.ExpressionForAll; +import parser.ast.ExpressionFormula; import parser.ast.ExpressionFunc; import parser.ast.ExpressionLabel; import parser.ast.ExpressionLiteral; @@ -372,6 +373,12 @@ final public class ParamModelChecker extends PrismComponent res = checkExpressionBinaryOp(model, (ExpressionBinaryOp) expr, needStates); } else if (expr instanceof ExpressionLabel) { res = checkExpressionLabel(model, (ExpressionLabel) expr, needStates); + } else if (expr instanceof ExpressionFormula) { + // This should have been defined or expanded by now. + if (((ExpressionFormula) expr).getDefinition() != null) + res = checkExpression(model, ((ExpressionFormula) expr).getDefinition(), needStates); + else + throw new PrismException("Unexpanded formula \"" + ((ExpressionFormula) expr).getName() + "\""); } else if (expr instanceof ExpressionProp) { res = checkExpressionProp(model, (ExpressionProp) expr, needStates); } else if (expr instanceof ExpressionFilter) {