imported patch symb-counter-transform-ProbModelChecker.patch

prism/src/prism/CounterTransformation.java

@@ -105,6 +105,9 @@ public class CounterTransformation<M extends Model> implements ModelExpressionTr
 	private void doTransformation(M originalModel, List<TemporalOperatorBound> bounds, JDDNode statesOfInterest) throws PrismException {	
 		if (originalModel instanceof NondetModel) {
 				doTransformation((NondetModel)originalModel, bounds, statesOfInterest);
+		} else if (originalModel instanceof ProbModel) {
+			doTransformation((ProbModel)originalModel, bounds, statesOfInterest);
+
 		} else {
 			throw new PrismException("Counter-Transformation is not supported for "+originalModel.getClass());
 		}
@@ -176,6 +179,69 @@ public class CounterTransformation<M extends Model> implements ModelExpressionTr
 	}
 
 
+	@SuppressWarnings("unchecked")
+	private void doTransformation(ProbModel originalModel, List<TemporalOperatorBound> bounds, JDDNode statesOfInterest) throws PrismException
+	{
+		List<IntegerBound> intBounds = new ArrayList<IntegerBound>();
+
+		if (bounds.isEmpty()) {
+			throw new IllegalArgumentException("Can not do counter transformation without any bounds.");
+		}
+
+		for (TemporalOperatorBound bound : bounds) {
+			IntegerBound intBound = IntegerBound.fromTemporalOperatorBound(bound, mc.constantValues, true);
+			intBounds.add(intBound);
+
+			if (!bound.hasSameDomainDiscreteTime(bounds.get(0))) {
+				throw new IllegalArgumentException("Can only do counter transformation for bounds with same domain.");
+			}
+		}
+		JDDNode trRewards = null;
+
+		switch (bounds.get(0).getBoundType()) {
+		case REWARD_BOUND: {
+			// Get reward info
+			Object rsi = bounds.get(0).getRewardStructureIndex();
+			JDDNode srew = mc.getStateRewardsByIndexObject(rsi, originalModel, mc.constantValues).copy();
+			JDDNode trew = mc.getTransitionRewardsByIndexObject(rsi, originalModel, mc.constantValues).copy();
+
+			trRewards = JDD.Apply(JDD.PLUS, srew, trew);
+			break;
+		}
+		case DEFAULT_BOUND:
+		case STEP_BOUND:
+		case TIME_BOUND:
+			// a time/step bound, use constant reward structure assigning 1 to each state
+			trRewards = JDD.Constant(1);
+			break;
+		}
+
+		if (trRewards == null) {
+			throw new PrismException("Couldn't generate reward information.");
+		}
+
+		int saturation_limit = IntegerBound.getMaximalInterestingValueForConjunction(intBounds);
+
+		product = (RewardCounterProduct<M>) RewardCounterProduct.generate(mc.prism, originalModel, trRewards, saturation_limit, statesOfInterest);
+
+		// add 'in_bound-x' label
+		JDDNode statesInBound = product.getStatesWithAccumulatedRewardInBoundConjunction(intBounds);
+		//JDD.PrintMinterms(mc.prism.getMainLog(), statesInBound.copy(), "statesInBound (1)");
+		statesInBound = JDD.And(statesInBound, product.getTransformedModel().getReach().copy());
+		//JDD.PrintMinterms(mc.prism.getMainLog(), statesInBound.copy(), "statesInBound (2)");
+		String labelInBound = ((ProbModel)product.getTransformedModel()).addUniqueLabelDD("in_bound", statesInBound, mc.getDefinedLabelNames());
+
+		// transform expression
+		for (TemporalOperatorBound bound : bounds) {
+			ReplaceBound replace = new ReplaceBound(bound, labelInBound);
+			transformedExpression = (Expression) transformedExpression.accept(replace);
+
+			if (!replace.wasSuccessfull()) {
+				throw new PrismException("Replacing bound was not successfull.");
+			}
+		}
+	}
+	
 	public static <M extends Model> ModelExpressionTransformation<M, M> replaceBoundsWithCounters(StateModelChecker mc,
 			M originalModel, Expression originalExpression,
 			List<TemporalOperatorBound> bounds,

prism/src/prism/ProbModelChecker.java

@@ -56,6 +56,7 @@ import parser.ast.ExpressionTemporal;
 import parser.ast.ExpressionUnaryOp;
 import parser.ast.PropertiesFile;
 import parser.ast.RelOp;
+import parser.ast.TemporalOperatorBound;
 import parser.type.TypeBool;
 import parser.type.TypePathBool;
 import parser.type.TypePathDouble;
@@ -503,14 +504,39 @@ public class ProbModelChecker 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
+			
+			if (model.getModelType().continuousTime()) {
+				throw new PrismNotSupportedException("Reward bounds for continuous time not supported yet");
+			}
+			
+			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<ProbModel, ProbModel> transformed = 
+			    CounterTransformation.replaceBoundsWithCounters(this, model, expr, boundsToReplace, statesOfInterest);
+			mainLog.println("\nPerforming actual calculations for\n");
+			mainLog.println("DTMC:  ");
+			transformed.getTransformedModel().printTransInfo(mainLog);
+			mainLog.println("Formula: "+transformed.getTransformedExpression() +"\n");
+
+			ProbModelChecker transformedMC = createNewModelChecker(prism, transformed.getTransformedModel(), propertiesFile);
+			StateValues svTransformed = transformedMC.checkProbPathFormulaSimple(transformed.getTransformedExpression(), qual, transformed.getTransformedStatesOfInterest());
+			StateValues svOriginal = transformed.projectToOriginalModel(svTransformed);
+			transformed.clear();
+			return svOriginal;
 		}
-		
+
+		// handle straighforwardly
+
 		// Negation		
 		if (expr instanceof ExpressionUnaryOp &&
 		    ((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {

prism/src/prism/RewardCounterProduct.java

@@ -75,6 +75,25 @@ public class RewardCounterProduct<M extends Model> extends Product<M>
 		return new RewardCounterProduct<NondetModel>(originalModel, transformedModel, transform, productStatesOfInterest, transform.getExtraRowVars().copy());
 	}
 
+	/**
+	 * Generate the product of a DTMC with an accumulated reward counter.
+	 * The counter has the range [0,limit], with saturation semantics for accumulated
+	 * rewards >=limit.
+	 * @param originalModel the DTMC
+	 * @param rewards integer MCRewards
+	 * @param limit the saturation value for the counter
+	 * @param statesOfInterest the set of state of interest, the starting point for the counters
+	 * @return
+	 * @throws PrismException
+	 */
+	static public RewardCounterProduct<ProbModel> generate(PrismComponent parent, ProbModel originalModel, JDDNode trRewards, int limit, JDDNode statesOfInterest) throws PrismException {
+		TransitionsByRewardsInfo info = new TransitionsByRewardsInfo(parent, originalModel, trRewards);
+		RewardCounterTransformationAdd transform = new RewardCounterTransformationAdd(originalModel, info, limit, statesOfInterest);
+	
+		ProbModel transformedModel = originalModel.getTransformed(transform);
+		JDDNode productStatesOfInterest = transformedModel.getStart().copy();
+		return new RewardCounterProduct<ProbModel>(originalModel, transformedModel, transform, productStatesOfInterest, transform.getExtraRowVars().copy());
+	}
 
 	/**
 	 * Get the states in the product DTMC inside the conjunction of integer bound.