From f4dab093cb776e0ec72825c6c90fe18e319ae525 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 a1775a03..c0ecb67e 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -820,7 +820,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) { @@ -832,6 +833,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 */