From eae5aa9de144c7c1132b94423d94dbd038d9048f Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Thu, 20 Dec 2018 15:30:09 +0100 Subject: [PATCH] clean up, stopwatches --- .../explicit/AccumulationProductComplex.java | 20 +++++------ .../AccumulationProductComplexCounting.java | 2 +- .../AccumulationProductComplexRegular.java | 2 +- .../explicit/AccumulationTransformation.java | 36 +++++++++++++++++-- prism/src/explicit/DTMCModelChecker.java | 2 +- prism/src/explicit/MDPModelChecker.java | 2 +- .../ReplaceAccumulationExpressionComplex.java | 11 +++--- 7 files changed, 53 insertions(+), 22 deletions(-) diff --git a/prism/src/explicit/AccumulationProductComplex.java b/prism/src/explicit/AccumulationProductComplex.java index 2dc3f587..df0acd35 100644 --- a/prism/src/explicit/AccumulationProductComplex.java +++ b/prism/src/explicit/AccumulationProductComplex.java @@ -68,20 +68,18 @@ public abstract class AccumulationProductComplex exte for(int trackIdx=0; trackIdx track = tracker.getTracks().get(trackIdx); - // Is this an initial - if (trackIdx==accState.lastRestartNr) { - initStates.get(trackIdx).set(index); - } + boolean isInitial = trackIdx==accState.lastRestartNr; + boolean isRunning = track != null; + boolean isGoal = isGoalTrack(track,accexp,mc); - // Is this a running track? - if (track != null) { - runStates.get(trackIdx).set(index); - } + // Is this an initial + initStates.get(trackIdx).set(index, isInitial); + // Is this a running track? (Initial tracks are NOT running) + runStates.get(trackIdx).set(index, isRunning && !isInitial); + // Is this a goal track? - if (isGoalTrack(track, accexp, mc)) { - goalStates.get(trackIdx).set(index); - } + goalStates.get(trackIdx).set(index, isGoal); } } diff --git a/prism/src/explicit/AccumulationProductComplexCounting.java b/prism/src/explicit/AccumulationProductComplexCounting.java index 0d7e4f5d..6486dcb4 100644 --- a/prism/src/explicit/AccumulationProductComplexCounting.java +++ b/prism/src/explicit/AccumulationProductComplexCounting.java @@ -207,7 +207,7 @@ public class AccumulationProductComplexCounting extends Accumul * @throws PrismException */ protected void createAuxData(final Model graph, final ExpressionAccumulation accexp, final Vector rewards, final ProbModelChecker mc) throws PrismException { - numberOfTracks = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger()+2; + numberOfTracks = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger()+1; numberOfWeights = rewards.size(); for(int i=0; i extends Accumula throw new PrismException("Cannot handle cyclic automata!"); } - numberOfTracks = automaton.getLongestPathLength()+1; + numberOfTracks = automaton.getLongestPathLength(); numberOfWeights= rewards.size(); for(int i=0; i implements ModelExpressionTransformation { +public class AccumulationTransformation implements ModelExpressionTransformation { final protected Expression originalExpression; final protected M originalModel; final protected BitSet statesOfInterest; @@ -66,10 +67,16 @@ public class AccumulationTransformation implements ModelExpress } protected void doTransformation() throws PrismException { + mc.getLog().println("Handling maximal state formulas..."); + transformedExpression = mc.handleMaximalStateFormulas(originalModel, originalExpression); + mc.getLog().println("Performing accumulation transformation..."); - // We work on a copy - transformedExpression = originalExpression.deepCopy(); + + // Is this whole thing an ExpressionAccumulation? + //if(transformedExpression.isAccumulationExpression()) { System.out.println("HEYOOOO!!! " + transformedExpression); } + // TODO: WHILE getFirstAccumulationExpression + // Get the first ExpressionAccumulation ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpression(); mc.getLog().println(" [AT] for " + accexp); @@ -116,7 +123,11 @@ public class AccumulationTransformation implements ModelExpress @SuppressWarnings("unchecked") protected void doTransformationComplex(ExpressionAccumulation accexp, Vector rewards) throws PrismException { + StopWatch clock = new StopWatch(mc.getLog()); + // Build the product + clock.start("accumulation product construction"); + if(accexp.hasRegularExpression()) { product = (AccumulationProductComplexRegular) AccumulationProductComplexRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest); } else if (accexp.hasBoundExpression()) { @@ -125,6 +136,8 @@ public class AccumulationTransformation implements ModelExpress throw new PrismException("Accumulation Expression has no valid monitor!"); } + clock.stop(product.getTransformedModel().getNumStates() + " states"); + mc.getLog().println(" [AT] finished product construction: " + product.getTransformedModel().getNumStates()); // Transform the model @@ -147,11 +160,16 @@ public class AccumulationTransformation implements ModelExpress goalLabels.add(goalLabel); } // Transform the expression + clock.start("transforming expresssion"); + mc.getLog().println(" [AT] replacing the formula..."); ReplaceAccumulationExpressionComplex replace = new ReplaceAccumulationExpressionComplex(accexp, initLabels, runLabels, goalLabels, product.getNumberOfTracks()-1); transformedExpression = (Expression)transformedExpression.accept(replace); mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" + " -> " + transformedExpression.toString()); + + clock.stop(); + if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) { product.exportToDotFile("DEBUG-product.dot"); } @@ -159,7 +177,11 @@ public class AccumulationTransformation implements ModelExpress @SuppressWarnings("unchecked") protected void doTransformationSimple(ExpressionAccumulation accexp, Vector rewards) throws PrismException { + StopWatch clock = new StopWatch(mc.getLog()); + // Build the product + clock.start("accumulation product construction"); + if(accexp.hasRegularExpression()) { //throw new PrismException("I don't know how to do regular things..."); product = (AccumulationProductSimpleRegular) AccumulationProductSimpleRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest); @@ -169,6 +191,8 @@ public class AccumulationTransformation implements ModelExpress throw new PrismException("Accumulation Expression has no valid monitor!"); } + clock.stop(product.getTransformedModel().getNumStates() + " states"); + mc.getLog().println(" [AT] finished product construction: " + product.getTransformedModel().getNumStates()); // Transform the model @@ -176,12 +200,18 @@ public class AccumulationTransformation implements ModelExpress BitSet goodStates = ((AccumulationProductSimple)product).getGoodStates(); String goodLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal", goodStates, product.getTransformedModel().getLabels()); + // Transform the expression + clock.start("transforming expresssion"); + mc.getLog().println(" [AT] replacing the formula..."); ReplaceAccumulationExpressionSimple replace = new ReplaceAccumulationExpressionSimple(accexp, goodLabel, product.getNumberOfTracks()-2); transformedExpression = (Expression)transformedExpression.accept(replace); mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" + " -> " + transformedExpression.toString()); + + clock.stop(); + if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) { product.exportToDotFile("DEBUG-product.dot"); } diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 29b495e2..d5ea11a5 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -83,7 +83,7 @@ public class DTMCModelChecker extends ProbModelChecker protected StateValues checkProbPathFormulaAccumulationExpression(Model model, Expression expr, BitSet statesOfInterest) throws PrismException { // Do a transformation and a projection - AccumulationTransformation accTrans = new AccumulationTransformation(this, (DTMC)model, expr, statesOfInterest); + AccumulationTransformation accTrans = new AccumulationTransformation(this, (DTMCExplicit)model, expr, statesOfInterest); StateValues transValues = this.checkProbPathFormula(accTrans.getTransformedModel(), accTrans.getTransformedExpression(), MinMax.blank(), accTrans.getTransformedStatesOfInterest()); //this.getLog().println("TransValues"); //transValues.print(this.getLog()); diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 8c130c76..cd7b4dde 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -93,7 +93,7 @@ public class MDPModelChecker extends ProbModelChecker protected StateValues checkProbPathFormulaAccumulationExpression(Model model, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException { // Do a transformation and a projection - AccumulationTransformation accTrans = new AccumulationTransformation(this, (MDP)model, expr, statesOfInterest); + AccumulationTransformation accTrans = new AccumulationTransformation(this, (MDPExplicit)model, expr, statesOfInterest); StateValues transValues = this.checkProbPathFormula(accTrans.getTransformedModel(), accTrans.getTransformedExpression(), minMax, accTrans.getTransformedStatesOfInterest()); StateValues projectedValues = accTrans.projectToOriginalModel(transValues); return projectedValues; diff --git a/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java b/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java index 9645bb02..d0caaedb 100644 --- a/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java +++ b/prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java @@ -40,19 +40,22 @@ public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify { Expression goal = new ExpressionLabel(goalLabels.get(i)); // if this is until: - // append first operand to run + // append first operand to init and run // append second operand to goal if(accexp.getOperand1() != null) { - run = new ExpressionBinaryOp(ExpressionBinaryOp.AND, run, accexp.getOperand1()); + run = new ExpressionBinaryOp(ExpressionBinaryOp.AND, run, accexp.getOperand1()); + init = new ExpressionBinaryOp(ExpressionBinaryOp.AND, init, accexp.getOperand1()); } if(accexp.getOperand2() != null) { goal = new ExpressionBinaryOp(ExpressionBinaryOp.AND, goal, accexp.getOperand2()); } // until: (run_i UNTIL goal_i) - ExpressionTemporal until = new ExpressionTemporal(ExpressionTemporal.P_U, run, goal); + ExpressionTemporal until = new ExpressionTemporal(ExpressionTemporal.P_U, run, goal); + // xuntil:(X until) + ExpressionTemporal xuntil = new ExpressionTemporal(ExpressionTemporal.P_X, null, Expression.Parenth(until)); // and: (init_i AND until) - ExpressionBinaryOp and = new ExpressionBinaryOp(ExpressionBinaryOp.AND, init, Expression.Parenth(until)); + ExpressionBinaryOp and = new ExpressionBinaryOp(ExpressionBinaryOp.AND, init, xuntil); clauses.add(and); if(i==0) {