From e965d0f99339c73aefc814dad96a3d135d3e77fd Mon Sep 17 00:00:00 2001 From: Sascha Wunderlich Date: Fri, 21 Dec 2018 15:26:05 +0100 Subject: [PATCH] accumulation: deduplicate the rest --- prism/src/explicit/AccumulationContext.java | 4 +- prism/src/explicit/AccumulationProduct.java | 71 +++++- .../explicit/AccumulationProductComplex.java | 139 ----------- ....java => AccumulationProductCounting.java} | 28 ++- ...r.java => AccumulationProductRegular.java} | 28 ++- .../explicit/AccumulationProductSimple.java | 107 -------- .../AccumulationProductSimpleCounting.java | 195 --------------- .../AccumulationProductSimpleRegular.java | 228 ------------------ .../explicit/AccumulationTransformation.java | 144 ++++------- 9 files changed, 155 insertions(+), 789 deletions(-) delete mode 100644 prism/src/explicit/AccumulationProductComplex.java rename prism/src/explicit/{AccumulationProductComplexCounting.java => AccumulationProductCounting.java} (81%) rename prism/src/explicit/{AccumulationProductComplexRegular.java => AccumulationProductRegular.java} (85%) delete mode 100644 prism/src/explicit/AccumulationProductSimple.java delete mode 100644 prism/src/explicit/AccumulationProductSimpleCounting.java delete mode 100644 prism/src/explicit/AccumulationProductSimpleRegular.java diff --git a/prism/src/explicit/AccumulationContext.java b/prism/src/explicit/AccumulationContext.java index a0c98109..5c2fc7fd 100644 --- a/prism/src/explicit/AccumulationContext.java +++ b/prism/src/explicit/AccumulationContext.java @@ -11,6 +11,7 @@ public class AccumulationContext { /** Information about the accumulation strategy */ public enum strategy {UNTIL, REACH}; + public boolean simpleMethod; public boolean singleTrack; /** The ingredients */ @@ -20,11 +21,10 @@ public class AccumulationContext { /** We also have a model checker */ public StateModelChecker mc; - public AccumulationContext(ExpressionAccumulation accexp, Vector rewards, StateModelChecker mc, boolean singleTrack) { + public AccumulationContext(ExpressionAccumulation accexp, Vector rewards, StateModelChecker mc) { this.accexp = accexp; this.rewards = rewards; this.mc = mc; - this.singleTrack = singleTrack; } // A mini reward wrapper. diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index fd93235f..ee8907c6 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -4,6 +4,7 @@ import java.util.ArrayList; import java.util.BitSet; import java.util.Iterator; import java.util.Map; + import parser.ast.AccumulationFactor; import parser.ast.Expression; import prism.IntegerBound; @@ -32,6 +33,10 @@ public abstract class AccumulationProduct extends Pro protected int numberOfTracks; protected int numberOfWeights; + + protected final ArrayList initStates; + protected final ArrayList runStates; + protected final ArrayList goalStates; public AccumulationProduct(M originalModel, AccumulationContext ctx) { super(originalModel); @@ -40,6 +45,10 @@ public abstract class AccumulationProduct extends Pro labels = new ArrayList(); + initStates = new ArrayList<>(); + runStates = new ArrayList<>(); + goalStates = new ArrayList<>(); + this.ctx = ctx; } @@ -179,8 +188,6 @@ public abstract class AccumulationProduct extends Pro } protected abstract boolean isFinalTrack(AccumulationTrack track) throws PrismException; - - protected abstract String labelString(Integer stateId); @Override public String toDot() { @@ -237,4 +244,64 @@ public abstract class AccumulationProduct extends Pro return result.toString(); } + + public final BitSet getInitStates(int track) { + return initStates.get(track); + } + + public final BitSet getRunStates(int track) { + return runStates.get(track); + } + + public final BitSet getGoalStates(int track) { + return goalStates.get(track); + } + + protected void generateTrackInfo(ProductState state, Integer index) throws PrismException { + AccumulationState accState = accStates.getById(state.getSecondState()); + + // If this is a simple Product, we only set the GoalState and return + if(ctx.simpleMethod) { + goalStates.get(0).set(index, accState.hasGoodTracks()); + return; + } + + AccumulationTracker tracker = accState.getTracker(trackers); + + for(int trackIdx=0; trackIdx track = tracker.getTracks().get(trackIdx); + + boolean isInitial = trackIdx==accState.lastRestartNr; + boolean isRunning = track != null; + boolean isGoal = accState.getGoodTracks().get(trackIdx); // isGoalTrack(track) + + // 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? + goalStates.get(trackIdx).set(index, isGoal); + } + } + + protected String labelString(Integer stateId) { + StringBuffer result = new StringBuffer(); + + for(int t=0; t accstate = accStates.getById(prod_states.get(stateId).getSecondState()); + if(accstate.getGoodTracks().get(t)){ result.append("+"); continue; } + } else { + if(goalStates.get(t).get(stateId)) { result.append("G"); continue; } + if(initStates.get(t).get(stateId)) { result.append("I"); continue; } + if(runStates.get(t).get(stateId)) { result.append("R"); continue; } + } + result.append("_"); + } + + return result.toString(); + } } diff --git a/prism/src/explicit/AccumulationProductComplex.java b/prism/src/explicit/AccumulationProductComplex.java deleted file mode 100644 index 6ab26450..00000000 --- a/prism/src/explicit/AccumulationProductComplex.java +++ /dev/null @@ -1,139 +0,0 @@ -package explicit; - -import java.util.ArrayList; -import java.util.BitSet; -import java.util.Iterator; -import java.util.Map; - -import prism.PrismException; - -import common.Dottable; - -/** - * An AccumulationProduct has ProductStates, where the first component is the - * stateId in the original model, and the second component is the index of an - * AccumulationTracker. - * - * @author Sascha Wunderlich - * - * @param - */ - -public abstract class AccumulationProductComplex extends AccumulationProduct implements Dottable -{ - protected final ArrayList initStates; - protected final ArrayList runStates; - protected final ArrayList goalStates; - - public AccumulationProductComplex(M originalModel, AccumulationContext ctx) { - super(originalModel, ctx); - initStates = new ArrayList<>(); - runStates = new ArrayList<>(); - goalStates = new ArrayList<>(); - } - - public final BitSet getInitStates(int track) { - return initStates.get(track); - } - - public final BitSet getRunStates(int track) { - return runStates.get(track); - } - - public final BitSet getGoalStates(int track) { - return goalStates.get(track); - } - - protected void generateTrackInfo(ProductState state, Integer index) throws PrismException { - AccumulationState accState = accStates.getById(state.getSecondState()); - AccumulationTracker tracker = accState.getTracker(trackers); - - for(int trackIdx=0; trackIdx track = tracker.getTracks().get(trackIdx); - - boolean isInitial = trackIdx==accState.lastRestartNr; - boolean isRunning = track != null; - boolean isGoal = accState.getGoodTracks().get(trackIdx); // isGoalTrack(track) - - // 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? - goalStates.get(trackIdx).set(index, isGoal); - } - } - - @Override - protected String labelString(Integer stateId) { - StringBuffer result = new StringBuffer(); - - for(int t=0; t accState = accStates.getById(fromState.getSecondState()); - AccumulationTracker tracker = accState.getTracker(trackers); - result.append("" - + i - + "[shape=box, color=black" - + " label= < " - + "" - + "" - + "" - + "" - + "" - + "" - + "" - + "" - + "" - + "
" + i + "=" + fromState + "
" + accState + "
" + labelString(i) + "
\"" + Dottable.quoteForDot(tracker.toString()) + "\"
>]\n"); - - switch(productModel.getModelType()) { - case DTMC: - DTMCExplicit castDTMC = (DTMCExplicit)productModel; - Iterator> dtmcIter = castDTMC.getTransitionsIterator(i); - while (dtmcIter.hasNext()) { - Map.Entry e = dtmcIter.next(); - result.append(i + " -> " + e.getKey() + " [ label=\""); - result.append(e.getValue() + "\" ];\n"); - } - break; - case MDP: - MDPExplicit castMDP = (MDPExplicit)productModel; - for(int c = 0; c < castMDP.getNumChoices(i); c++) { - Iterator> mdpIter = castMDP.getTransitionsIterator(i, c); - while (mdpIter.hasNext()) { - Map.Entry e = mdpIter.next(); - result.append(i + " -> " + e.getKey() + " [ label=\""); - result.append(c + "," + e.getValue() + "\" ];\n"); - } - } - break; - default: - break; - } - } - - result.append("}"); - - return result.toString(); - } -} diff --git a/prism/src/explicit/AccumulationProductComplexCounting.java b/prism/src/explicit/AccumulationProductCounting.java similarity index 81% rename from prism/src/explicit/AccumulationProductComplexCounting.java rename to prism/src/explicit/AccumulationProductCounting.java index b435893d..6a406b92 100644 --- a/prism/src/explicit/AccumulationProductComplexCounting.java +++ b/prism/src/explicit/AccumulationProductCounting.java @@ -16,27 +16,27 @@ import prism.PrismException; * @param */ -public class AccumulationProductComplexCounting extends AccumulationProductComplex +public class AccumulationProductCounting extends AccumulationProduct { - public AccumulationProductComplexCounting(M originalModel, AccumulationContext ctx) { + public AccumulationProductCounting(M originalModel, AccumulationContext ctx) { super(originalModel, ctx); } @SuppressWarnings("unchecked") - public static AccumulationProductComplexCounting generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductCounting generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { switch(graph.getModelType()) { case DTMC: - return (AccumulationProductComplexCounting)generate((DTMC) graph, ctx, statesOfInterest); + return (AccumulationProductCounting)generate((DTMC) graph, ctx, statesOfInterest); case MDP: - return (AccumulationProductComplexCounting)generate((MDP) graph, ctx, statesOfInterest); + return (AccumulationProductCounting)generate((MDP) graph, ctx, statesOfInterest); default: throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); } } - public static AccumulationProductComplexCounting generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { - final AccumulationProductComplexCounting result = new AccumulationProductComplexCounting(graph, ctx); + public static AccumulationProductCounting generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { + final AccumulationProductCounting result = new AccumulationProductCounting(graph, ctx); // Create auxiliary data result.createAuxData(graph); @@ -89,9 +89,9 @@ public class AccumulationProductComplexCounting extends Accumul return result; } - public static AccumulationProductComplexCounting generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductCounting generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { // This is basically the same thing as for DTMCs - final AccumulationProductComplexCounting result = new AccumulationProductComplexCounting(graph, ctx); + final AccumulationProductCounting result = new AccumulationProductCounting(graph, ctx); // Create auxiliary data result.createAuxData(graph); @@ -182,10 +182,14 @@ public class AccumulationProductComplexCounting extends Accumul numberOfTracks = IntegerBound.fromTemporalOperatorBound(ctx.accexp.getBoundExpression(), ctx.mc.getConstantValues(), true).getHighestInteger()+1; numberOfWeights = ctx.rewards.size(); - for(int i=0; i */ -public class AccumulationProductComplexRegular extends AccumulationProductComplex +public class AccumulationProductRegular extends AccumulationProduct { protected DeterministicFiniteAutomaton automaton; - public AccumulationProductComplexRegular(M originalModel, AccumulationContext ctx) { + public AccumulationProductRegular(M originalModel, AccumulationContext ctx) { super(originalModel, ctx); } @SuppressWarnings("unchecked") - public static AccumulationProductComplexRegular generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductRegular generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { switch(graph.getModelType()) { case DTMC: - return (AccumulationProductComplexRegular)generate((DTMC) graph, ctx, statesOfInterest); + return (AccumulationProductRegular)generate((DTMC) graph, ctx, statesOfInterest); case MDP: - return (AccumulationProductComplexRegular)generate((MDP) graph, ctx, statesOfInterest); + return (AccumulationProductRegular)generate((MDP) graph, ctx, statesOfInterest); default: throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); } } - public static AccumulationProductComplexRegular generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { - final AccumulationProductComplexRegular result = new AccumulationProductComplexRegular(graph, ctx); + public static AccumulationProductRegular generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { + final AccumulationProductRegular result = new AccumulationProductRegular(graph, ctx); // Create auxiliary data result.createAuxData(graph); @@ -97,9 +97,9 @@ public class AccumulationProductComplexRegular extends Accumula return result; } - public static AccumulationProductComplexRegular generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { + public static AccumulationProductRegular generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { // This is basically the same thing as for DTMCs - final AccumulationProductComplexRegular result = new AccumulationProductComplexRegular(graph, ctx); + final AccumulationProductRegular result = new AccumulationProductRegular(graph, ctx); // Create auxiliary data result.createAuxData(graph); @@ -226,10 +226,14 @@ public class AccumulationProductComplexRegular extends Accumula numberOfTracks = automaton.getLongestPathLength()+1; numberOfWeights= ctx.rewards.size(); - for(int i=0; i - */ - -public abstract class AccumulationProductSimple extends AccumulationProduct implements Dottable -{ - protected final BitSet goodStates; - - public AccumulationProductSimple(M originalModel, AccumulationContext ctx) { - super(originalModel, ctx); - goodStates = new BitSet(); - } - - public final BitSet getGoodStates() { - return goodStates; - } - - protected void generateStateInfo(ProductState state, Integer index) throws PrismException { - AccumulationState accState = accStates.getById(state.getSecondState()); - goodStates.set(index, accState.hasGoodTracks()); - } - - protected String labelString(Integer stateId) { - StringBuffer result = new StringBuffer(); - if(goodStates.get(stateId)) { result.append("G: "); } - - for(int t=0; t accState = accStates.getById(fromState.getSecondState()); - AccumulationTracker tracker = accState.getTracker(trackers); - result.append("" - + i - + "[shape=box, color=black" - + " label= < " - + "" - + "" - + "" - + "" - + "" - + "" - + "" - + "" - + "" - + "
" + i + "=" + fromState + "
" + accState + "
" + labelString(i) + "
\"" + Dottable.quoteForDot(tracker.toString()) + "\"
>]\n"); - - switch(productModel.getModelType()) { - case DTMC: - DTMCExplicit castDTMC = (DTMCExplicit)productModel; - Iterator> dtmcIter = castDTMC.getTransitionsIterator(i); - while (dtmcIter.hasNext()) { - Map.Entry e = dtmcIter.next(); - result.append(i + " -> " + e.getKey() + " [ label=\""); - result.append(e.getValue() + "\" ];\n"); - } - break; - case MDP: - MDPExplicit castMDP = (MDPExplicit)productModel; - for(int c = 0; c < castMDP.getNumChoices(i); c++) { - Iterator> mdpIter = castMDP.getTransitionsIterator(i, c); - while (mdpIter.hasNext()) { - Map.Entry e = mdpIter.next(); - result.append(i + " -> " + e.getKey() + " [ label=\""); - result.append(c + "," + e.getValue() + "\" ];\n"); - } - } - break; - default: - break; - } - } - - result.append("}"); - - return result.toString(); - } -} diff --git a/prism/src/explicit/AccumulationProductSimpleCounting.java b/prism/src/explicit/AccumulationProductSimpleCounting.java deleted file mode 100644 index ad44f2ea..00000000 --- a/prism/src/explicit/AccumulationProductSimpleCounting.java +++ /dev/null @@ -1,195 +0,0 @@ -package explicit; - -import java.util.BitSet; - -import explicit.rewards.Rewards; -import prism.IntegerBound; -import prism.PrismException; - -/** - * An AccumulationProduct has ProductStates, where the first component is the - * stateId in the original model, and the second component is the index of an - * AccumulationTracker. - * - * @author Sascha Wunderlich - * - * @param - */ - -public class AccumulationProductSimpleCounting extends AccumulationProductSimple -{ - - public AccumulationProductSimpleCounting(M originalModel, AccumulationContext ctx) { - super(originalModel, ctx); - } - - @SuppressWarnings("unchecked") - public static AccumulationProductSimpleCounting generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { - switch(graph.getModelType()) { - case DTMC: - return (AccumulationProductSimpleCounting)generate((DTMC) graph, ctx, statesOfInterest); - case MDP: - return (AccumulationProductSimpleCounting)generate((MDP) graph, ctx, statesOfInterest); - default: - throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); - } - } - - public static AccumulationProductSimpleCounting generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { - final AccumulationProductSimpleCounting result = new AccumulationProductSimpleCounting(graph,ctx); - // Create auxiliary data - result.createAuxData(graph); - - // Build an operator - class AccumulationDTMCProductOperator implements DTMCProductOperator - { - @Override - public ProductState getInitialState(Integer dtmc_state) - throws PrismException { - int initialAccStateId = result.createInitialStateId(); - return new ProductState(dtmc_state, initialAccStateId); - } - - @Override - public ProductState getSuccessor(ProductState from_state, Integer dtmc_to_state) throws PrismException { - // Get the current accumulation state - AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); - - // Get step weights - double[] weights = ctx.getWeights(from_state.getFirstState()); - - // Update accumulation product state, store it and get its ID. - AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, weights); - int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); - - return new ProductState(dtmc_to_state, to_accproduct_id); - } - - @Override - public void notify(ProductState state, Integer index) - throws PrismException { - result.generateStateInfo(state, index); - } - - @Override - public void finish() throws PrismException { - // Do nothing - } - - @Override - public DTMC getGraph() { - return graph; - } - } - - // Apply the operator - AccumulationDTMCProductOperator op = new AccumulationDTMCProductOperator(); - ProductWithProductStates.generate(op, result, statesOfInterest); - - return result; - } - - public static AccumulationProductSimpleCounting generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { - // This is basically the same thing as for DTMCs - final AccumulationProductSimpleCounting result = new AccumulationProductSimpleCounting(graph, ctx); - - // Create auxiliary data - result.createAuxData(graph); - - class AccumulationMDPProductOperator implements MDPProductOperator - { - - @Override - public ProductState getInitialState(final Integer MDP_state) - throws PrismException { - int initialAccStateId = result.createInitialStateId(); - return new ProductState(MDP_state, initialAccStateId); - } - - @Override - public ProductState getSuccessor(final ProductState from_state, final int choice_i, final Integer mdp_to_state) throws PrismException { - // Get the current accumulation state - AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); - - // Get step weights - // THIS IS DIFFERENT FROM ABOVE! - double[] weights = ctx.getWeights(from_state.getFirstState(), choice_i); - - // Update accumulation product state, store it and get its ID. - AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, weights); - int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); - return new ProductState(mdp_to_state, to_accproduct_id); - } - - @Override - public void notify(final ProductState state, final Integer index) - throws PrismException { - result.generateStateInfo(state, index); - } - - @Override - public void finish() throws PrismException { - // Do nothing - //mc.getLog().println("."); - } - - @Override - public MDP getGraph() { - return graph; - } - } - - AccumulationMDPProductOperator op = new AccumulationMDPProductOperator(); - ProductWithProductStates.generate(op, result, statesOfInterest); - return result; - } - - @Override - protected boolean isFinalTrack(final AccumulationTrack track) throws PrismException { - boolean isFinal = false; - if ( track != null ) { - Integer step = track.getComponent(); - if ( step > 0 ) { // if the step is 0, we cannot have a goal state. - IntegerBound stepBound = IntegerBound.fromTemporalOperatorBound(ctx.accexp.getBoundExpression(), ctx.mc.getConstantValues(), true); - isFinal = stepBound.isInBounds(step); - } - } - return isFinal; - } - - @Override - protected Integer getInitialComponent() { - return 0; - } - - @Override - protected Integer updateComponent(Integer modelFromStateId, final AccumulationTrack track) { - int currentStep = track.getComponent(); - - int maxStep = 0; - try { - maxStep = IntegerBound.fromTemporalOperatorBound(ctx.accexp.getBoundExpression(), ctx.mc.getConstantValues(), true).getHighestInteger(); - } catch(PrismException e) { - throw new RuntimeException("..."); - } - - int nextStep = currentStep+1; - if(nextStep > maxStep) { return null; } - return nextStep; - } - - /** - * Populates fields: - * - numberOfTracks with the highest relevant integer plus one, and - * - numberOfWeights with the size of the reward vector. - * @param graph - * @param accexp - * @param rewards - * @param mc - * @throws PrismException - */ - protected void createAuxData(final Model graph) throws PrismException { - numberOfTracks = IntegerBound.fromTemporalOperatorBound(ctx.accexp.getBoundExpression(), ctx.mc.getConstantValues(), true).getHighestInteger()+1; - numberOfWeights = ctx.rewards.size(); - } -} diff --git a/prism/src/explicit/AccumulationProductSimpleRegular.java b/prism/src/explicit/AccumulationProductSimpleRegular.java deleted file mode 100644 index c0247c24..00000000 --- a/prism/src/explicit/AccumulationProductSimpleRegular.java +++ /dev/null @@ -1,228 +0,0 @@ -package explicit; - -import java.util.ArrayList; -import java.util.BitSet; - -import automata.finite.DeterministicFiniteAutomaton; -import automata.finite.EdgeLabel; -import automata.finite.NondeterministicFiniteAutomaton; -import automata.finite.State; -import explicit.rewards.Rewards; -import parser.ast.ExpressionRegular; -import prism.PrismException; -import prism.PrismSettings; - -/** - * An AccumulationProduct has ProductStates, where the first component is the - * stateId in the original model, and the second component is the index of an - * AccumulationTracker. - * - * @author Sascha Wunderlich - * - * @param - */ - -public class AccumulationProductSimpleRegular extends AccumulationProductSimple -{ - protected DeterministicFiniteAutomaton automaton; - - public AccumulationProductSimpleRegular(M originalModel, AccumulationContext ctx) { - super(originalModel, ctx); - } - - @SuppressWarnings("unchecked") - public static AccumulationProductSimpleRegular generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { - switch(graph.getModelType()) { - case DTMC: - return (AccumulationProductSimpleRegular)generate((DTMC) graph, ctx, statesOfInterest); - case MDP: - return (AccumulationProductSimpleRegular)generate((MDP) graph, ctx, statesOfInterest); - default: - throw new PrismException("Can't handle accumulation product for " + graph.getModelType()); - } - } - - public static AccumulationProductSimpleRegular generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { - final AccumulationProductSimpleRegular result = new AccumulationProductSimpleRegular(graph, ctx); - // Create auxiliary data - result.createAuxData(graph); - - // Build an operator - class AccumulationDTMCProductOperator implements DTMCProductOperator - { - @Override - public ProductState getInitialState(Integer dtmc_state) - throws PrismException { - int initialAccStateId = result.createInitialStateId(); - return new ProductState(dtmc_state, initialAccStateId); - } - - @Override - public ProductState getSuccessor(ProductState from_state, - Integer dtmc_to_state) throws PrismException { - // Get the current accumulation state - AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); - - // Get step weights - double[] weights = ctx.getWeights(from_state.getFirstState()); - - // Update accumulation product state, store it and get its ID. - AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, weights); - int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); - - return new ProductState(dtmc_to_state, to_accproduct_id); - } - - @Override - public void notify(ProductState state, Integer index) - throws PrismException { - result.generateStateInfo(state, index); - } - - @Override - public void finish() throws PrismException { - // Do nothing - } - - @Override - public DTMC getGraph() { - return graph; - } - } - - // Apply the operator - AccumulationDTMCProductOperator op = new AccumulationDTMCProductOperator(); - ProductWithProductStates.generate(op, result, statesOfInterest); - - return result; - } - - public static AccumulationProductSimpleRegular generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException { - // This is basically the same thing as for DTMCs - final AccumulationProductSimpleRegular result = new AccumulationProductSimpleRegular(graph, ctx); - - // Create auxiliary data - result.createAuxData(graph); - - class AccumulationMDPProductOperator implements MDPProductOperator - { - - @Override - public ProductState getInitialState(final Integer MDP_state) - throws PrismException { - int initialAccStateId = result.createInitialStateId(); - return new ProductState(MDP_state, initialAccStateId); - } - - @Override - public ProductState getSuccessor(final ProductState from_state, - final int choice_i, final Integer mdp_to_state) throws PrismException { - // Get the current accumulation state - AccumulationState from_accstate = result.accStates.getById(from_state.getSecondState()); - - // Get step weights - double[] weights = ctx.getWeights(from_state.getFirstState(), choice_i); - - // Update accumulation product state, store it and get its ID. - AccumulationState to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, weights); - int to_accproduct_id = result.accStates.findOrAdd(to_accproduct); - return new ProductState(mdp_to_state, to_accproduct_id); - } - - @Override - public void notify(final ProductState state, final Integer index) - throws PrismException { - result.generateStateInfo(state, index); - } - - @Override - public void finish() throws PrismException { - // Do nothing - //mc.getLog().println("."); - } - - @Override - public MDP getGraph() { - return graph; - } - } - - AccumulationMDPProductOperator op = new AccumulationMDPProductOperator(); - ProductWithProductStates.generate(op, result, statesOfInterest); - return result; - } - - @Override - protected boolean isFinalTrack(AccumulationTrack track) throws PrismException { - boolean isFinal = false; - if ( track != null ) { - isFinal = automaton.isAcceptingState(track.getComponent()); - } - - return isFinal; - } - - @Override - protected State getInitialComponent() { - return automaton.getInitialState(); - } - - @Override - protected State updateComponent(Integer modelFromStateId, final AccumulationTrack track) { - State currentState = track.getComponent(); - - // Build EdgeLabel from labels. - // labels is a BitSet with labels L0,...,Ln - ArrayList edgeSymbols = new ArrayList<>(); - BitSet edgeValues = new BitSet(); - - for (int i=0; i < labels.size(); i++) { - // Each bitLabel contains one L - edgeSymbols.add(i, "L"+i); - if(labels.get(i).get(modelFromStateId)) { - edgeValues.set(i); - } - } - - EdgeLabel edgeLabel = new EdgeLabel<>(edgeSymbols, edgeValues); - - State nextState = automaton.getSuccessor(currentState,edgeLabel); - if(nextState == null) { return null; } - return nextState; - } - - /** - * Populates fields: - * - numberOfTracks with the highest relevant integer plus one, and - * - numberOfWeights with the size of the reward vector. - * @param graph - * @param accexp - * @param rewards - * @param mc - * @throws PrismException - */ - protected void createAuxData(final Model graph) throws PrismException { - // Build labels and DFA - AccumulationModelChecker accMc = new AccumulationModelChecker(); - ExpressionRegular reg = (ExpressionRegular)accMc.checkMaximalStateFormulas((ProbModelChecker) ctx.mc, graph, ctx.accexp.getRegularExpression(), labels); - - // Create and store the actual DFA - NondeterministicFiniteAutomaton nfa = NondeterministicFiniteAutomaton.fromExpressionRegular(reg); - //System.out.println(nfa.toDot()); - - automaton = nfa.determinize(); - automaton.trim(); // This should remove cycles. - - if(ctx.mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) { - nfa.exportToDotFile("DEBUG-automaton-nfa.dot"); - automaton.exportToDotFile("DEBUG-automaton-dfa.dot"); - } - - if (!automaton.isAcyclic()) { - throw new PrismException("Cannot handle cyclic automata!"); - } - - numberOfTracks = automaton.getLongestPathLength()+1; - numberOfWeights= ctx.rewards.size(); - } -} diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java index 7de6c96d..24738ba9 100644 --- a/prism/src/explicit/AccumulationTransformation.java +++ b/prism/src/explicit/AccumulationTransformation.java @@ -13,6 +13,7 @@ import parser.ast.ExpressionReward; import parser.ast.RewardStruct; import parser.visitor.ReplaceAccumulationExpressionComplex; import parser.visitor.ReplaceAccumulationExpressionSimple; +import parser.visitor.ASTVisitor; import parser.visitor.ReplaceAccumulationBox; import prism.PrismException; import prism.PrismSettings; @@ -26,6 +27,10 @@ public class AccumulationTransformation implements Mode protected Expression transformedExpression; protected AccumulationProduct product; + ArrayList initLabels; + ArrayList runLabels; + ArrayList goalLabels; + public AccumulationTransformation( StateModelChecker mc, M originalModel, Expression expr, @@ -35,6 +40,11 @@ public class AccumulationTransformation implements Mode this.originalModel = originalModel; this.mc = mc; this.statesOfInterest = statesOfInterest; + + this.initLabels = new ArrayList<>(); + this.runLabels = new ArrayList<>(); + this.goalLabels = new ArrayList<>(); + doTransformation(); } @@ -67,12 +77,14 @@ public class AccumulationTransformation implements Mode } protected void doTransformation() throws PrismException { + StopWatch clock = new StopWatch(mc.getLog()); + mc.getLog().println("Handling maximal state formulas..."); - transformedExpression = mc.handleMaximalStateFormulas(originalModel, originalExpression); - - mc.getLog().println("Performing accumulation transformation..."); + transformedExpression = mc.handleMaximalStateFormulas(originalModel, originalExpression); // Get the first ExpressionAccumulation + mc.getLog().println("Looking for an accumulation formula..."); + boolean singleTrack = true; ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpressionWithoutTemporal(); if(accexp == null || mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_MULTI)) { @@ -80,15 +92,14 @@ public class AccumulationTransformation implements Mode accexp = transformedExpression.getFirstAccumulationExpression(); } - mc.getLog().println(" [AT] for " + accexp); - mc.getLog().println(" ... single track? " + singleTrack); + mc.getLog().println("... found " + accexp); // Rewrite it, if it is a BOX if (accexp.getSymbol().isBox()) { ReplaceAccumulationBox replace = new ReplaceAccumulationBox(accexp); transformedExpression = (Expression)transformedExpression.accept(replace); accexp = transformedExpression.getFirstAccumulationExpression(); - mc.getLog().println(" ... after unboxing: " + accexp + " (in " + transformedExpression + ")"); + mc.getLog().println("... after unboxing: " + accexp + " (in " + transformedExpression + ")"); } // Get the rewards @@ -106,7 +117,7 @@ public class AccumulationTransformation implements Mode } // Figure out if we need a complex or a simple trafo... - boolean isComplex = accexp.hasFireOn() || !accexp.isNullary(); + boolean isSimple = !accexp.hasFireOn() && accexp.isNullary(); boolean isPast = accexp.getSymbol().isMinus(); boolean forceComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX); @@ -115,110 +126,59 @@ public class AccumulationTransformation implements Mode } // Build the AccumulationContext - AccumulationContext ctx = new AccumulationContext(accexp, rewards, mc, singleTrack); - - if(isComplex || forceComplex) { - mc.getLog().println(" ... using complex!"); - doTransformationComplex(ctx); - } else { - mc.getLog().println(" ... using simple!"); - doTransformationSimple(ctx); - } - } - - @SuppressWarnings("unchecked") - protected void doTransformationComplex(AccumulationContext ctx) throws PrismException { - StopWatch clock = new StopWatch(mc.getLog()); + AccumulationContext ctx = new AccumulationContext(accexp, rewards, mc); + ctx.singleTrack = singleTrack; + ctx.simpleMethod = isSimple && !forceComplex; // Build the product clock.start("accumulation product construction"); - if(ctx.accexp.hasRegularExpression()) { - product = (AccumulationProductComplexRegular) AccumulationProductComplexRegular.generate(originalModel, ctx, statesOfInterest); + product = AccumulationProductRegular.generate(originalModel, ctx, statesOfInterest); } else if (ctx.accexp.hasBoundExpression()) { - product = (AccumulationProductComplexCounting) AccumulationProductComplexCounting.generate(originalModel, ctx, statesOfInterest); + product = AccumulationProductCounting.generate(originalModel, ctx, statesOfInterest); } else { 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 - mc.getLog().println(" [AT] getting the init/run/goal states: "); - - ArrayList initLabels = new ArrayList(); - ArrayList runLabels = new ArrayList(); - ArrayList goalLabels = new ArrayList(); - - for(int track=0; track < product.getNumberOfTracks(); track++) { - BitSet initStates = ((AccumulationProductComplex)product).getInitStates(track); - BitSet runStates = ((AccumulationProductComplex)product).getRunStates(track); - BitSet goalStates = ((AccumulationProductComplex)product).getGoalStates(track); - - String initLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("init" + track, initStates, product.getTransformedModel().getLabels()); - initLabels.add(initLabel); - String runLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("run" + track, runStates, product.getTransformedModel().getLabels()); - runLabels.add(runLabel); - String goalLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal" + track, goalStates, product.getTransformedModel().getLabels()); - goalLabels.add(goalLabel); - } - // Transform the expression - clock.start("transforming expresssion"); - - mc.getLog().println(" [AT] replacing the formula..."); - ReplaceAccumulationExpressionComplex replace = new ReplaceAccumulationExpressionComplex(ctx.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"); - } - } - - @SuppressWarnings("unchecked") - protected void doTransformationSimple(AccumulationContext ctx) throws PrismException { - StopWatch clock = new StopWatch(mc.getLog()); + // Attach labels + clock.start("attaching labels"); - // Build the product - clock.start("accumulation product construction"); - - if(ctx.accexp.hasRegularExpression()) { - //throw new PrismException("I don't know how to do regular things..."); - product = (AccumulationProductSimpleRegular) AccumulationProductSimpleRegular.generate(originalModel, ctx, statesOfInterest); - } else if (ctx.accexp.hasBoundExpression()) { - product = (AccumulationProductSimpleCounting) AccumulationProductSimpleCounting.generate(originalModel, ctx, statesOfInterest); + if(ctx.simpleMethod) { + BitSet goodStates = product.getGoalStates(0); + String goodLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal", goodStates, product.getTransformedModel().getLabels()); + + goalLabels.add(goodLabel); } else { - throw new PrismException("Accumulation Expression has no valid monitor!"); + for(int track=0; track < product.getNumberOfTracks(); track++) { + BitSet initStates = product.getInitStates(track); + BitSet runStates = product.getRunStates(track); + BitSet goalStates = product.getGoalStates(track); + + String initLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("init" + track, initStates, product.getTransformedModel().getLabels()); + initLabels.add(initLabel); + String runLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("run" + track, runStates, product.getTransformedModel().getLabels()); + runLabels.add(runLabel); + String goalLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal" + track, goalStates, product.getTransformedModel().getLabels()); + goalLabels.add(goalLabel); + } } - clock.stop(product.getTransformedModel().getNumStates() + " states"); - - mc.getLog().println(" [AT] finished product construction: " + product.getTransformedModel().getNumStates()); - - // Transform the model - mc.getLog().println(" [AT] getting the good states: "); - - BitSet goodStates = ((AccumulationProductSimple)product).getGoodStates(); - String goodLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal", goodStates, product.getTransformedModel().getLabels()); + clock.stop(initLabels.size() + "/" + runLabels.size() + "/" + goalLabels.size() + " labels"); // Transform the expression - clock.start("transforming expresssion"); - - mc.getLog().println(" [AT] replacing the formula..."); - ReplaceAccumulationExpressionSimple replace = new ReplaceAccumulationExpressionSimple(ctx.accexp, goodLabel, product.getNumberOfTracks()-1); + clock.start("replacing formula"); + ASTVisitor replace; + if(ctx.simpleMethod) { + replace = new ReplaceAccumulationExpressionSimple(ctx.accexp, goalLabels.get(0), product.getNumberOfTracks()-1); + } else { + replace = new ReplaceAccumulationExpressionComplex(ctx.accexp, initLabels, runLabels, goalLabels, product.getNumberOfTracks()-1); + } transformedExpression = (Expression)transformedExpression.accept(replace); - mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" + - " -> " + transformedExpression.toString()); - - clock.stop(); + clock.stop("\n ->" + transformedExpression); if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) { - product.exportToDotFile("DEBUG-product.dot"); + product.exportToDotFile("DEBUG-product.dot"); } } } \ No newline at end of file