From 82b708ef5bab4ffd44fd80f3578d98d338e44edc Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:26:07 +0200
Subject: [PATCH] imported patch rewardcounter-DTMC-no-negative.patch

---
 prism/src/explicit/CounterTransformation.java | 3 +++
 1 file changed, 3 insertions(+)

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<M extends Model> 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: