accumulation: support filtered simple method and until cascades

prism/src/explicit/AccumulationContext.java

@@ -13,6 +13,7 @@ public class AccumulationContext {
 	public enum strategy {UNTIL, REACH};
 	public boolean simpleMethod;
 	public boolean singleTrack;
+	public boolean untilConstr;
 	
 	/** The ingredients */
 	public ExpressionAccumulation accexp;

prism/src/explicit/AccumulationTransformation.java

@@ -125,10 +125,13 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		}
 		
 		// Figure out if we need a complex or a simple trafo...
-		boolean isSimple     = !accexp.hasFireOn() && accexp.isNullary();
+		//boolean isSimple     = !accexp.hasFireOn() && accexp.isNullary();
+		boolean isSimple     = accexp.isNullary();
+		boolean isFiltered   = accexp.hasFireOn();
 		boolean isPast       = accexp.getSymbol().isMinus();
 		boolean forceComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX) || forceComplexFlag;
 		boolean forceMulti   = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_MULTI);
+		boolean forceUntil   = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_UNTIL);
 		
 		if(forceComplex && isPast) {
 			throw new PrismException("Unable to handle <->/[-] with -accforcecomplex. Bailing.");
@@ -138,6 +141,7 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		AccumulationContext ctx = new AccumulationContext(accexp, rewards, mc);
 		ctx.singleTrack  = isSingleTrack && !forceMulti;
 		ctx.simpleMethod = isSimple      && !forceComplex;
+		ctx.untilConstr  = (isSimple && isFiltered) || forceUntil;
 		
 		mc.getLog().print("Using optimizations: ");
 		if(ctx.singleTrack)  { mc.getLog().print(" singleTrack "); }
@@ -184,7 +188,7 @@ 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);
+			replace = new ReplaceAccumulationExpressionSimple(ctx.accexp, goalLabels.get(0), product.getNumberOfTracks()-1, ctx.untilConstr);
 		} else {
 			replace = new ReplaceAccumulationExpressionComplex(ctx.accexp, initLabels, runLabels, goalLabels, product.getNumberOfTracks()-1, ctx.singleTrack);
 		}

prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java

@@ -1,10 +1,13 @@
 package parser.visitor;
 
+import java.util.ArrayList;
+
 import parser.ast.AccumulationSymbol;
+import parser.ast.Expression;
 import parser.ast.ExpressionAccumulation;
+import parser.ast.ExpressionBinaryOp;
 import parser.ast.ExpressionLabel;
 import parser.ast.ExpressionTemporal;
-import parser.ast.ExpressionUnaryOp;
 import parser.ast.TemporalOperatorBound;
 import parser.ast.TemporalOperatorBounds;
 import prism.IntegerBound;
