From 5b803247f3aad7a5f8e5528fe49ed41315d224e4 Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Wed, 20 Feb 2019 13:18:33 +0100 Subject: [PATCH] accumulation: support filtered simple method and until cascades --- prism/src/explicit/AccumulationContext.java | 1 + .../explicit/AccumulationTransformation.java | 8 +- .../ReplaceAccumulationExpressionSimple.java | 77 +++++++++++++++---- prism/src/prism/PrismSettings.java | 8 +- 4 files changed, 77 insertions(+), 17 deletions(-) diff --git a/prism/src/explicit/AccumulationContext.java b/prism/src/explicit/AccumulationContext.java index 5c2fc7fd..08045e4a 100644 --- a/prism/src/explicit/AccumulationContext.java +++ b/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; diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index 34dddb86..af84a7c9 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -125,10 +125,13 @@ 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.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 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 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); } diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java b/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java index 80402efd..45921dbb 100644 --- a/prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java +++ b/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 fireOn = accexp.getFireOn(); + + notfiltered = fireOn.get(0); + for(int i=1;i