diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index d5ea11a5..56f47377 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -79,19 +79,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 accTrans = new AccumulationTransformation(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 diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index cd7b4dde..bc5b103e 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -89,15 +89,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 accTrans = new AccumulationTransformation(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 diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 0874a24d..588a82d4 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/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(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()); }