From 6b87fcf172e4ef3f1e0cf080b7885a273dfef1f7 Mon Sep 17 00:00:00 2001
From: Sascha Wunderlich <sascha.wunderlich@tu-dresden.de>
Date: Fri, 21 Dec 2018 11:22:56 +0100
Subject: [PATCH] accumulation: fix bound check

---
 prism/src/explicit/AccumulationProduct.java        | 2 +-
 prism/src/explicit/AccumulationTransformation.java | 4 +---
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java
index e1a4781e..798670a2 100644
--- a/prism/src/explicit/AccumulationProduct.java
+++ b/prism/src/explicit/AccumulationProduct.java
@@ -58,7 +58,7 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
         }
 
         // Check the bound
-        IntegerBound rhs = IntegerBound.fromTemporalOperatorBound(accexp.getConstraint().getBound(), mc.getConstantValues(), true);
+        IntegerBound rhs = IntegerBound.fromTemporalOperatorBound(accexp.getConstraint().getBound(), mc.getConstantValues(), false);
         
         return rhs.isInBounds(lhs);
 	}
diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java
index db4ce83b..048a2d08 100644
--- a/prism/src/explicit/AccumulationTransformation.java
+++ b/prism/src/explicit/AccumulationTransformation.java
@@ -71,9 +71,7 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		transformedExpression = mc.handleMaximalStateFormulas(originalModel, originalExpression);
 		
 		mc.getLog().println("Performing accumulation transformation...");
-		
-		// TODO: WHILE getFirstAccumulationExpression
-		
+				
 		// Get the first ExpressionAccumulation
 		boolean singleTrack = true;
 		ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpressionWithoutTemporal();