diff --git a/prism/src/prism/CounterTransformation.java b/prism/src/prism/CounterTransformation.java index 1bab32c6..5282bbeb 100644 --- a/prism/src/prism/CounterTransformation.java +++ b/prism/src/prism/CounterTransformation.java @@ -206,6 +206,10 @@ public class CounterTransformation 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: