Remove (most) usage of R_F in temporal operators.

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

prism/src/explicit/ProbModelChecker.java

@@ -890,9 +890,6 @@ public class ProbModelChecker extends NonProbModelChecker
 		if (expr.getType() instanceof TypePathDouble) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			switch (exprTemp.getOperator()) {
-			case ExpressionTemporal.R_F:
-				rewards = checkRewardReach(model, modelRewards, exprTemp, minMax, statesOfInterest);
-				break;
 			case ExpressionTemporal.R_I:
 				rewards = checkRewardInstantaneous(model, modelRewards, exprTemp, minMax);
 				break;

prism/src/param/ParamModelChecker.java

@@ -1007,7 +1007,7 @@ final public class ParamModelChecker extends PrismComponent
 		if (expr instanceof ExpressionTemporal) {
 			ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
 			switch (exprTemp.getOperator()) {
-			case ExpressionTemporal.R_F:
+			case ExpressionTemporal.P_F:
 				rewards = checkRewardReach(model, rew, exprTemp, min, needStates);
 				break;
 			case ExpressionTemporal.R_S:

prism/src/parser/visitor/SemanticCheck.java

@@ -384,9 +384,6 @@ public class SemanticCheck extends ASTTraverse
 		if (op == ExpressionTemporal.R_I && (operand1 != null || operand2 != null || lBound != null || uBound == null)) {
 			throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e);
 		}
-		if (op == ExpressionTemporal.R_F && (operand1 != null || operand2 == null || lBound != null || uBound != null)) {
-			throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e);
-		}
 		if (op == ExpressionTemporal.R_S && (operand1 != null || operand2 != null || lBound != null || uBound != null)) {
 			throw new PrismLangException("Badly formed " + e.getOperatorSymbol() + " operator", e);
 		}

prism/src/parser/visitor/TypeCheck.java

@@ -193,14 +193,6 @@ public class TypeCheck extends ASTTraverse
 			}
 			e.setType(TypePathBool.getInstance());
 			break;
-		case ExpressionTemporal.R_F:
-			if (e.getOperand2() != null) {
-				type = e.getOperand2().getType();
-				if (!(type instanceof TypeBool) && !(type instanceof TypePathBool))
-					throw new PrismLangException("Type error: Argument of " + e.getOperatorSymbol() + " operator is not Boolean", e.getOperand2());
-			}
-			e.setType(TypePathDouble.getInstance());
-			break;
 		case ExpressionTemporal.R_C:
 		case ExpressionTemporal.R_I:
 		case ExpressionTemporal.R_S:

prism/src/prism/NondetModelChecker.java

@@ -249,9 +249,6 @@ public class NondetModelChecker extends NonProbModelChecker
 			case ExpressionTemporal.R_I:
 				rewards = checkRewardInst(exprTemp, stateRewards, transRewards, minMax.isMin());
 				break;
-			case ExpressionTemporal.R_F:
-				rewards = checkRewardReach(exprTemp, stateRewards, transRewards, minMax.isMin());
-				break;
 			}
 		} else if (expr2.getType() instanceof TypePathBool || expr2.getType() instanceof TypeBool) {
 			rewards = checkRewardPathFormula(expr2, stateRewards, transRewards, minMax.isMin());

prism/src/prism/ProbModelChecker.java

@@ -237,9 +237,6 @@ public class ProbModelChecker extends NonProbModelChecker
 			case ExpressionTemporal.R_I:
 				rewards = checkRewardInst(exprTemp, stateRewards, transRewards);
 				break;
-			case ExpressionTemporal.R_F:
-				rewards = checkRewardReach(exprTemp, stateRewards, transRewards);
-				break;
 			case ExpressionTemporal.R_S:
 				rewards = checkRewardSS(exprTemp, stateRewards, transRewards);
 				break;

prism/src/simulator/sampler/Sampler.java

@@ -253,7 +253,7 @@ public abstract class Sampler
 				// Discrete-time instantaneous reward
 				return new SamplerRewardInstDisc(exprTemp, rsi);
 			}
-		case ExpressionTemporal.R_F:
+		case ExpressionTemporal.P_F:
 			// reachability reward
 			return new SamplerRewardReach(exprTemp, rsi);
 		}

prism/src/simulator/sampler/SamplerRewardReach.java

@@ -49,7 +49,7 @@ public class SamplerRewardReach extends SamplerDouble
 		
 		// Make sure expression is of the correct type
 		// Then extract other required info
-		if (expr.getOperator() != ExpressionTemporal.R_F)
+		if (expr.getOperator() != ExpressionTemporal.P_F)
 			throw new PrismException("Error creating Sampler");
 		target = expr.getOperand2();
 		this.rewardStructIndex = rewardStructIndex;