Browse Source

accumulation: fix bound check

accumulation
Sascha Wunderlich 7 years ago
parent
commit
6b87fcf172
  1. 2
      prism/src/explicit/AccumulationProduct.java
  2. 4
      prism/src/explicit/AccumulationTransformation.java

2
prism/src/explicit/AccumulationProduct.java

@ -58,7 +58,7 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
} }
// Check the bound // 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); return rhs.isInBounds(lhs);
} }

4
prism/src/explicit/AccumulationTransformation.java

@ -71,9 +71,7 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
transformedExpression = mc.handleMaximalStateFormulas(originalModel, originalExpression); transformedExpression = mc.handleMaximalStateFormulas(originalModel, originalExpression);
mc.getLog().println("Performing accumulation transformation..."); mc.getLog().println("Performing accumulation transformation...");
// TODO: WHILE getFirstAccumulationExpression
// Get the first ExpressionAccumulation // Get the first ExpressionAccumulation
boolean singleTrack = true; boolean singleTrack = true;
ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpressionWithoutTemporal(); ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpressionWithoutTemporal();

Loading…
Cancel
Save