From 150fcd39a33f9c5cf02511702b46a4acc152679f Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:25:55 +0200 Subject: [PATCH] imported patch rewardcounter-MDPModelChecker.simple-path-formulas-with-bounds.patch --- prism/src/explicit/MDPModelChecker.java | 42 +++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 53bf0d55..0297804b 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -41,6 +41,8 @@ import parser.VarList; import parser.ast.Declaration; import parser.ast.DeclarationIntUnbounded; import parser.ast.Expression; +import parser.ast.ExpressionTemporal; +import parser.ast.TemporalOperatorBound; import prism.OptionsIntervalIteration; import prism.Prism; import prism.PrismComponent; @@ -85,6 +87,46 @@ public class MDPModelChecker extends ProbModelChecker // Model checking functions + @Override + protected StateValues checkProbPathFormulaSimple(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException + { + // In continuous time case, defer to the standard handling without special treatments for rewards + if (model.getModelType().continuousTime()) { + return super.checkProbPathFormulaSimple(model, expr, minMax, statesOfInterest); + } + + expr = Expression.convertSimplePathFormulaToCanonicalForm(expr); + ExpressionTemporal exprTemp = Expression.getTemporalOperatorForSimplePathFormula(expr); + + if (exprTemp.getBounds().hasRewardBounds() || + exprTemp.getBounds().countTimeBoundsDiscrete() > 1) { + // We have reward bounds or multiple time / step bounds + // transform model and expression and recurse + + List boundsToReplace = exprTemp.getBounds().getStepBoundsForDiscreteTime(); + if (!boundsToReplace.isEmpty()) { + // exempt first time bound, is handled by standard simple path formula procedure + boundsToReplace.remove(0); + } + boundsToReplace.addAll(exprTemp.getBounds().getRewardBounds()); + + ModelExpressionTransformation transformed = + CounterTransformation.replaceBoundsWithCounters(this, (MDP) model, expr, boundsToReplace, statesOfInterest); + mainLog.println("\nPerforming actual calculations for\n"); + mainLog.println("MDP: "+transformed.getTransformedModel().infoString()); + mainLog.println("Formula: "+transformed.getTransformedExpression() +"\n"); + + // We can now delegate to ProbModelChecker.checkProbPathFormulaSimple as there is + // at most one time / step bound remaining + StateValues svTransformed = super.checkProbPathFormulaSimple(transformed.getTransformedModel(), transformed.getTransformedExpression(), minMax, transformed.getTransformedStatesOfInterest()); + return transformed.projectToOriginalModel(svTransformed); + } else { + // We are fine, delegate to ProbModelChecker.checkProbPathFormulaSimple + return super.checkProbPathFormulaSimple(model, expr, minMax, statesOfInterest); + } + } + + @Override protected StateValues checkProbPathFormulaLTL(Model model, Expression expr, boolean qual, MinMax minMax, BitSet statesOfInterest) throws PrismException {