From 51b031952064a659ceb1e0af059a981f7edd872f Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:26:28 +0200
Subject: [PATCH] imported patch
 symb-counter-transform-ProbModelChecker-protect-dtmc-trew.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 5282bbeb..694c18ac 100644
--- a/prism/src/prism/CounterTransformation.java
+++ b/prism/src/prism/CounterTransformation.java
@@ -204,6 +204,10 @@ public class CounterTransformation<M extends Model> implements ModelExpressionTr
 			Object rsi = bounds.get(0).getRewardStructureIndex();
 			JDDNode srew = mc.getStateRewardsByIndexObject(rsi, originalModel, mc.constantValues).copy();
 			JDDNode trew = mc.getTransitionRewardsByIndexObject(rsi, originalModel, mc.constantValues).copy();
+			if (!trew.equals(JDD.ZERO)) {
+				JDD.Deref(srew, trew);
+				throw new PrismException("Can not perform counter transformation for transition rewards in " + originalModel.getModelType());
+			}
 
 			trRewards = JDD.Apply(JDD.PLUS, srew, trew);
 			if (JDD.FindMin(trRewards) < 0) {