diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index 86150f9b..97e8388b 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -93,22 +93,16 @@ public abstract class AccumulationProduct extends Pro return new AccumulationTrack(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 updateAccumulationState(final int modelFromStateId, final AccumulationState 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. diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index af84a7c9..61f253d9 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -127,7 +127,7 @@ public class AccumulationTransformation 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); diff --git a/prism/src/parser/PrismParser.java b/prism/src/parser/PrismParser.java index 2f98c0b1..efb80ef9 100644 --- a/prism/src/parser/PrismParser.java +++ b/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; } diff --git a/prism/src/parser/ast/ExpressionAccumulation.java b/prism/src/parser/ast/ExpressionAccumulation.java index b93affc1..0163cf90 100644 --- a/prism/src/parser/ast/ExpressionAccumulation.java +++ b/prism/src/parser/ast/ExpressionAccumulation.java @@ -41,7 +41,7 @@ public class ExpressionAccumulation extends Expression AccumulationConstraint constraint; ExpressionRegular regexp; TemporalOperatorBound bound; - ArrayList fireOn; + ArrayList recordSet; Expression operand1 = null; Expression operand2 = null; @@ -110,16 +110,27 @@ public class ExpressionAccumulation extends Expression } } - public ArrayList getFireOn() { - return fireOn; + public ArrayList getRecordSet() { + return recordSet; } - public void setFireOn(ArrayList fireOn) { - this.fireOn = fireOn; + public void setRecordSet(ArrayList 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 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(this.getFireOn().size())); - for(Expression e : this.getFireOn()) { - ret.fireOn.add(e.deepCopy()); + if ( this.hasRecordSet() ) { + ret.setRecordSet(new ArrayList(this.getRecordSet().size())); + for(Expression e : this.getRecordSet()) { + ret.recordSet.add(e.deepCopy()); } } diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java b/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java index ff3b1925..9d2d0151 100644 --- a/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java +++ b/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 { diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java b/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java index 45921dbb..92a29bb5 100644 --- a/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java +++ b/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 fireOn = accexp.getFireOn(); - - notfiltered = fireOn.get(0); - for(int i=1;i