From 409ab5d1996d88a6791989f745310749712ef7ff Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:24:56 +0200 Subject: [PATCH] add Expression.isReachWithStateFormula isReach() is more restrictive, only allowing propositions as operand of R=?[ F phi ], while we are also interested in the case where phi as some complex state formula, potentially with nested operators, etc. --- prism/src/parser/ast/Expression.java | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index 50c58717..f000926a 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -806,7 +806,8 @@ public abstract class Expression extends ASTElement } /** - * Test if an expression is a reachability path formula (F phi), possibly with a time bound. + * Test if an expression is a reachability path formula (F phi), possibly with a time bound, + * where phi is a proposition. */ public static boolean isReach(Expression expr) { @@ -818,6 +819,20 @@ public abstract class Expression extends ASTElement return false; } + /** + * Test if an expression is a reachability path formula (F phi), possibly with a time bound, + * where phi is an arbitrary state formula. + */ + public static boolean isReachWithStateFormula(Expression expr) + { + if (expr instanceof ExpressionTemporal) { + if (((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F) { + return ((ExpressionTemporal) expr).getOperand2().getType() == TypeBool.getInstance(); + } + } + return false; + } + /** * Test if an expression contains time bounds on temporal operators */