diff --git a/prism/src/prism/CounterTransformation.java b/prism/src/prism/CounterTransformation.java index 5282bbeb..694c18ac 100644 --- a/prism/src/prism/CounterTransformation.java +++ b/prism/src/prism/CounterTransformation.java @@ -204,6 +204,10 @@ public class CounterTransformation implements ModelExpressionTr Object rsi = bounds.get(0).getRewardStructureIndex(); JDDNode srew = mc.getStateRewardsByIndexObject(rsi, originalModel, mc.constantValues).copy(); JDDNode trew = mc.getTransitionRewardsByIndexObject(rsi, originalModel, mc.constantValues).copy(); + if (!trew.equals(JDD.ZERO)) { + JDD.Deref(srew, trew); + throw new PrismException("Can not perform counter transformation for transition rewards in " + originalModel.getModelType()); + } trRewards = JDD.Apply(JDD.PLUS, srew, trew); if (JDD.FindMin(trRewards) < 0) {