imported patch rewardcounter-MDPModelChecker.simple-path-formulas-with-bounds.patch

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<TemporalOperatorBound> 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<MDP, MDP> 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
 	{