Unbreak R[F] for DTMCs (symbolic) following changes to parser.

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

prism/src/prism/ProbModelChecker.java

@@ -52,6 +52,9 @@ import parser.ast.ExpressionTemporal;
 import parser.ast.ExpressionUnaryOp;
 import parser.ast.PropertiesFile;
 import parser.ast.RelOp;
+import parser.type.TypeBool;
+import parser.type.TypePathBool;
+import parser.type.TypePathDouble;
 import sparse.PrismSparse;
 import dv.DoubleVector;
 
@@ -221,7 +224,7 @@ public class ProbModelChecker extends NonProbModelChecker
 		// Compute rewards
 		StateValues rewards = null;
 		Expression expr2 = expr.getExpression();
-		if (expr2 instanceof ExpressionTemporal) {
+		if (expr2.getType() instanceof TypePathDouble) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr2;
 			switch (exprTemp.getOperator()) {
 			case ExpressionTemporal.R_C:
@@ -241,7 +244,10 @@ public class ProbModelChecker extends NonProbModelChecker
 				rewards = checkRewardSS(exprTemp, stateRewards, transRewards);
 				break;
 			}
+		} else if (expr2.getType() instanceof TypePathBool || expr2.getType() instanceof TypeBool) {
+			rewards = checkRewardPathFormula(expr2, stateRewards, transRewards);
 		}
+		
 		if (rewards == null)
 			throw new PrismException("Unrecognised operator in R operator");
 
@@ -849,6 +855,20 @@ public class ProbModelChecker extends NonProbModelChecker
 		return rewards;
 	}
 
+	/**
+	 * Compute rewards for a reachability reward operator.
+	 */
+	protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException
+	{
+		if (Expression.isReach(expr)) {
+			return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards);
+		}
+		else if (Expression.isCoSafeLTLSyntactic(expr)) {
+			throw new PrismNotSupportedException("Co-safe reward properties not yet supported for DTMCs in this engine");
+		}
+		throw new PrismException("Invalid contents for an R operator: " + expr);
+	}
+	
 	// reach reward
 
 	protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards) throws PrismException