From 96b4668afd313e1fd7a120e5bea9dfa1a2d7e048 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:26:04 +0200 Subject: [PATCH] imported patch rewardcounter-continous-time-bounds.patch --- prism/src/explicit/ProbModelChecker.java | 27 ++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) diff --git a/prism/src/explicit/ProbModelChecker.java b/prism/src/explicit/ProbModelChecker.java index 01a8ea2d..db224f80 100644 --- a/prism/src/explicit/ProbModelChecker.java +++ b/prism/src/explicit/ProbModelChecker.java @@ -635,13 +635,28 @@ public class ProbModelChecker extends NonProbModelChecker boolean negated = false; StateValues probs = null; - if (Expression.containsTemporalRewardBounds(expr)) { - throw new PrismNotSupportedException("Can not handle reward bounds."); - } - expr = Expression.convertSimplePathFormulaToCanonicalForm(expr); + ExpressionTemporal exprTemp = Expression.getTemporalOperatorForSimplePathFormula(expr); + + // Here, in the generic method, reward bounds and multiple bounds are not handled. + // If they can be handled, they will have been processed already by a checkProbPathFormulaSimple + // function in a derived model checker class. + if (exprTemp.getBounds().hasRewardBounds()) + throw new PrismNotSupportedException("Reward bounds are not supported in this case for " + model.getModelType()); + if (model.getModelType().continuousTime()) { + if (exprTemp.getBounds().hasStepBounds()) { + throw new PrismNotSupportedException("Step bounds are not supported for continuous time models"); + } + if (exprTemp.getBounds().countTimeBoundsContinuous() > 1) { + throw new PrismNotSupportedException("Multiple time bounds are not supported for continuous time models"); + } + } else { + if (exprTemp.getBounds().countStepBounds() > 1) { + throw new PrismNotSupportedException("Multiple step bounds are not supported by the generic calculator"); + } + } - // Negation + // Negation if (expr instanceof ExpressionUnaryOp && ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) { negated = true; @@ -650,7 +665,7 @@ public class ProbModelChecker extends NonProbModelChecker } if (expr instanceof ExpressionTemporal) { - ExpressionTemporal exprTemp = (ExpressionTemporal) expr; + exprTemp = (ExpressionTemporal) expr; // Next if (exprTemp.getOperator() == ExpressionTemporal.P_X) {