Fix accumulation length and single track method

prism/src/explicit/AccumulationProduct.java

@@ -30,6 +30,8 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 	protected final ArrayList<BitSet> labels;
 	
 	protected int numberOfTracks;
+	protected int accumulationLength;
+	
 	protected int numberOfWeights;
 
 	protected final ArrayList<BitSet> initStates;
@@ -54,6 +56,10 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 		return numberOfTracks;
 	}
 	
+	public final int getAccumulationLength() {
+		return accumulationLength;
+	}
+	
 	protected final boolean constraintHolds(final AccumulationTrack<Component> track) throws PrismException {
         return ctx.accexp.getConstraint().holds(ctx, track.getWeights());
 	}
@@ -87,13 +93,16 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 	
 	protected final AccumulationState<Component> updateAccumulationState(final int modelFromStateId, final AccumulationState<Component> accstate, final HashMap<Object, 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)) {
-			// We still need to return an "empty" accstate.
+		
+		if(ctx.singleTrack && (accstate.lastRestartNr == numberOfTracks)) {
+			// We still need to return an "empty" accstate
 			AccumulationState<Component> newAccstate = this.accStates.getById(0);
-			newAccstate.lastRestartNr = numberOfTracks-1;
+			newAccstate.lastRestartNr = numberOfTracks;
 			return newAccstate;
+			//return accstate;
 		}
 		
+		
 		// If this is not a recorded action, we can return the same accstate. Copies are made on modification.
 		if(!recordIn(modelFromStateId)) { return accstate; }
 		// ...otherwise proceed.

prism/src/explicit/AccumulationProductCounting.java

@@ -180,7 +180,14 @@ public class AccumulationProductCounting<M extends Model> extends AccumulationPr
 	}
 	
 	protected void createAuxData(final Model graph) throws PrismException {
-		numberOfTracks  = IntegerBound.fromTemporalOperatorBound(ctx.accexp.getBoundExpression(), ctx.mc.getConstantValues(), true).getHighestInteger()+1;
+		accumulationLength = IntegerBound.fromTemporalOperatorBound(ctx.accexp.getBoundExpression(), ctx.mc.getConstantValues(), true).getHighestInteger();
+		
+		if(ctx.singleTrack) {
+			numberOfTracks = 1;
+		} else {
+			numberOfTracks = accumulationLength + 1; 
+		}
+		
 		numberOfWeights = ctx.rewards.size();
 		
 		if(ctx.simpleMethod) {

prism/src/explicit/AccumulationProductRegular.java

@@ -224,8 +224,14 @@ public class AccumulationProductRegular<M extends Model> extends AccumulationPro
 			throw new PrismException("Cannot handle cyclic automata!");
 		}
 		
-		numberOfTracks = automaton.getLongestPathLength()+1;
-		numberOfWeights= ctx.rewards.size();
+		accumulationLength = automaton.getLongestPathLength(); 
+		numberOfWeights    = ctx.rewards.size();
+		
+		if(ctx.singleTrack) {
+			numberOfTracks = 1;
+		} else {
+			numberOfTracks = accumulationLength + 1;
+		}
 		
 		if(ctx.simpleMethod) {
 			goalStates.add(new BitSet());

prism/src/explicit/AccumulationTransformation.java

@@ -165,6 +165,7 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 
 		if(ctx.simpleMethod) {
 			BitSet goodStates = product.getGoalStates(0);
+			System.out.println(goodStates);
 			String goodLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal", goodStates, product.getTransformedModel().getLabels());
 			
 			goalLabels.add(goodLabel);
@@ -189,12 +190,13 @@ 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.reachConstr);
+			replace = new ReplaceAccumulationExpressionSimple(ctx.accexp, goalLabels.get(0), product.getAccumulationLength(), product.getNumberOfTracks(), ctx.reachConstr);
 		} else {
-			replace = new ReplaceAccumulationExpressionComplex(ctx.accexp, initLabels, runLabels, goalLabels, product.getNumberOfTracks()-1, ctx.singleTrack);
+			replace = new ReplaceAccumulationExpressionComplex(ctx.accexp, initLabels, runLabels, goalLabels, product.getAccumulationLength(), product.getNumberOfTracks());
 		}
 		transformedExpression = (Expression)transformedExpression.accept(replace);
 		clock.stop("got " + transformedExpression);
+		//clock.stop();
 		
 		if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) {
 			product.exportToDotFile("DEBUG-product.dot");

prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java

@@ -17,17 +17,16 @@ public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify {
 	private ArrayList<String> runLabels;
 	private ArrayList<String> goalLabels;
 	private int accLength;
+	private int numberOfTracks;
 	
-	private boolean singleTrack;
-	
-	public ReplaceAccumulationExpressionComplex(ExpressionAccumulation accexp, ArrayList<String> initLabels, ArrayList<String> runLabels, ArrayList<String> goalLabels, int accLength, boolean singleTrack) {
+	public ReplaceAccumulationExpressionComplex(ExpressionAccumulation accexp, ArrayList<String> initLabels, ArrayList<String> runLabels, ArrayList<String> goalLabels, int accLength, int numberOfTracks) {
 		super();
 		this.accexp = accexp;
 		this.initLabels = initLabels;
 		this.runLabels = runLabels;
 		this.goalLabels = goalLabels;
 		this.accLength = accLength;
-		this.singleTrack = singleTrack;
+		this.numberOfTracks = numberOfTracks;
 	}
 	
 	private Object replaceWithUntil(ExpressionAccumulation accexp) throws PrismLangException {
@@ -37,10 +36,7 @@ public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify {
 		ArrayList<Expression> clauses = new ArrayList<>();
 		Expression result = null;
 		
-		for(int i=0; i<accLength; i++) {
-			// if this is singleTrack: break after the first loop
-			if(singleTrack && i>0) { break; }
-			
+		for(int i=0; i<numberOfTracks; i++) {			
 			Expression init = new ExpressionLabel(initLabels.get(i));
 			Expression run  = new ExpressionLabel(runLabels.get(i));
 			Expression goal = new ExpressionLabel(goalLabels.get(i));

prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java

@@ -16,13 +16,15 @@ public class ReplaceAccumulationExpressionSimple extends ASTTraverseModify {
 	private ExpressionAccumulation accexp;
 	private String goodLabel;
 	private int accLength;
+	private int numberOfTracks;
 	private boolean reachConstr;
 	
-	public ReplaceAccumulationExpressionSimple(ExpressionAccumulation accexp, String goodLabel, int accLength, boolean reachConstr) {
+	public ReplaceAccumulationExpressionSimple(ExpressionAccumulation accexp, String goodLabel, int accLength, int numberOfTracks, boolean reachConstr) {
 		super();
 		this.accexp = accexp;
 		this.goodLabel = goodLabel;
 		this.accLength = accLength;
+		this.numberOfTracks = numberOfTracks;
 		this.reachConstr = reachConstr;
 	}
 	
@@ -54,7 +56,7 @@ public class ReplaceAccumulationExpressionSimple extends ASTTraverseModify {
 		}
 		
 		ExpressionLabel label = new ExpressionLabel(goodLabel);
-		
+				
 		Expression current = label;
 		
 		Expression record   = accexp.recordSetExpression();