From 230df7bd649b21c7fd3c71d254265eeb942c3746 Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Fri, 18 Jan 2019 11:07:37 +0100 Subject: [PATCH] accumulation: small refactor --- prism/src/explicit/ProbModelChecker.java | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) 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); }