imported patch symb-counter-transform-NondetModelChecker.patch

prism/src/prism/NondetModelChecker.java

@@ -951,15 +951,35 @@ public class NondetModelChecker extends NonProbModelChecker
 
 		expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
 		ExpressionTemporal exprTemp = Expression.getTemporalOperatorForSimplePathFormula(expr);
-		if (exprTemp.getBounds().hasRewardBounds()) {
-			throw new PrismException("Reward bounds are currently not supported with the symbolic engine");
-		}
 
-		if (exprTemp.getBounds().countTimeBoundsDiscrete() > 1) {
-			throw new PrismException("Multiple time / step bounds are currently not supported with the symbolic engine");
+		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<NondetModel, NondetModel> transformed = 
+			    CounterTransformation.replaceBoundsWithCounters(this, model, expr, boundsToReplace, statesOfInterest);
+			mainLog.println("\nPerforming actual calculations for\n");
+			mainLog.println("MDP:  ");
+			transformed.getTransformedModel().printTransInfo(mainLog);
+			mainLog.println("Formula: "+transformed.getTransformedExpression() +"\n");
+
+			NondetModelChecker transformedMC = createNewModelChecker(prism, transformed.getTransformedModel(), propertiesFile);
+			StateValues svTransformed = transformedMC.checkProbPathFormulaSimple(transformed.getTransformedExpression(), qual, min, transformed.getTransformedStatesOfInterest());
+			StateValues svOriginal = transformed.projectToOriginalModel(svTransformed);
+			transformed.clear();
+			return svOriginal;
 		}
 
-		
+		// handle straighforwardly
+
 		// Negation		
 		if (expr instanceof ExpressionUnaryOp &&
 		    ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {