Browse Source

accumulation: small refactor

accumulation
Sascha Wunderlich 7 years ago
parent
commit
230df7bd64
  1. 9
      prism/src/explicit/ProbModelChecker.java

9
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<ModelExplicit>(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);
}

Loading…
Cancel
Save