diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java index 5842abd2..fcbca21e 100644 --- a/prism/src/explicit/AccumulationProduct.java +++ b/prism/src/explicit/AccumulationProduct.java @@ -24,15 +24,15 @@ import common.Dottable; public abstract class AccumulationProduct extends ProductWithProductStates implements Dottable { - final StoragePool> trackers; - final StoragePool> accStates; + protected final StoragePool> trackers; + protected final StoragePool> accStates; - final BitSet goodStates; + protected final BitSet goodStates; - final ArrayList labels; + protected final ArrayList labels; - int numberOfTracks; - int numberOfWeights; + protected int numberOfTracks; + protected int numberOfWeights; public AccumulationProduct(M originalModel) { super(originalModel); @@ -43,18 +43,34 @@ public abstract class AccumulationProduct extends Pro labels = new ArrayList(); } - public BitSet getGoodStates() { + public final BitSet getGoodStates() { return goodStates; } - public int getNumberOfTracks() { + public final int getNumberOfTracks() { return numberOfTracks; } + /** Checks whether a track is final according to the bound in the accumulation expression and the context in mc. + * @param track + * @param accexp + * @param mc + * @return + * @throws PrismException + */ protected abstract boolean isFinalTrack(final AccumulationTrack track, final ExpressionAccumulation accexp, final ProbModelChecker mc) throws PrismException; - protected boolean isGoodTrack(final AccumulationTrack track, final ExpressionAccumulation accexp, final ProbModelChecker mc) + /** Checks whether a track is good. + * + * Tracks are good, if they are final and fulfill the constraint in the accumulation expression with context mc. + * @param track + * @param accexp + * @param mc + * @return + * @throws PrismException + */ + protected final boolean isGoodTrack(final AccumulationTrack track, final ExpressionAccumulation accexp, final ProbModelChecker mc) throws PrismException { // Only final tracks can be good if (!isFinalTrack(track,accexp,mc)) { return false; } @@ -94,17 +110,71 @@ public abstract class AccumulationProduct extends Pro return isGood; } - protected boolean isGoodAccState(final AccumulationState state, final ExpressionAccumulation accexp, final ProbModelChecker mc) + /** Accumulation states are good if they contain at least one good track. + * @param state + * @return + * @throws PrismException + */ + protected final boolean isGoodAccState(final AccumulationState state) throws PrismException { return state.hasGoodTrack(); } + /** Get the initial Component of the accumulation monitor. + * @return + */ protected abstract Component getInitialComponent(); - protected abstract AccumulationTrack updateTrack(Integer modelFromStateId, final AccumulationTrack track, - final ExpressionAccumulation accexp, final double[] weights, final StateModelChecker mc); + /** Update the Component of the accumulation monitor when leaving modelFromStateId. + * @param modelFromStateId + * @param track + * @param accexp + * @param mc + * @return + */ + protected abstract Component updateComponent(Integer modelFromStateId, final AccumulationTrack track, + final ExpressionAccumulation accexp, final StateModelChecker mc); - protected AccumulationState updateAccumulationState(final int modelFromStateId, + /** Updates a single AccumulationTrack. Used in updateAccumulationState. + * + * Uses updateComponent to get the next Component, accumulates the current weights + * and makes a new track. + * @param modelFromStateId + * @param track + * @param accexp + * @param weights + * @param mc + * @return + */ + protected final AccumulationTrack updateTrack(Integer modelFromStateId, final AccumulationTrack track, + final ExpressionAccumulation accexp, final double[] weights, final StateModelChecker mc) { + Component nextComponent = updateComponent(modelFromStateId, track, accexp, mc); + + // If we are done, return null-Track + if (nextComponent == null) { return null; } + + // Otherwise, we update the weights and increase the step. + double[] newweights = new double[weights.length]; + for (int i = 0; i < weights.length; i++) { + newweights[i] = weights[i] + track.getWeights()[i]; + } + + return new AccumulationTrack(newweights, nextComponent); + } + + /** Generates a new accumulation state from an old one. + * + * To do so, it reads the necessary information from the model and its rewards + * and updates all tracks and their goodness accordingly. + * @param modelFromStateId + * @param accstate + * @param accexp + * @param weights + * @param mc + * @return + * @throws PrismException + */ + protected final AccumulationState updateAccumulationState(final int modelFromStateId, final AccumulationState accstate, final ExpressionAccumulation accexp, final double[] weights, final ProbModelChecker mc) throws PrismException { // Get the old tracker and tracks. @@ -161,7 +231,14 @@ public abstract class AccumulationProduct extends Pro return new AccumulationState<>(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks); } - protected int createInitialStateId(int numberOfRewards) { + /** + * Creates the initial state for the accumulation part of this of this accumulation product. Returns its ID. + * + * The initial state has a tracker filled with null-tracks, none of which is good + * where the first restart is the first (0th) track. + * @return + */ + protected final int createInitialStateId() { Component initialComponent = getInitialComponent(); // The initial active track is the first one, all tracks are non-good by default @@ -169,7 +246,7 @@ public abstract class AccumulationProduct extends Pro BitSet initialGoodTracks = new BitSet(); // Generate the initial track and product state - AccumulationTracker initialTracker = new AccumulationTracker(numberOfTracks, numberOfRewards, initialComponent); + AccumulationTracker initialTracker = new AccumulationTracker(numberOfTracks, numberOfWeights, initialComponent); int initialTrackerId = trackers.findOrAdd(initialTracker); AccumulationState initialAccState = new AccumulationState(initialTrackerId, initialActiveTrack, numberOfTracks, initialGoodTracks); int initialAccStateId = accStates.findOrAdd(initialAccState); diff --git a/prism/src/explicit/AccumulationProductCounting.java b/prism/src/explicit/AccumulationProductCounting.java index e9b4e91b..cd5f7b8c 100644 --- a/prism/src/explicit/AccumulationProductCounting.java +++ b/prism/src/explicit/AccumulationProductCounting.java @@ -38,7 +38,7 @@ public class AccumulationProductCounting extends AccumulationPr @Override public ProductState getInitialState(Integer dtmc_state) throws PrismException { - int initialAccStateId = result.createInitialStateId(rewards.size()); + int initialAccStateId = result.createInitialStateId(); return new ProductState(dtmc_state, initialAccStateId); } @@ -66,7 +66,7 @@ public class AccumulationProductCounting extends AccumulationPr public void notify(ProductState state, Integer index) throws PrismException { AccumulationState accState = result.accStates.getById(state.getSecondState()); - if (result.isGoodAccState(accState, accexp, mc)) { + if (result.isGoodAccState(accState)) { result.goodStates.set(index); } } @@ -102,7 +102,7 @@ public class AccumulationProductCounting extends AccumulationPr @Override public ProductState getInitialState(final Integer MDP_state) throws PrismException { - int initialAccStateId = result.createInitialStateId(rewards.size()); + int initialAccStateId = result.createInitialStateId(); return new ProductState(MDP_state, initialAccStateId); } @@ -132,7 +132,7 @@ public class AccumulationProductCounting extends AccumulationPr public void notify(final ProductState state, final Integer index) throws PrismException { AccumulationState accState = result.accStates.getById(state.getSecondState()); - if (result.isGoodAccState(accState, accexp, mc)) { + if (result.isGoodAccState(accState)) { result.goodStates.set(index); } } @@ -171,26 +171,20 @@ public class AccumulationProductCounting extends AccumulationPr } @Override - protected AccumulationTrack updateTrack(Integer modelFromStateId, final AccumulationTrack track, - final ExpressionAccumulation accexp, final double[] weights, final StateModelChecker mc) { + protected Integer updateComponent(Integer modelFromStateId, final AccumulationTrack track, + final ExpressionAccumulation accexp, final StateModelChecker mc) { int currentStep = track.getComponent(); + int maxStep = 0; try { maxStep = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger(); } catch(PrismException e) { throw new RuntimeException("..."); } - - // If we are done, return null-Track - if (currentStep >= maxStep) { return null; } - - // Otherwise, we update the weights and increase the step. - double[] newweights = new double[weights.length]; - for (int i = 0; i < weights.length; i++) { - newweights[i] = weights[i] + track.getWeights()[i]; - } - return new AccumulationTrack(newweights, currentStep+1); + int nextStep = currentStep+1; + if(nextStep > maxStep) { return null; } + return nextStep; } /** diff --git a/prism/src/explicit/AccumulationProductRegular.java b/prism/src/explicit/AccumulationProductRegular.java index d4488d02..41e1b10a 100644 --- a/prism/src/explicit/AccumulationProductRegular.java +++ b/prism/src/explicit/AccumulationProductRegular.java @@ -28,7 +28,7 @@ import prism.PrismSettings; public class AccumulationProductRegular extends AccumulationProduct { - DeterministicFiniteAutomaton automaton; + protected DeterministicFiniteAutomaton automaton; public AccumulationProductRegular(M originalModel) { super(originalModel); @@ -45,7 +45,7 @@ public class AccumulationProductRegular extends AccumulationPro @Override public ProductState getInitialState(Integer dtmc_state) throws PrismException { - int initialAccStateId = result.createInitialStateId(rewards.size()); + int initialAccStateId = result.createInitialStateId(); return new ProductState(dtmc_state, initialAccStateId); } @@ -73,7 +73,7 @@ public class AccumulationProductRegular extends AccumulationPro public void notify(ProductState state, Integer index) throws PrismException { AccumulationState accState = result.accStates.getById(state.getSecondState()); - if (result.isGoodAccState(accState, accexp, mc)) { + if (result.isGoodAccState(accState)) { result.goodStates.set(index); } } @@ -111,7 +111,7 @@ public class AccumulationProductRegular extends AccumulationPro @Override public ProductState getInitialState(Integer MDP_state) throws PrismException { - int initialAccStateId = result.createInitialStateId(rewards.size()); + int initialAccStateId = result.createInitialStateId(); return new ProductState(MDP_state, initialAccStateId); } @@ -143,7 +143,7 @@ public class AccumulationProductRegular extends AccumulationPro public void notify(ProductState state, Integer index) throws PrismException { AccumulationState accState = result.accStates.getById(state.getSecondState()); - if (result.isGoodAccState(accState, accexp, mc)) { + if (result.isGoodAccState(accState)) { result.goodStates.set(index); } } @@ -181,12 +181,12 @@ public class AccumulationProductRegular extends AccumulationPro } @Override - protected AccumulationTrack updateTrack(Integer modelFromStateId, AccumulationTrack track, ExpressionAccumulation accexp, double[] weights, StateModelChecker mc) { + protected State updateComponent(Integer modelFromStateId, final AccumulationTrack track, + final ExpressionAccumulation accexp, final StateModelChecker mc) { State currentState = track.getComponent(); // Build EdgeLabel from labels. // labels is a BitSet with labels L0,...,Ln - ArrayList edgeSymbols = new ArrayList<>(); BitSet edgeValues = new BitSet(); @@ -201,18 +201,8 @@ public class AccumulationProductRegular extends AccumulationPro EdgeLabel edgeLabel = new EdgeLabel<>(edgeSymbols, edgeValues); State nextState = automaton.getSuccessor(currentState,edgeLabel); - //System.out.println("Successor of " + currentState + " via " + edgeLabel + ":" + nextState); - - // Undefined behavior, return the null-Track - if (nextState == null) { return null; } - - // If we have defined behavior, update the weights and get the new stateId. - double[] newweights = new double[weights.length]; - for (int i = 0; i < weights.length; i++) { - newweights[i] = weights[i] + track.getWeights()[i]; - } - - return new AccumulationTrack(newweights, nextState); + if(nextState == null) { return null; } + return nextState; } /**