From c4bd020074634f22b4531bd0fcf200f8c5f89f11 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:26:27 +0200
Subject: [PATCH] imported patch
 symb-counter-transform-ProbModelChecker-protect-negative.patch

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

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<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: