accumulation: reduce box handling to diamonds

prism/src/explicit/AccumulationTransformation.java

@@ -12,6 +12,7 @@ import parser.ast.ExpressionReward;
 import parser.ast.RewardStruct;
 import parser.visitor.ReplaceAccumulationExpressionComplex;
 import parser.visitor.ReplaceAccumulationExpressionSimple;
+import parser.visitor.ReplaceAccumulationBox;
 import prism.PrismException;
 import prism.PrismSettings;
 
@@ -72,6 +73,14 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 		// Get the first ExpressionAccumulation
 		ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpression();
 	    mc.getLog().println(" [AT] for " + accexp);
+	    
+	    // Rewrite it, if it is a BOX
+	    if (accexp.getSymbol().isBox()) {
+	    	ReplaceAccumulationBox replace = new ReplaceAccumulationBox(accexp);
+	    	transformedExpression = (Expression)transformedExpression.accept(replace);
+	    	accexp = transformedExpression.getFirstAccumulationExpression();
+	    	mc.getLog().println(" ... after unboxing: " + accexp + " (in " + transformedExpression + ")");
+	    }
 		
 		// Get the rewards
 	    Vector<Rewards> rewards = new Vector<Rewards>();

prism/src/parser/ast/AccumulationConstraint.java

@@ -31,6 +31,12 @@ public class AccumulationConstraint extends ASTElement {
 	public void setBound(TemporalOperatorBound bound) {
 		this.bound = bound;
 	}
+	
+	public AccumulationConstraint negate() {
+		AccumulationConstraint result = this.deepCopy();
+		result.setBound(result.getBound().invert());
+		return result;
+	}
 
 	public AccumulationConstraint deepCopy() {
 		ArrayList<AccumulationFactor> factorscopy = new ArrayList<AccumulationFactor>();

prism/src/parser/ast/TemporalOperatorBound.java

@@ -274,7 +274,26 @@ public class TemporalOperatorBound extends ASTElement {
 	public Integer getResolvedRewardStructIndex() {
 		return resolvedRewardStructIndex;
 	}
+	
+	/** Get an inverted copy of the bound */
+	public TemporalOperatorBound invert() {
+		TemporalOperatorBound result = new TemporalOperatorBound();
 
+		if (lBound != null) {
+			result.uBound = lBound.deepCopy();
+		}
+		if (uBound != null) {
+			result.lBound = uBound.deepCopy();
+		}
+		result.uBoundStrict = !lBoundStrict;
+		result.lBoundStrict = !uBoundStrict;
+		result.equals = equals;
+		result.boundType = boundType;
+		result.rewardStructureIndex = rewardStructureIndex;
+
+		return result;
+	}
+	
 	@Override
 	public Object accept(ASTVisitor v) throws PrismLangException {
 		return v.visit(this);

prism/src/parser/visitor/ReplaceAccumulationBox.java

@@ -0,0 +1,50 @@
+package parser.visitor;
+
+import parser.ast.AccumulationConstraint;
+import parser.ast.AccumulationSymbol;
+import parser.ast.Expression;
+import parser.ast.ExpressionAccumulation;
+import prism.PrismLangException;
+
+public class ReplaceAccumulationBox extends ASTTraverseModify {
+
+	private ExpressionAccumulation accexp;
+	
+	public ReplaceAccumulationBox(ExpressionAccumulation accexp) {
+		super();
+		this.accexp = accexp;
+	}
+	
+	public Object visit(ExpressionAccumulation expr) throws PrismLangException
+	{
+		// If this is no accexp, we do nothing
+		if (expr != accexp) { return expr; }
+		
+		// Get the symbol, if it is no BOX, we do nothing
+		AccumulationSymbol sym = accexp.getSymbol();
+		if (!sym.isBox()) { return expr; }
+		
+		// Negate the constraint
+		AccumulationConstraint newConstr = accexp.getConstraint().negate();
+		
+		// Switch the symbol
+		AccumulationSymbol newSym;
+		switch(sym) {	
+		case ACCBOXPLUS:
+			newSym = AccumulationSymbol.ACCDIAPLUS;
+			break;
+		case ACCBOXMINUS:
+			newSym = AccumulationSymbol.ACCDIAMINUS;
+			break;
+		default:
+			throw new PrismLangException("Error: Accsymbol is a box and not a box.");
+		}
+		
+		// Make a copy and set constraint an symbol
+		ExpressionAccumulation newAccexp = (ExpressionAccumulation)accexp.deepCopy();
+		newAccexp.setSymbol(newSym);
+		newAccexp.setConstraint(newConstr);
+		
+		return Expression.Not(newAccexp);
+	}
+}