From 99d91a5f9d6d700dc43545973f4e40a65ed390d8 Mon Sep 17 00:00:00 2001
From: Sascha Wunderlich <sascha.wunderlich@tu-dresden.de>
Date: Fri, 7 Dec 2018 17:20:12 +0100
Subject: [PATCH] accumulation: fix behaviour for step 0

---
 prism/src/explicit/AccumulationProductCounting.java | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/prism/src/explicit/AccumulationProductCounting.java b/prism/src/explicit/AccumulationProductCounting.java
index 46201730..ca434f93 100644
--- a/prism/src/explicit/AccumulationProductCounting.java
+++ b/prism/src/explicit/AccumulationProductCounting.java
@@ -153,8 +153,11 @@ public class AccumulationProductCounting<M extends Model> extends AccumulationPr
 			throws PrismException {
 		boolean isFinal = false;
 		if ( track != null ) {
-			IntegerBound stepBound = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true);
-			isFinal = stepBound.isInBounds(track.getComponent());
+			Integer step = track.getComponent();
+			if ( step > 0 ) { // if the step is 0, we cannot have a goal state.
+				IntegerBound stepBound = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true);
+				isFinal = stepBound.isInBounds(step);
+			}
 		}
 		return isFinal;
 	}