From 29cf893bc3c7a86468ba1f81e2e822dd603eff0e Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:26:26 +0200 Subject: [PATCH] imported patch symb-counter-transform-ProbModelChecker.patch --- prism/src/prism/CounterTransformation.java | 66 ++++++++++++++++++++++ prism/src/prism/ProbModelChecker.java | 40 ++++++++++--- prism/src/prism/RewardCounterProduct.java | 19 +++++++ 3 files changed, 118 insertions(+), 7 deletions(-) diff --git a/prism/src/prism/CounterTransformation.java b/prism/src/prism/CounterTransformation.java index c9d074ce..1bab32c6 100644 --- a/prism/src/prism/CounterTransformation.java +++ b/prism/src/prism/CounterTransformation.java @@ -105,6 +105,9 @@ public class CounterTransformation implements ModelExpressionTr private void doTransformation(M originalModel, List 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 implements ModelExpressionTr } + @SuppressWarnings("unchecked") + private void doTransformation(ProbModel originalModel, List bounds, JDDNode statesOfInterest) throws PrismException + { + List intBounds = new ArrayList(); + + 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) 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 ModelExpressionTransformation replaceBoundsWithCounters(StateModelChecker mc, M originalModel, Expression originalExpression, List bounds, diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index 1995b790..83e22ff8 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/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 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, 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) { diff --git a/prism/src/prism/RewardCounterProduct.java b/prism/src/prism/RewardCounterProduct.java index f8af02e0..5e79fdb6 100644 --- a/prism/src/prism/RewardCounterProduct.java +++ b/prism/src/prism/RewardCounterProduct.java @@ -75,6 +75,25 @@ public class RewardCounterProduct extends Product return new RewardCounterProduct(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 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(originalModel, transformedModel, transform, productStatesOfInterest, transform.getExtraRowVars().copy()); + } /** * Get the states in the product DTMC inside the conjunction of integer bound.