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 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 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();