diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index 719a04fb..25b2ed0a 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -98,7 +98,12 @@ public abstract class AccumulationProduct extends Pro 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(ctx.singleTrack && (accstate.lastRestartNr == numberOfTracks-1)) { + // We still need to return an "empty" accstate. + AccumulationState newAccstate = this.accStates.getById(0); + newAccstate.lastRestartNr = numberOfTracks-1; + return newAccstate; + } // If this is not a recorded action, we can return the same accstate. Copies are made on modification. if(!recordIn(modelFromStateId)) { return accstate; } diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index a2c4756e..bcfee6d3 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -514,10 +514,10 @@ TOKEN : | < QMARK: "?" > | < CARET: "^" > // Accumulation -| < ACCDIAPLUS: "<+>" > -| < ACCDIAMINUS: "<->" > -| < ACCBOXPLUS: "[+]" > -| < ACCBOXMINUS: "[-]" > +| < ACCDIAPLUS: "<+>"|"F+" > +| < ACCDIAMINUS: "<->"|"F-" > +| < ACCBOXPLUS: "[+]"|"G+" > +| < ACCBOXMINUS: "[-]"|"G-" > | < ACCUNTIL: "U+" > // Regular expressions | < REG_INT: (["1"-"9"](["0"-"9"])*)|("0") > @@ -1180,26 +1180,26 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) : // Accumulation symbol { accexp = new ExpressionAccumulation(AccumulationSymbol.ACCUNTIL); accexp.setOperand1(ret); } // Regular expression, should be star-free - + ( ( reg = ExpressionRegularUnary(prop, false) { accexp.setRegularExpression((ExpressionRegular)reg); } ) | ( bound = BoundExpression() { accexp.setBoundExpression(bound); } ) ) - + // Weight constraint - + ( constr = ExpressionAccumulationConstraint() { accexp.setConstraint(constr); } ) - - // Fire set (= !StutterSet) - ( + + // Record set (= !StutterSet) + ( ( fireOn = ExpressionAccumulationFire() - { accexp.setFireOn(fireOn); } + { accexp.setRecordSet(fireOn); } ) - )? + )? ret = ExpressionTemporalUnary(prop, pathprop) { accexp.setOperand2(ret); ret = accexp; } // END ACCUMULATION @@ -1231,20 +1231,21 @@ Expression ExpressionTemporalUnary(boolean prop, boolean pathprop) : | ret = ExpressionITE(prop, pathprop) | - ret = ExpressionAccumulationNullary(prop, pathprop) + ret = ExpressionAccumulationUnary(prop, pathprop) ) { return ret; } } /* START Accumulation Specification */ -ExpressionAccumulation ExpressionAccumulationNullary(boolean prop, boolean pathprop) : +ExpressionAccumulation ExpressionAccumulationUnary(boolean prop, boolean pathprop) : { ExpressionAccumulation ret; AccumulationConstraint constr; TemporalOperatorBound bound; Expression reg; ArrayList fireOn; + Expression tmp; } { // Accumulation symbol @@ -1255,26 +1256,30 @@ ExpressionAccumulation ExpressionAccumulationNullary(boolean prop, boolean pathp | ( { ret = new ExpressionAccumulation(AccumulationSymbol.ACCBOXMINUS); } ) ) // Regular expression, should be star-free - + ( ( reg = ExpressionRegularUnary(prop, false) { ret.setRegularExpression((ExpressionRegular)reg); } ) | ( bound = BoundExpression() { ret.setBoundExpression(bound); } ) ) - + // Weight constraint - + ( constr = ExpressionAccumulationConstraint() { ret.setConstraint(constr); } ) - - // Fire set (= !StutterSet) - ( + + // Record set (= !StutterSet) + ( ( fireOn = ExpressionAccumulationFire() - { ret.setFireOn(fireOn); } + { ret.setRecordSet(fireOn); } ) - )? + )? + ( + tmp = ExpressionTemporalUnary(prop, pathprop) + { ret.setOperand2(tmp); } + )? { return ret; } } diff --git a/prism/src/parser/ast/ExpressionAccumulation.java b/prism/src/parser/ast/ExpressionAccumulation.java index 0163cf90..521cc536 100644 --- a/prism/src/parser/ast/ExpressionAccumulation.java +++ b/prism/src/parser/ast/ExpressionAccumulation.java @@ -134,7 +134,7 @@ public class ExpressionAccumulation extends Expression } public boolean isNullary() { - return symbol.isDia() || symbol.isBox(); + return (symbol.isDia() || symbol.isBox()) && operand2 == null; } // Add a toString