accumulation: refactor ProbModelChecker methods

prism/src/explicit/DTMCModelChecker.java

@@ -80,19 +80,6 @@ public class DTMCModelChecker extends ProbModelChecker
 		super(parent);
 	}
 	
-	protected StateValues checkProbPathFormulaAccumulationExpression(Model model, Expression expr, BitSet statesOfInterest) throws PrismException
-	{
-		// Do a transformation and a projection
-		AccumulationTransformation<DTMCExplicit> accTrans = new AccumulationTransformation<DTMCExplicit>(this, (DTMCExplicit)model, expr, statesOfInterest);
-		StateValues transValues = this.checkProbPathFormula(accTrans.getTransformedModel(), accTrans.getTransformedExpression(), MinMax.blank(), accTrans.getTransformedStatesOfInterest());
-		//this.getLog().println("TransValues");
-		//transValues.print(this.getLog());
-		StateValues projectedValues = accTrans.projectToOriginalModel(transValues);
-		//this.getLog().println("ProjectedValues");
-		//projectedValues.print(this.getLog());
-		return projectedValues;
-	}
-	
 	// Model checking functions
 
 	@Override

prism/src/explicit/MDPModelChecker.java

@@ -90,15 +90,6 @@ public class MDPModelChecker extends ProbModelChecker
 	
 	// Model checking functions
 	
-	protected StateValues checkProbPathFormulaAccumulationExpression(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
-	{
-		// Do a transformation and a projection
-		AccumulationTransformation<MDPExplicit> accTrans = new AccumulationTransformation<MDPExplicit>(this, (MDPExplicit)model, expr, statesOfInterest);
-		StateValues transValues = this.checkProbPathFormula(accTrans.getTransformedModel(), accTrans.getTransformedExpression(), minMax, accTrans.getTransformedStatesOfInterest());
-		StateValues projectedValues = accTrans.projectToOriginalModel(transValues);
-		return projectedValues;
-	}
-	
 	@Override
 	protected StateValues checkProbPathFormulaSimple(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
 	{

prism/src/explicit/ProbModelChecker.java

@@ -602,6 +602,19 @@ public class ProbModelChecker extends NonProbModelChecker
 		}
 	}
 
+	protected StateValues checkProbPathFormulaAccumulationExpression(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
+	{
+		// Do a transformation and a projection
+		AccumulationTransformation<?> accTrans = new AccumulationTransformation<ModelExplicit>(this, (ModelExplicit)model, expr, statesOfInterest);
+		StateValues transValues = this.checkProbPathFormula(accTrans.getTransformedModel(), accTrans.getTransformedExpression(), minMax, accTrans.getTransformedStatesOfInterest());
+		//this.getLog().println("TransValues");
+		//transValues.print(this.getLog());
+		StateValues projectedValues = accTrans.projectToOriginalModel(transValues);
+		//this.getLog().println("ProjectedValues");
+		//projectedValues.print(this.getLog());
+		return projectedValues;
+	}
+	
 	/**
 	 * Compute probabilities for the contents of a P operator.
 	 * @param statesOfInterest the states of interest, see checkExpression()
@@ -623,10 +636,8 @@ public class ProbModelChecker extends NonProbModelChecker
 		if (useSimplePathAlgo) {
 			return checkProbPathFormulaSimple(model, expr, minMax, statesOfInterest);
 		} else if (Expression.containsAccumulationExpression(expr)) {
-			if (model.getModelType() == ModelType.DTMC) {
-				return ((DTMCModelChecker)this).checkProbPathFormulaAccumulationExpression(model, expr, statesOfInterest);
-			} else if (model.getModelType() == ModelType.MDP) {
-				return ((MDPModelChecker)this).checkProbPathFormulaAccumulationExpression(model, expr, minMax, statesOfInterest);
+			if (model.getModelType() == ModelType.DTMC || model.getModelType() == ModelType.MDP) {
+				return this.checkProbPathFormulaAccumulationExpression(model, expr, minMax, statesOfInterest);
 			} else {
 				throw new PrismException("Model checking of accumulation expressions formulas is not supported for "+model.getModelType().name());
 			}