imported patch symb-counter-transform-ProbModelChecker-protect-dtmc-trew.patch

prism/src/prism/CounterTransformation.java

@@ -204,6 +204,10 @@ public class CounterTransformation<M extends Model> 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) {