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

@@ -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)