prism-accumulation/prism/src/parser/visitor/ReplaceAccumulationBox.java

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 and symbol
		ExpressionAccumulation newAccexp = (ExpressionAccumulation)accexp.deepCopy();
		newAccexp.setSymbol(newSym);
		newAccexp.setConstraint(newConstr);
		
		return Expression.Not(Expression.Parenth(newAccexp));
	}
}