From ea537cc895635973ed90c68a09082974a3d2a33f Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 10 Dec 2015 15:53:17 +0000 Subject: [PATCH] Expression.containsTemporalTimeBounds(): do not recurse into P/R/SS subformulas Expressions such as P=?[ X F P>0[F<=4 s=7] ] were problematic before, as the LTL check for time bounds would recurse into the P-subformula and complain without need. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11036 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/ast/Expression.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java index ffaa345b..146e37b5 100644 --- a/prism/src/parser/ast/Expression.java +++ b/prism/src/parser/ast/Expression.java @@ -731,7 +731,8 @@ public abstract class Expression extends ASTElement public static boolean containsTemporalTimeBounds(Expression expr) { try { - expr.accept(new ASTTraverse() + // check for time bounds, don't recurse into P/R/SS subformulas + expr.accept(new ExpressionTraverseNonNested() { public void visitPre(ExpressionTemporal e) throws PrismLangException {