add Expression.isReachWithStateFormula

isReach() is more restrictive, only allowing propositions as operand
of R=?[ F phi ], while we are also interested in the case where phi
as some complex state formula, potentially with nested operators, etc.

prism/src/parser/ast/Expression.java

@@ -806,7 +806,8 @@ public abstract class Expression extends ASTElement
 	}
 
 	/**
-	 * Test if an expression is a reachability path formula (F phi), possibly with a time bound.
+	 * Test if an expression is a reachability path formula (F phi), possibly with a time bound,
+	 * where phi is a proposition.
 	 */
 	public static boolean isReach(Expression expr)
 	{
@@ -818,6 +819,20 @@ public abstract class Expression extends ASTElement
 		return false;
 	}
 
+	/**
+	 * Test if an expression is a reachability path formula (F phi), possibly with a time bound,
+	 * where phi is an arbitrary state formula.
+	 */
+	public static boolean isReachWithStateFormula(Expression expr)
+	{
+		if (expr instanceof ExpressionTemporal) {
+			if (((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F) {
+				return ((ExpressionTemporal) expr).getOperand2().getType() == TypeBool.getInstance();
+			}
+		}
+		return false;
+	}
+
 	/**
 	 * Test if an expression contains time bounds on temporal operators 
 	 */