accumulation: stuttering -> recording

prism/src/explicit/AccumulationProduct.java

@@ -93,22 +93,16 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 		return new AccumulationTrack<Component>(newweights, nextComponent);
 	}
 	
-	private boolean stutterIn(int stateId) throws PrismException {
-		if(!ctx.accexp.hasFireOn()) { return false; }
-		for(Expression f : ctx.accexp.getFireOn()) {
-			if(ctx.mc.checkExpression(originalModel, f, null).getBitSet().get(stateId)) {
-				return false;
-			}
-		}
-		return true;
+	private boolean recordIn(int stateId) throws PrismException {
+		return ctx.mc.checkExpression(originalModel, ctx.accexp.recordSetExpression(), null).getBitSet().get(stateId);
 	}
 	
 	protected final AccumulationState<Component> updateAccumulationState(final int modelFromStateId, final AccumulationState<Component> accstate, final double[] weights) throws PrismException {
 		// If we are in singleTrack mode and the last restart is the numberOfTracks, we can stop...
 		if(ctx.singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) { return accstate; }
 		
-		// If this is a stutter action, we can return the same accstate. Copies are made on modification.
-		if(stutterIn(modelFromStateId)) { return accstate; }
+		// If this is not a recorded action, we can return the same accstate. Copies are made on modification.
+		if(!recordIn(modelFromStateId)) { return accstate; }
 		// ...otherwise proceed.
 		
 		// Get the old tracker and tracks.

prism/src/explicit/AccumulationTransformation.java

@@ -127,7 +127,7 @@ 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.isNullary();
-		boolean isFiltered   = accexp.hasFireOn();
+		boolean isFiltered   = accexp.hasRecordSet();
 		boolean isPast       = accexp.getSymbol().isMinus();
 		boolean forceComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX) || forceComplexFlag;
 		boolean forceMulti   = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_MULTI);

prism/src/parser/PrismParser.java

@@ -1772,7 +1772,7 @@ accexp.setConstraint(constr);
         case LPARENTH:{
           jj_consume_token(LPARENTH);
           fireOn = ExpressionAccumulationFire();
-accexp.setFireOn(fireOn);
+accexp.setRecordSet(fireOn);
           jj_consume_token(RPARENTH);
           break;
           }
@@ -1980,7 +1980,7 @@ ret.setConstraint(constr);
     case LPARENTH:{
       jj_consume_token(LPARENTH);
       fireOn = ExpressionAccumulationFire();
-ret.setFireOn(fireOn);
+ret.setRecordSet(fireOn);
       jj_consume_token(RPARENTH);
       break;
       }

prism/src/parser/ast/ExpressionAccumulation.java

@@ -41,7 +41,7 @@ public class ExpressionAccumulation extends Expression
 	AccumulationConstraint constraint;
 	ExpressionRegular regexp;
 	TemporalOperatorBound bound;
-	ArrayList<Expression> fireOn;
+	ArrayList<Expression> recordSet;
 	
 	Expression operand1 = null;
 	Expression operand2 = null;
@@ -110,16 +110,27 @@ public class ExpressionAccumulation extends Expression
 		}
 	}
 	
-	public ArrayList<Expression> getFireOn() {
-		return fireOn;
+	public ArrayList<Expression> getRecordSet() {
+		return recordSet;
 	}
 
-	public void setFireOn(ArrayList<Expression> fireOn) {
-		this.fireOn = fireOn;
+	public void setRecordSet(ArrayList<Expression> fireOn) {
+		this.recordSet = fireOn;
 	}
 	
-	public boolean hasFireOn() {
-		return fireOn != null;
+	public boolean hasRecordSet() {
+		return recordSet != null;
+	}
+	
+	public Expression recordSetExpression() {
+		if(!hasRecordSet()) { return Expression.True(); }
+		
+		Expression ret = recordSet.get(0);
+		for(int i=1;i<recordSet.size();i++) {
+			ret = new ExpressionBinaryOp(ExpressionBinaryOp.OR, ret, recordSet.get(i));
+		}
+		
+		return ret;
 	}
 	
 	public boolean isNullary() {
@@ -140,8 +151,8 @@ public class ExpressionAccumulation extends Expression
 		
 		ret += "(" + constraint.toString() + ")";
 		
-		if ( hasFireOn() ) {
-			String fireOnString = fireOn.stream().map(f -> f.toString()).collect(Collectors.joining(","));
+		if ( hasRecordSet() ) {
+			String fireOnString = recordSet.stream().map(f -> f.toString()).collect(Collectors.joining(","));
 			ret += "(" + fireOnString + ")";
 		}
 		
@@ -186,10 +197,10 @@ public class ExpressionAccumulation extends Expression
 		if ( this.hasRegularExpression() ) {
 			ret.setRegularExpression((ExpressionRegular) this.getRegularExpression().deepCopy());
 		}
-		if ( this.hasFireOn() ) {
-			ret.setFireOn(new ArrayList<Expression>(this.getFireOn().size()));
-			for(Expression e : this.getFireOn()) {
-				ret.fireOn.add(e.deepCopy());
+		if ( this.hasRecordSet() ) {
+			ret.setRecordSet(new ArrayList<Expression>(this.getRecordSet().size()));
+			for(Expression e : this.getRecordSet()) {
+				ret.recordSet.add(e.deepCopy());
 			}
 		}
 		

prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java

@@ -62,7 +62,7 @@ public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify {
 			ExpressionTemporal xuntil = new ExpressionTemporal(ExpressionTemporal.P_X, null, Expression.Parenth(until));
 			
 			Expression clause;
-			if(accexp.hasFireOn()) {
+			if(accexp.hasRecordSet()) {
 				// until: (init_i UNTIL until)
 				clause    = new ExpressionTemporal(ExpressionTemporal.P_U, init, xuntil);
 			} else {

prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java

@@ -1,7 +1,5 @@
 package parser.visitor;
 
-import java.util.ArrayList;
-
 import parser.ast.AccumulationSymbol;
 import parser.ast.Expression;
 import parser.ast.ExpressionAccumulation;
@@ -49,7 +47,6 @@ public class ReplaceAccumulationExpressionSimple extends ASTTraverseModify {
 		}
 	}
 	
-	//TODO: Fixme
 	private Object replaceWithUntilCascade(ExpressionAccumulation expr) throws PrismLangException {
 		AccumulationSymbol sym = accexp.getSymbol();
 		if(sym.isMinus()) {
@@ -60,20 +57,8 @@ public class ReplaceAccumulationExpressionSimple extends ASTTraverseModify {
 		
 		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);
+		Expression record   = accexp.recordSetExpression();
+		Expression norecord = Expression.Not(record);
 			
 		// Build the following tree:
 		//          U
@@ -85,10 +70,10 @@ public class ReplaceAccumulationExpressionSimple extends ASTTraverseModify {
 			ExpressionTemporal xCurrent = new ExpressionTemporal(ExpressionTemporal.P_X, null, current);
 			
 			// notfil & xCurrent
-			ExpressionBinaryOp and = new ExpressionBinaryOp(ExpressionBinaryOp.AND, notfiltered, xCurrent);
+			ExpressionBinaryOp and = new ExpressionBinaryOp(ExpressionBinaryOp.AND, record, xCurrent);
 			
 			// filtered U and
-			ExpressionTemporal until = new ExpressionTemporal(ExpressionTemporal.P_U, filtered, and);
+			ExpressionTemporal until = new ExpressionTemporal(ExpressionTemporal.P_U, norecord, and);
 			
 			// Set this for the next round
 			current = Expression.Parenth(until);