From 3208eadeb4da79210465498eddd747c4e806a573 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:25:49 +0200
Subject: [PATCH] imported patch
 rewardcounter-expression.getTemporalOperator.patch

---
 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 c2fafa2f..440c8c6f 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -1165,6 +1165,34 @@ public abstract class Expression extends ASTElement
 			throw new PrismException("Cannot convert jltl2ba formula " + ltl);
 		}
 	}
+
+	/**
+	 * Return the temporal operator for a simple path formula, i.e.,
+	 * ignoring parentheses and negation.
+	 */
+	public static ExpressionTemporal getTemporalOperatorForSimplePathFormula(Expression expr) throws PrismLangException {
+		// Negation/parentheses
+		while (expr instanceof ExpressionUnaryOp) {
+			ExpressionUnaryOp exprUnary = (ExpressionUnaryOp) expr;
+			// Parentheses
+			if (exprUnary.getOperator() == ExpressionUnaryOp.PARENTH) {
+				expr = exprUnary.getOperand();
+			}
+			// Negation
+			else if (exprUnary.getOperator() == ExpressionUnaryOp.NOT) {
+				expr = exprUnary.getOperand();
+			} else {
+				throw new PrismLangException("Expression is not a simple path formula: Unexpected unary operator "+exprUnary.getOperatorSymbol());
+			}
+		}
+
+		// Temporal operator
+		if (expr instanceof ExpressionTemporal) {
+			return (ExpressionTemporal)expr;
+		} else {
+			throw new PrismLangException("Expression is not a simple path formula: Unsupported expression "+expr.toString());
+		}
+	}
 }
 
 //------------------------------------------------------------------------------