From e02281dc8655b8d0470f1e64465054b9dc1401ce Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sat, 31 Jan 2015 10:45:46 +0000
Subject: [PATCH] Add Expression.isPathFormula(). [Joachim Klein]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9599 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/parser/ast/Expression.java | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index 15ae7ba0..e1a5e72a 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -122,6 +122,34 @@ public abstract class Expression extends ASTElement
 		return false;
 	}
 
+	/**
+	 * Returns {@code true} if this expression is a path formula.
+	 * If {@code allowNestedOperators==false} then we don't allow
+	 * nested P, R, ... operators.
+	 * @param allowNestedOperators allow nested P, R, ... operators?
+	 */
+	public boolean isPathFormula(boolean allowNestedOperators)
+	{
+		try {
+			if (getType() == null) {
+				this.typeCheck();
+			}
+			if (getType() == TypePathBool.getInstance() ||
+			    getType() == TypeBool.getInstance()) {
+				if (!allowNestedOperators) {
+					if (this.computeProbNesting() >= 1) {
+						return false;
+					}
+				}
+				return true;
+			}
+
+			return false;
+		} catch (PrismLangException e) {
+			return false;
+		}
+	}
+
 	/**
 	 * Convert a property expression (an LTL formula) into the classes used by
 	 * the jltl2ba (and jltl2dstar) libraries.