diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index 2e2ddfcf..1a0e36db 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -119,21 +119,25 @@ public abstract class AccumulationProduct extends Pro // For DIA operators, we just check the bound. // For BOX operators, we check the INVERTED bound. + + // TODO: THIS MAY BE BROKEN switch(accexp.getSymbol()) { case ACCBOXMINUS: case ACCBOXPLUS: if (!rhs.isInBounds(lhs)) { isGood = true; } + mc.getLog().println("WARNING: This may be wrong."); break; case ACCDIAMINUS: case ACCDIAPLUS: + case ACCUNTIL: if (rhs.isInBounds(lhs)) { isGood = true; } break; default: - throw new RuntimeException("Oh boy!"); + throw new RuntimeException("Accumulation symbol cannot be handled..."); } //if(isGood) {mc.getLog().print("+");} else {mc.getLog().print("-");} return isGood; diff --git a/prism/src/parser/PrismParser.jj b/prism/src/parser/PrismParser.jj index da36cabd..53a4c152 100644 --- a/prism/src/parser/PrismParser.jj +++ b/prism/src/parser/PrismParser.jj @@ -1152,10 +1152,18 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) : TemporalOperatorBound defaultBound = null; TemporalOperatorBounds bounds = null; Token begin = null; + + //Accumulation + ExpressionAccumulation accexp; + AccumulationConstraint constr; + TemporalOperatorBound bound; + Expression reg; + ArrayList fireOn; + } { { begin = getToken(1); } ret = ExpressionTemporalUnary(prop, pathprop) - [ + ( // This production is only allowed in expressions if the "pathprop" parameter is true { if (!pathprop) throw generateParseException(); } { exprTemp = new ExpressionTemporal(); exprTemp.setOperand1(ret); } @@ -1167,7 +1175,33 @@ Expression ExpressionTemporalBinary(boolean prop, boolean pathprop) : )? expr = ExpressionTemporalUnary(prop, pathprop) { exprTemp.setOperand2(expr); exprTemp.setPosition(begin, getToken(0)); ret = exprTemp; } - ] + | + // 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) + ( + ( + fireOn = ExpressionAccumulationFire() + { accexp.setFireOn(fireOn); } + ) + )? + ret = ExpressionTemporalUnary(prop, pathprop) + { accexp.setOperand2(ret); ret = accexp; } + )? { return ret; } } diff --git a/prism/src/parser/ast/ExpressionAccumulation.java b/prism/src/parser/ast/ExpressionAccumulation.java index f5ea1fd6..75d8f90b 100644 --- a/prism/src/parser/ast/ExpressionAccumulation.java +++ b/prism/src/parser/ast/ExpressionAccumulation.java @@ -27,6 +27,7 @@ package parser.ast; import java.util.ArrayList; +import java.util.stream.Collectors; import param.BigRational; import parser.EvaluateContext; @@ -125,7 +126,7 @@ public class ExpressionAccumulation extends Expression public String toString() { String ret = ""; - if(operand1 != null) { ret += operand1.toString(); } + if(operand1 != null) { ret += operand1.toString() + " "; } ret += symbol.toString(); @@ -135,9 +136,12 @@ public class ExpressionAccumulation extends Expression ret += "(" + constraint.toString() + ")"; - if ( hasFireOn() ) { ret += "(" + fireOn.toString() + ")"; } + if ( hasFireOn() ) { + String fireOnString = fireOn.stream().map(f -> f.toString()).collect(Collectors.joining(",")); + ret += "(" + fireOnString + ")"; + } - if(operand2 != null) { ret += operand2.toString(); } + if(operand2 != null) { ret += " " + operand2.toString(); } return ret; } diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpression.java b/prism/src/parser/visitor/ReplaceAccumulationExpression.java index bf9aad6b..b7b9259b 100644 --- a/prism/src/parser/visitor/ReplaceAccumulationExpression.java +++ b/prism/src/parser/visitor/ReplaceAccumulationExpression.java @@ -39,51 +39,47 @@ public class ReplaceAccumulationExpression extends ASTTraverseModify { if (sym.isMinus()) { throw(new PrismLangException("Accumulation with past is not supported.")); } + + // This expression is of the form OR{0..(l-1)}(init_i AND (run_i UNTIL goal_i)) - if (sym.isUntil()) { - throw(new PrismLangException("ACCUNTIL is not supported.")); - } else { - // This expression is of the form OR{0..(l-1)}(init_i AND (run_i UNTIL goal_i)) - - // Build all the subexpressions... - ArrayList clauses = new ArrayList<>(); - Expression result = null; + // Build all the subexpressions... + ArrayList clauses = new ArrayList<>(); + Expression result = null; + + for(int i=0; i