From 2e6659a177ea8ec4f7d2de003a9f207d3d37603e Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:24:40 +0200
Subject: [PATCH] Expression.isCoSafeLTLSyntactic: properly handle nesting and
 operator bounds

For determining syntactic co-safety, we are not interested in
the complex state formulas (e.g., with P, R, E, A, ... operators),
so we iterate without recursing into nested operators.

Furthermore, we currently don't support temporal operator bounds
for co-safety LTL formulas; check for those as well.
---
 prism/src/parser/ast/Expression.java | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/prism/src/parser/ast/Expression.java b/prism/src/parser/ast/Expression.java
index 8fbe7e2d..a1775a03 100644
--- a/prism/src/parser/ast/Expression.java
+++ b/prism/src/parser/ast/Expression.java
@@ -978,6 +978,11 @@ public abstract class Expression extends ASTElement
 	/**
 	 * Test if an expression is a co-safe LTL formula, detected syntactically
 	 * (i.e. if it is in positive normal form and only uses X, F and U).
+	 * <br>
+	 * Treats nested non-Boolean state subformulas as opaque, i.e., considers
+	 * only the top-level LTL formula without recursing into operators such as P, R, etc.
+	 * <br>
+	 * Temporal operator bounds are considered to render the LTL formula unsafe.
 	 */
 	public static boolean isCoSafeLTLSyntactic(Expression expr)
 	{
@@ -990,6 +995,11 @@ public abstract class Expression extends ASTElement
 	 * If {@code convert} is true, the expression is first converted into positive normal form,
 	 * and then it is checked whether it only uses X, F and U.
 	 * For example, a => ! (G b) would return true if (and only if) {@code convert} was true.
+	 * <br>
+	 * Treats nested non-Boolean state subformulas as opaque, i.e., considers
+	 * only the top-level LTL formula without recursing into operators such as P, R, etc.
+	 * <br>
+	 * Temporal operator bounds are considered to render the LTL formula unsafe.
 	 */
 	public static boolean isCoSafeLTLSyntactic(Expression expr, boolean convert)
 	{
@@ -1000,12 +1010,17 @@ public abstract class Expression extends ASTElement
 			if (!isPositiveNormalFormLTL(expr))
 				return false;
 		}
-		// Check temporal operators
+
+		// Check temporal operators, don't recurse into nested operators
 		try {
-			ASTTraverse astt = new ASTTraverse()
+			ASTTraverse astt = new ExpressionTraverseNonNested()
 			{
 				public void visitPost(ExpressionTemporal e) throws PrismLangException
 				{
+					if (e.hasBounds()) {
+						throw new PrismLangException("Found temporal operator bound", e);
+					}
+
 					if (e.getOperator() == ExpressionTemporal.P_X)
 						return;
 					if (e.getOperator() == ExpressionTemporal.P_F)