Browse Source

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
master
Joachim Klein 10 years ago
parent
commit
ea537cc895
  1. 3
      prism/src/parser/ast/Expression.java

3
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
{

Loading…
Cancel
Save