diff --git a/prism/src/explicit/CounterTransformation.java b/prism/src/explicit/CounterTransformation.java index e3fb1ccb..21a1aab0 100644 --- a/prism/src/explicit/CounterTransformation.java +++ b/prism/src/explicit/CounterTransformation.java @@ -174,6 +174,9 @@ public class CounterTransformation implements ModelExpressionTr Integer rewStruct = bounds.get(0).getResolvedRewardStructIndex(); rewards = (MCRewards) mc.constructRewards(originalModel, rewStruct); + if (rewards.hasNegativeRewards()) { + throw new PrismException("Can not perform counter transformation in the presence of negative rewards"); + } break; } case DEFAULT_BOUND: