From 18c6fe77011af3393cb491e1290faa6c37101f6d Mon Sep 17 00:00:00 2001
From: Sascha Wunderlich <sascha.wunderlich@tu-dresden.de>
Date: Thu, 20 Dec 2018 10:32:13 +0100
Subject: [PATCH] accumulation: reduce box handling to diamonds

---
 .../explicit/AccumulationTransformation.java  |  9 ++++
 .../parser/ast/AccumulationConstraint.java    |  6 +++
 .../src/parser/ast/TemporalOperatorBound.java | 19 +++++++
 .../visitor/ReplaceAccumulationBox.java       | 50 +++++++++++++++++++
 4 files changed, 84 insertions(+)
 create mode 100644 prism/src/parser/visitor/ReplaceAccumulationBox.java

diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java
index 684b5568..bd67553d 100644
--- a/prism/src/explicit/AccumulationTransformation.java
+++ b/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>();
diff --git a/prism/src/parser/ast/AccumulationConstraint.java b/prism/src/parser/ast/AccumulationConstraint.java
index 0b5864c5..44e125eb 100644
--- a/prism/src/parser/ast/AccumulationConstraint.java
+++ b/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>();
diff --git a/prism/src/parser/ast/TemporalOperatorBound.java b/prism/src/parser/ast/TemporalOperatorBound.java
index d6d389f3..c4081c8d 100644
--- a/prism/src/parser/ast/TemporalOperatorBound.java
+++ b/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);
diff --git a/prism/src/parser/visitor/ReplaceAccumulationBox.java b/prism/src/parser/visitor/ReplaceAccumulationBox.java
new file mode 100644
index 00000000..22f68ccd
--- /dev/null
+++ b/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);
+	}
+}