@@ -15,12 +18,14 @@ public class ReplaceAccumulationExpressionSimple extends ASTTraverseModify {
 	private ExpressionAccumulation accexp;
 	private String goodLabel;
 	private int accLength;
+	private boolean untilConstr;
 	
-	public ReplaceAccumulationExpressionSimple(ExpressionAccumulation accexp, String goodLabel, int accLength) {
+	public ReplaceAccumulationExpressionSimple(ExpressionAccumulation accexp, String goodLabel, int accLength, boolean untilConstr) {
 		super();
 		this.accexp = accexp;
 		this.goodLabel = goodLabel;
 		this.accLength = accLength;
+		this.untilConstr = untilConstr;
 	}
 	
 	private Object replaceWithReach(ExpressionAccumulation expr) throws PrismLangException {
@@ -28,32 +33,76 @@ public class ReplaceAccumulationExpressionSimple extends ASTTraverseModify {
 		
 		ExpressionLabel label = new ExpressionLabel(goodLabel);
 		
+		if (sym.isBox()) {
+			throw new PrismLangException("This is a box, which should have been replaced already!");
+		}
+		
 		if (sym.isPlus()) {
 			ExpressionTemporal fExpr = new ExpressionTemporal(ExpressionTemporal.P_F, null, label);
 			TemporalOperatorBounds fBounds = new TemporalOperatorBounds();
 			TemporalOperatorBound  fBound = IntegerBound.fromEqualBounds(accLength).toTemporalOperatorBound();
 			fBounds.setDefaultBound(fBound);
 			fExpr.setBounds(fBounds);
-			// If its a BOX, negate it
-			if (sym.isBox()) {
-				return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, fExpr);
-			} else {
-				return fExpr;
-			}
+			return fExpr;
 		} else { //isMinus
-			if (sym.isBox()) {
-				return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, label);
-			} else {
-				return label;
+			return label;
+		}
+	}
+	
+	//TODO: Fixme
+	private Object replaceWithUntilCascade(ExpressionAccumulation expr) throws PrismLangException {
+		AccumulationSymbol sym = accexp.getSymbol();
+		if(sym.isMinus()) {
+			throw new PrismLangException("Tried to handle past with untilCascade. Bailing...");
+		}
+		
+		ExpressionLabel label = new ExpressionLabel(goodLabel);
+		
+		Expression current = label;
+		
+		// TODO: moveme
+		Expression notfiltered = Expression.True();
+		if(accexp.hasFireOn()) {
+			// Build the fireOn expressions
+			ArrayList<Expression> fireOn = accexp.getFireOn();
+			
+			notfiltered = fireOn.get(0);
+			for(int i=1;i<fireOn.size();i++) {
+				notfiltered = new ExpressionBinaryOp(ExpressionBinaryOp.OR, notfiltered, fireOn.get(i));
 			}
+			System.out.println("notfiltered: " + notfiltered);
+		}
+
+		Expression filtered = Expression.Not(notfiltered);
+			
+		// Build the following tree:
+		//          U
+		// filtered   and
+		//      notfil   next
+		//               current
+		for(int i=0;i<accLength;i++) {
+			// X current
+			ExpressionTemporal xCurrent = new ExpressionTemporal(ExpressionTemporal.P_X, null, current);
+			
+			// notfil & xCurrent
+			ExpressionBinaryOp and = new ExpressionBinaryOp(ExpressionBinaryOp.AND, notfiltered, xCurrent);
+			
+			// filtered U and
+			ExpressionTemporal until = new ExpressionTemporal(ExpressionTemporal.P_U, filtered, and);
+			
+			// Set this for the next round
+			current = Expression.Parenth(until);
 		}
+		
+		return current;
 	}
 	
 	public Object visit(ExpressionAccumulation expr) throws PrismLangException
 	{
 		if (expr == accexp) {
-			// This is a simple accumulation expression. Rewrite to F=....
-			return replaceWithReach(expr);
+			// This is a simple accumulation expression. Rewrite to F=.... or to until cascade
+			if (untilConstr) { return replaceWithUntilCascade(expr); }
+			else             { return replaceWithReach(expr); }
 		} else {
 			return expr;
 		}

prism/src/prism/PrismSettings.java

@@ -162,6 +162,7 @@ public class PrismSettings implements Observer
 	public static final String ACC_GENERATE_DOTS                    = "accumulation.generateDots";
 	public static final String ACC_FORCE_COMPLEX                    = "accumulation.forceComplex";
 	public static final String ACC_FORCE_MULTI						= "accumulation.forceMulti";
+	public static final String ACC_FORCE_UNTIL						= "accumulation.forceUntil";
 	
 	//GUI Model
 	public static final	String MODEL_AUTO_PARSE						= "model.autoParse";
@@ -418,7 +419,8 @@ public class PrismSettings implements Observer
 		{
 			{ BOOLEAN_TYPE,     ACC_GENERATE_DOTS,                      "Accumulation: generate DOT files",     "4.4",          false, "", "Generate DOT files for accumulation monitors and products"},
 			{ BOOLEAN_TYPE,     ACC_FORCE_COMPLEX,                      "Accumulation: force U-construction",   "4.4",          false, "", "Force complex accumulation construction"},
-			{ BOOLEAN_TYPE,     ACC_FORCE_MULTI,                        "Accumulation: force multiple tracks",  "4.4",          false, "", "Force multiple accumulation tracks"}
+			{ BOOLEAN_TYPE,     ACC_FORCE_MULTI,                        "Accumulation: force multiple tracks",  "4.4",          false, "", "Force multiple accumulation tracks"},
+			{ BOOLEAN_TYPE,     ACC_FORCE_UNTIL,                        "Accumulation: force cascading until",  "4.4",          false, "", "Force until accumulation construction"}
 
 		},
 		{
@@ -1706,6 +1708,10 @@ public class PrismSettings implements Observer
 		else if (sw.equals("accforcemulti")) {
 			set(ACC_FORCE_MULTI, true);
 		}
+		
+		else if (sw.equals("accforceuntil")) {
+			set(ACC_FORCE_UNTIL, true);
+		}
 
 		// HIDDEN OPTIONS