From 0933901c34932e2c40f7a5331b66df2278b9ef95 Mon Sep 17 00:00:00 2001
From: Sascha Wunderlich <sascha.wunderlich@tu-dresden.de>
Date: Thu, 21 Nov 2019 13:05:54 +0100
Subject: [PATCH] accumulation: untilConstr -> reachConstr

---
 prism/src/explicit/AccumulationContext.java            |  2 +-
 prism/src/explicit/AccumulationProduct.java            |  1 -
 prism/src/explicit/AccumulationTransformation.java     |  7 ++++---
 .../visitor/ReplaceAccumulationExpressionSimple.java   | 10 +++++-----
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/prism/src/explicit/AccumulationContext.java b/prism/src/explicit/AccumulationContext.java
index 08045e4a..b3fafb7d 100644
--- a/prism/src/explicit/AccumulationContext.java
+++ b/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;
diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java
index 97e8388b..719a04fb 100644
--- a/prism/src/explicit/AccumulationProduct.java
+++ b/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;
 
diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java
index 61f253d9..d922ebe1 100644
--- a/prism/src/explicit/AccumulationTransformation.java
+++ b/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);
 		}
diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java b/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java
index 92a29bb5..a7a42012 100644
--- a/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java
+++ b/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;
 		}