Finish refactoring from last commit (missed something in STPG model checker).

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

prism/src/explicit/ProbModelChecker.java

@@ -44,6 +44,7 @@ import explicit.rewards.ConstructRewards;
 import explicit.rewards.MCRewards;
 import explicit.rewards.MDPRewards;
 import explicit.rewards.Rewards;
+import explicit.rewards.STPGRewards;
 
 /**
  * Super class for explicit-state probabilistic model checkers.
@@ -808,6 +809,9 @@ public class ProbModelChecker extends NonProbModelChecker
 			res = ((MDPModelChecker) this).computeReachRewards((MDP) model, (MDPRewards) modelRewards, target, minMax.isMin());
 			result.setStrategy(res.strat);
 			break;
+		case STPG:
+			res = ((STPGModelChecker) this).computeReachRewards((STPG) model, (STPGRewards) modelRewards, target, minMax.isMin1(), minMax.isMin2());
+			break;
 		default:
 			throw new PrismException("Explicit engine does not yet handle the " + expr.getOperatorSymbol() + " reward operator for " + model.getModelType()
 					+ "s");

prism/src/explicit/STPGModelChecker.java

@@ -32,7 +32,6 @@ import java.util.List;
 import java.util.Map;
 
 import parser.ast.Expression;
-import parser.ast.ExpressionTemporal;
 import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismFileLog;
@@ -61,26 +60,6 @@ public class STPGModelChecker extends ProbModelChecker
 		throw new PrismException("LTL model checking not yet supported for stochastic games");
 	}
 	
-	/**
-	 * Compute rewards for the contents of an R operator.
-	 */
-	protected StateValues checkRewardFormula(Model model, STPGRewards rewards, ExpressionTemporal expr, boolean min1, boolean min2) throws PrismException
-	{
-		// Assume R [F ] for now...
-
-		BitSet target;
-		StateValues rews = null;
-		ModelCheckerResult res = null;
-
-		// model check operands first
-		target = checkExpression(model, expr.getOperand2()).getBitSet();
-
-		res = computeReachRewards((STPG) model, rewards, target, min1, min2);
-		rews = StateValues.createFromDoubleArray(res.soln, model);
-
-		return rews;
-	}
-
 	// Numerical computation functions
 
 	/**