Bug fix: better detection of R[F] when seeing if it is cosafe.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10338 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/ProbModelChecker.java

@@ -1054,7 +1054,7 @@ public class ProbModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkRewardPathFormula(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{
-		if (expr instanceof ExpressionTemporal && ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F){
+		if (Expression.isReach(expr)) {
 			return checkRewardReach(model, modelRewards, (ExpressionTemporal) expr, minMax, statesOfInterest);
 		}
 		else if (Expression.isCoSafeLTLSyntactic(expr)) {

prism/src/parser/ast/Expression.java

@@ -702,6 +702,19 @@ public abstract class Expression extends ASTElement
 		return false;
 	}
 
+	/**
+	 * Test if an expression is a reachability path formula (F phi) 
+	 */
+	public static boolean isReach(Expression expr)
+	{
+		if (expr instanceof ExpressionTemporal) {
+			if (((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F) {
+				return ((ExpressionTemporal) expr).getOperand2().isProposition();
+			}
+		}
+		return false;
+	}
+
 	/**
 	 * Test if an expression contains time bounds on temporal operators 
 	 */

prism/src/prism/NondetModelChecker.java

@@ -1186,7 +1186,7 @@ public class NondetModelChecker extends NonProbModelChecker
 	 */
 	protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
 	{
-		if (expr instanceof ExpressionTemporal && ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F){
+		if (Expression.isReach(expr)) {
 			return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, min);
 		}
 		else if (Expression.isCoSafeLTLSyntactic(expr)) {