From 91554ae55e1e7236b2dac18e7ae55b71d95d8b5f Mon Sep 17 00:00:00 2001
From: Sascha Wunderlich <sascha.wunderlich@tu-dresden.de>
Date: Mon, 7 Jan 2019 15:30:43 +0100
Subject: [PATCH] accumulation: fix stuttering in the beginning

---
 prism/src/explicit/AccumulationProduct.java   | 25 +++++++++----------
 prism/src/explicit/AccumulationState.java     |  4 ---
 .../ReplaceAccumulationExpressionComplex.java | 19 +++++++++-----
 3 files changed, 25 insertions(+), 23 deletions(-)

diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java
index c731b338..01071919 100644
--- a/prism/src/explicit/AccumulationProduct.java
+++ b/prism/src/explicit/AccumulationProduct.java
@@ -92,23 +92,22 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 		return new AccumulationTrack<Component>(newweights, nextComponent);
 	}
 	
+	private boolean stutterIn(int stateId) throws PrismException {
+		if(!ctx.accexp.hasFireOn()) { return false; }
+		for(Expression f : ctx.accexp.getFireOn()) {
+			if(ctx.mc.checkExpression(originalModel, f, null).getBitSet().get(stateId)) {
+				return false;
+			}
+		}
+		return true;
+	}
+	
 	protected final AccumulationState<Component> updateAccumulationState(final int modelFromStateId, final AccumulationState<Component> accstate, final double[] weights) throws PrismException {
 		// If we are in singleTrack mode and the last restart is the numberOfTracks, we can stop...
 		if(ctx.singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) { return accstate; }
 		
-		// Check if we even need to fire here.
-		if(ctx.accexp.hasFireOn()) {
-			boolean stutter = true;
-			for(Expression f : ctx.accexp.getFireOn()) {
-				if(ctx.mc.checkExpression(originalModel, f, null).getBitSet().get(modelFromStateId)) {
-					//mc.getLog().println("f:" + f);
-					stutter = false;
-					break;
-				}
-			}
-			// If this is a stutter action, we can return the same accstate. Copies are made on modification.
-			if(stutter) { return accstate; }
-		}
+		// If this is a stutter action, we can return the same accstate. Copies are made on modification.
+		if(stutterIn(modelFromStateId)) { return accstate; }
 		// ...otherwise proceed.
 		
 		// Get the old tracker and tracks.
diff --git a/prism/src/explicit/AccumulationState.java b/prism/src/explicit/AccumulationState.java
index 0e0b6742..987c65b7 100644
--- a/prism/src/explicit/AccumulationState.java
+++ b/prism/src/explicit/AccumulationState.java
@@ -44,10 +44,6 @@ public class AccumulationState<Component> {
 		return (lastRestartNr + 1) % numberOfTracks;
 	}
 	
-	public boolean hasGoodTracks() {
-		return !goodTracks.isEmpty();
-	}
-	
 	public boolean importantTrackIsGood() {
 		return goodTracks.get(getNextRestartNr());
 	}
diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java b/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java
index d0caaedb..6d242619 100644
--- a/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java
+++ b/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java
@@ -31,7 +31,7 @@ public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify {
 		// This expression is of the form OR{0..(l-1)}(init_i AND (run_i UNTIL goal_i))
 		
 		// Build all the subexpressions...
-		ArrayList<ExpressionBinaryOp> clauses = new ArrayList<>();
+		ArrayList<Expression> clauses = new ArrayList<>();
 		Expression result = null;
 		
 		for(int i=0; i<accLength; i++) {
@@ -54,14 +54,21 @@ public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify {
 			ExpressionTemporal until  = new ExpressionTemporal(ExpressionTemporal.P_U, run, goal);
 			// xuntil:(X until)
 			ExpressionTemporal xuntil = new ExpressionTemporal(ExpressionTemporal.P_X, null, Expression.Parenth(until));
-			// and:   (init_i AND until)
-			ExpressionBinaryOp and    = new ExpressionBinaryOp(ExpressionBinaryOp.AND, init, xuntil);
 			
-			clauses.add(and);
+			Expression clause;
+			if(accexp.hasFireOn()) {
+				// until: (init_i UNTIL until)
+				clause    = new ExpressionTemporal(ExpressionTemporal.P_U, init, xuntil);
+			} else {
+				// and:   (init_i AND until)
+				clause    = new ExpressionBinaryOp(ExpressionBinaryOp.AND, init, xuntil);
+			}
+			
+			clauses.add(clause);
 			if(i==0) {
-				result = and;
+				result = clause;
 			} else {
-				result = new ExpressionBinaryOp(ExpressionBinaryOp.OR, result, Expression.Parenth(and));
+				result = new ExpressionBinaryOp(ExpressionBinaryOp.OR, result, Expression.Parenth(clause));
 			}
 		}
 		return result;