diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index dbcc595e..b36e485e 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -30,6 +30,8 @@ public abstract class AccumulationProduct extends Pro protected final ArrayList labels; protected int numberOfTracks; + protected int accumulationLength; + protected int numberOfWeights; protected final ArrayList initStates; @@ -54,6 +56,10 @@ public abstract class AccumulationProduct extends Pro return numberOfTracks; } + public final int getAccumulationLength() { + return accumulationLength; + } + protected final boolean constraintHolds(final AccumulationTrack track) throws PrismException { return ctx.accexp.getConstraint().holds(ctx, track.getWeights()); } @@ -87,13 +93,16 @@ public abstract class AccumulationProduct extends Pro protected final AccumulationState updateAccumulationState(final int modelFromStateId, final AccumulationState accstate, final HashMap 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)) { - // We still need to return an "empty" accstate. + + if(ctx.singleTrack && (accstate.lastRestartNr == numberOfTracks)) { + // We still need to return an "empty" accstate AccumulationState newAccstate = this.accStates.getById(0); - newAccstate.lastRestartNr = numberOfTracks-1; + newAccstate.lastRestartNr = numberOfTracks; return newAccstate; + //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. diff --git a/prism/src/explicit/AccumulationProductCounting.java b/prism/src/explicit/AccumulationProductCounting.java index 320619f4..f1914353 100644 --- a/prism/src/explicit/AccumulationProductCounting.java +++ b/prism/src/explicit/AccumulationProductCounting.java @@ -180,7 +180,14 @@ public class AccumulationProductCounting extends AccumulationPr } protected void createAuxData(final Model graph) throws PrismException { - numberOfTracks = IntegerBound.fromTemporalOperatorBound(ctx.accexp.getBoundExpression(), ctx.mc.getConstantValues(), true).getHighestInteger()+1; + accumulationLength = IntegerBound.fromTemporalOperatorBound(ctx.accexp.getBoundExpression(), ctx.mc.getConstantValues(), true).getHighestInteger(); + + if(ctx.singleTrack) { + numberOfTracks = 1; + } else { + numberOfTracks = accumulationLength + 1; + } + numberOfWeights = ctx.rewards.size(); if(ctx.simpleMethod) { diff --git a/prism/src/explicit/AccumulationProductRegular.java b/prism/src/explicit/AccumulationProductRegular.java index 678e874e..2653a75d 100644 --- a/prism/src/explicit/AccumulationProductRegular.java +++ b/prism/src/explicit/AccumulationProductRegular.java @@ -224,8 +224,14 @@ public class AccumulationProductRegular extends AccumulationPro throw new PrismException("Cannot handle cyclic automata!"); } - numberOfTracks = automaton.getLongestPathLength()+1; - numberOfWeights= ctx.rewards.size(); + accumulationLength = automaton.getLongestPathLength(); + numberOfWeights = ctx.rewards.size(); + + if(ctx.singleTrack) { + numberOfTracks = 1; + } else { + numberOfTracks = accumulationLength + 1; + } if(ctx.simpleMethod) { goalStates.add(new BitSet()); diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index a7e172b4..3edaf9e8 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -165,6 +165,7 @@ public class AccumulationTransformation implements Mode if(ctx.simpleMethod) { BitSet goodStates = product.getGoalStates(0); + System.out.println(goodStates); String goodLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal", goodStates, product.getTransformedModel().getLabels()); goalLabels.add(goodLabel); @@ -189,12 +190,13 @@ 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, ctx.reachConstr); + replace = new ReplaceAccumulationExpressionSimple(ctx.accexp, goalLabels.get(0), product.getAccumulationLength(), product.getNumberOfTracks(), ctx.reachConstr); } else { - replace = new ReplaceAccumulationExpressionComplex(ctx.accexp, initLabels, runLabels, goalLabels, product.getNumberOfTracks()-1, ctx.singleTrack); + replace = new ReplaceAccumulationExpressionComplex(ctx.accexp, initLabels, runLabels, goalLabels, product.getAccumulationLength(), product.getNumberOfTracks()); } transformedExpression = (Expression)transformedExpression.accept(replace); clock.stop("got " + transformedExpression); + //clock.stop(); if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) { product.exportToDotFile("DEBUG-product.dot"); diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java b/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java index 9d2d0151..05cb1a5a 100644 --- a/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java +++ b/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java @@ -17,17 +17,16 @@ public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify { private ArrayList runLabels; private ArrayList goalLabels; private int accLength; + private int numberOfTracks; - private boolean singleTrack; - - public ReplaceAccumulationExpressionComplex(ExpressionAccumulation accexp, ArrayList initLabels, ArrayList runLabels, ArrayList goalLabels, int accLength, boolean singleTrack) { + public ReplaceAccumulationExpressionComplex(ExpressionAccumulation accexp, ArrayList initLabels, ArrayList runLabels, ArrayList goalLabels, int accLength, int numberOfTracks) { super(); this.accexp = accexp; this.initLabels = initLabels; this.runLabels = runLabels; this.goalLabels = goalLabels; this.accLength = accLength; - this.singleTrack = singleTrack; + this.numberOfTracks = numberOfTracks; } private Object replaceWithUntil(ExpressionAccumulation accexp) throws PrismLangException { @@ -37,10 +36,7 @@ public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify { ArrayList clauses = new ArrayList<>(); Expression result = null; - for(int i=0; i0) { break; } - + for(int i=0; i