imported patch symb-counter-transform-ProbModelChecker-protect-negative.patch

prism/src/prism/CounterTransformation.java

@@ -206,6 +206,10 @@ public class CounterTransformation<M extends Model> implements ModelExpressionTr
 			JDDNode trew = mc.getTransitionRewardsByIndexObject(rsi, originalModel, mc.constantValues).copy();
 
 			trRewards = JDD.Apply(JDD.PLUS, srew, trew);
+			if (JDD.FindMin(trRewards) < 0) {
+				JDD.Deref(trRewards);
+				throw new PrismException("Can not perform counter transformation in the presence of negative rewards");
+			}
 			break;
 		}
 		case DEFAULT_BOUND: