accumulation: untilConstr -> reachConstr

prism/src/explicit/AccumulationContext.java

@@ -13,7 +13,7 @@ public class AccumulationContext {
 	public enum strategy {UNTIL, REACH};
 	public boolean simpleMethod;
 	public boolean singleTrack;
-	public boolean untilConstr;
+	public boolean reachConstr;
 	
 	/** The ingredients */
 	public ExpressionAccumulation accexp;

prism/src/explicit/AccumulationProduct.java

@@ -6,7 +6,6 @@ import java.util.Iterator;
 import java.util.Map;
 
 import parser.ast.AccumulationFactor;
-import parser.ast.Expression;
 import prism.IntegerBound;
 import prism.PrismException;
 

prism/src/explicit/AccumulationTransformation.java

@@ -141,11 +141,12 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		AccumulationContext ctx = new AccumulationContext(accexp, rewards, mc);
 		ctx.singleTrack  = isSingleTrack && !forceMulti;
 		ctx.simpleMethod = isSimple      && !forceComplex;
-		ctx.untilConstr  = (isSimple && isFiltered) || forceUntil;
+		ctx.reachConstr  = (!isSimple || !isFiltered) && !forceUntil;
 		
-		mc.getLog().print("Using optimizations: ");
+		mc.getLog().print("Context flags: ");
 		if(ctx.singleTrack)  { mc.getLog().print(" singleTrack "); }
 		if(ctx.simpleMethod) { mc.getLog().print(" simpleMethod "); }
+		if(ctx.reachConstr)  { mc.getLog().print(" reachConstr" ); }
 		mc.getLog().println();
 		
 		// Build the product
@@ -188,7 +189,7 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		clock.start("replacing formula");
 		ASTVisitor replace;
 		if(ctx.simpleMethod) {
-			replace = new ReplaceAccumulationExpressionSimple(ctx.accexp, goalLabels.get(0), product.getNumberOfTracks()-1, ctx.untilConstr);
+			replace = new ReplaceAccumulationExpressionSimple(ctx.accexp, goalLabels.get(0), product.getNumberOfTracks()-1, ctx.reachConstr);
 		} else {
 			replace = new ReplaceAccumulationExpressionComplex(ctx.accexp, initLabels, runLabels, goalLabels, product.getNumberOfTracks()-1, ctx.singleTrack);
 		}

prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java

@@ -16,14 +16,14 @@ public class ReplaceAccumulationExpressionSimple extends ASTTraverseModify {
 	private ExpressionAccumulation accexp;
 	private String goodLabel;
 	private int accLength;
-	private boolean untilConstr;
+	private boolean reachConstr;
 	
-	public ReplaceAccumulationExpressionSimple(ExpressionAccumulation accexp, String goodLabel, int accLength, boolean untilConstr) {
+	public ReplaceAccumulationExpressionSimple(ExpressionAccumulation accexp, String goodLabel, int accLength, boolean reachConstr) {
 		super();
 		this.accexp = accexp;
 		this.goodLabel = goodLabel;
 		this.accLength = accLength;
-		this.untilConstr = untilConstr;
+		this.reachConstr = reachConstr;
 	}
 	
 	private Object replaceWithReach(ExpressionAccumulation expr) throws PrismLangException {
@@ -86,8 +86,8 @@ public class ReplaceAccumulationExpressionSimple extends ASTTraverseModify {
 	{
 		if (expr == accexp) {
 			// This is a simple accumulation expression. Rewrite to F=.... or to until cascade
-			if (untilConstr) { return replaceWithUntilCascade(expr); }
-			else             { return replaceWithReach(expr); }
+			if (reachConstr) { return replaceWithReach(expr); }
+			else             { return replaceWithUntilCascade(expr); }
 		} else {
 			return expr;
 		}