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 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; }