diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 588a82d4..c5e28dc6 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -604,6 +604,9 @@ public class ProbModelChecker extends NonProbModelChecker protected StateValues checkProbPathFormulaAccumulationExpression(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { + if (!(model.getModelType() == ModelType.DTMC || model.getModelType() == ModelType.MDP)) { + throw new PrismException("Model checking of accumulation expressions formulas is not supported for "+model.getModelType().name()); + } // 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()); @@ -636,11 +639,7 @@ public class ProbModelChecker extends NonProbModelChecker if (useSimplePathAlgo) { return checkProbPathFormulaSimple(model, expr, minMax, statesOfInterest); } else if (Expression.containsAccumulationExpression(expr)) { - 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()); - } + return this.checkProbPathFormulaAccumulationExpression(model, expr, minMax, statesOfInterest); } else { return checkProbPathFormulaLTL(model, expr, false, minMax, statesOfInterest); }