accumulation: documentation and refactoring

prism/src/explicit/AccumulationProduct.java

@@ -24,15 +24,15 @@ import common.Dottable;
 
 public abstract class AccumulationProduct<M extends Model,Component> extends ProductWithProductStates<M> implements Dottable
 {
-	final StoragePool<AccumulationTracker<Component>> trackers;
-	final StoragePool<AccumulationState<Component>> accStates;
+	protected final StoragePool<AccumulationTracker<Component>> trackers;
+	protected final StoragePool<AccumulationState<Component>> accStates;
 	
-	final BitSet goodStates;
+	protected final BitSet goodStates;
 
-	final ArrayList<BitSet> labels;
+	protected final ArrayList<BitSet> 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<M extends Model,Component> extends Pro
 		labels = new ArrayList<BitSet>();
 	}
 	
-	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<Component> track, final ExpressionAccumulation accexp, final ProbModelChecker mc)
 			throws PrismException;
 	
-	protected boolean isGoodTrack(final AccumulationTrack<Component> 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<Component> 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<M extends Model,Component> extends Pro
 		return isGood;
 	}
 	
-	protected boolean isGoodAccState(final AccumulationState<Component> 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<Component> state)
 			throws PrismException {
 		return state.hasGoodTrack();
 	}
 
+	/** Get the initial Component of the accumulation monitor.
+	 * @return
+	 */
 	protected abstract Component getInitialComponent();
 	
-	protected abstract AccumulationTrack<Component> updateTrack(Integer modelFromStateId, final AccumulationTrack<Component> 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<Component> track,
+			final ExpressionAccumulation accexp, final StateModelChecker mc);
 	
-	protected AccumulationState<Component> 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<Component> updateTrack(Integer modelFromStateId, final AccumulationTrack<Component> 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<Component>(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<Component> updateAccumulationState(final int modelFromStateId,
 			final AccumulationState<Component> 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<M extends Model,Component> 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<M extends Model,Component> extends Pro
 		BitSet initialGoodTracks = new BitSet();
 		
 		// Generate the initial track and product state
-		AccumulationTracker<Component> initialTracker = new AccumulationTracker<Component>(numberOfTracks, numberOfRewards, initialComponent);
+		AccumulationTracker<Component> initialTracker = new AccumulationTracker<Component>(numberOfTracks, numberOfWeights, initialComponent);
 		int initialTrackerId  = trackers.findOrAdd(initialTracker);
 		AccumulationState<Component> initialAccState = new AccumulationState<Component>(initialTrackerId, initialActiveTrack, numberOfTracks, initialGoodTracks);
 		int initialAccStateId = accStates.findOrAdd(initialAccState);

prism/src/explicit/AccumulationProductCounting.java

@@ -38,7 +38,7 @@ public class AccumulationProductCounting<M extends Model> 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<M extends Model> extends AccumulationPr
 			public void notify(ProductState state, Integer index)
 					throws PrismException {
 				AccumulationState<Integer> 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<M extends Model> 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<M extends Model> extends AccumulationPr
 			public void notify(final ProductState state, final Integer index)
 					throws PrismException {
 				AccumulationState<Integer> 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<M extends Model> extends AccumulationPr
 	}
 	
 	@Override
-	protected AccumulationTrack<Integer> updateTrack(Integer modelFromStateId, final AccumulationTrack<Integer> track,
-			final ExpressionAccumulation accexp, final double[] weights, final StateModelChecker mc) {
+	protected Integer updateComponent(Integer modelFromStateId, final AccumulationTrack<Integer> 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<Integer>(newweights, currentStep+1);
+		int nextStep = currentStep+1;
+		if(nextStep > maxStep) { return null; }
+		return nextStep;
 	}
 	
 	/**

prism/src/explicit/AccumulationProductRegular.java

@@ -28,7 +28,7 @@ import prism.PrismSettings;
 
 public class AccumulationProductRegular<M extends Model> extends AccumulationProduct<M,State>
 {
-	DeterministicFiniteAutomaton<String> automaton;
+	protected DeterministicFiniteAutomaton<String> automaton;
 	
 	public AccumulationProductRegular(M originalModel) {
 		super(originalModel);
@@ -45,7 +45,7 @@ public class AccumulationProductRegular<M extends Model> 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<M extends Model> extends AccumulationPro
 			public void notify(ProductState state, Integer index)
 					throws PrismException {
 				AccumulationState<State> 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<M extends Model> 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<M extends Model> extends AccumulationPro
 			public void notify(ProductState state, Integer index)
 					throws PrismException {
 				AccumulationState<State> 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<M extends Model> extends AccumulationPro
 	}
 	
 	@Override
-	protected AccumulationTrack<State> updateTrack(Integer modelFromStateId, AccumulationTrack<State> track, ExpressionAccumulation accexp, double[] weights, StateModelChecker mc) {
+	protected State updateComponent(Integer modelFromStateId, final AccumulationTrack<State> track,
+			final ExpressionAccumulation accexp, final StateModelChecker mc) {
 		State currentState = track.getComponent();
 		
 		// Build EdgeLabel from labels.
 		// labels is a BitSet with labels L0,...,Ln
-		
 		ArrayList<String> edgeSymbols = new ArrayList<>();
 		BitSet edgeValues = new BitSet();
 		
@@ -201,18 +201,8 @@ public class AccumulationProductRegular<M extends Model> extends AccumulationPro
 		EdgeLabel<String> 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<State>(newweights, nextState);
+		if(nextState == null) { return null; }
+		return nextState;
 	}
 	
 	/**