accumulation: fix off-by-one-error

prism/src/explicit/AccumulationTransformation.java

@@ -171,7 +171,7 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 		String goodLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal", goodStates, product.getTransformedModel().getLabels());
 		// Transform the expression
 		mc.getLog().println(" [AT] replacing the formula...");
-		ReplaceAccumulationExpressionSimple replace = new ReplaceAccumulationExpressionSimple(accexp, goodLabel, product.getNumberOfTracks()-1);
+		ReplaceAccumulationExpressionSimple replace = new ReplaceAccumulationExpressionSimple(accexp, goodLabel, product.getNumberOfTracks()-2);
 		transformedExpression = (Expression)transformedExpression.accept(replace);
 		mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" +
 							"   -> " + transformedExpression.toString());

prism/src/parser/visitor/ReplaceAccumulationBox.java

@@ -45,6 +45,6 @@ public class ReplaceAccumulationBox extends ASTTraverseModify {
 		newAccexp.setSymbol(newSym);
 		newAccexp.setConstraint(newConstr);
 		
-		return Expression.Not(newAccexp);
+		return Expression.Not(Expression.Parenth(newAccexp));
 	}
 }

prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java

@@ -27,7 +27,7 @@ public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify {
 		this.accLength = accLength;
 	}
 	
-	private Object replaceWithUntil(ExpressionAccumulation accexpr) throws PrismLangException {
+	private Object replaceWithUntil(ExpressionAccumulation accexp) throws PrismLangException {
 		// This expression is of the form OR{0..(l-1)}(init_i AND (run_i UNTIL goal_i))
 		
 		// Build all the subexpressions...
@@ -52,13 +52,13 @@ public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify {
 			// until: (run_i UNTIL goal_i)
 			ExpressionTemporal until = new ExpressionTemporal(ExpressionTemporal.P_U, run, goal);
 			// and:   (init_i AND until)
-			ExpressionBinaryOp  and  = new ExpressionBinaryOp(ExpressionBinaryOp.AND, init, until);
+			ExpressionBinaryOp  and  = new ExpressionBinaryOp(ExpressionBinaryOp.AND, init, Expression.Parenth(until));
 			
 			clauses.add(and);
 			if(i==0) {
 				result = and;
 			} else {
-				result = new ExpressionBinaryOp(ExpressionBinaryOp.OR, result, and);
+				result = new ExpressionBinaryOp(ExpressionBinaryOp.OR, result, Expression.Parenth(and));
 			}
 		}
 		return result;