accumulation: support simple trafo

prism/src/explicit/AccumulationProduct.java

@@ -44,119 +44,26 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 		return numberOfTracks;
 	}
 	
-	protected abstract void generateTrackInfo(ProductState state, Integer index, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException;
-	
-
-   /** 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 isGoalTrack(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; }
-           boolean isGood = false;
-           
-           //TODO: these should be double later on
-           // Collect the weight linear combination, factor*weight+...     
-           int lhs = 0;
-           int factorNr = 0;
-           for (AccumulationFactor factor : accexp.getConstraint().getFactors()) {
-                   lhs += factor.getFactor().evaluateInt(mc.getConstantValues())
-                                   * track.getWeight(factorNr);
-           }
-
-           // Check the bound
-           IntegerBound rhs = IntegerBound.fromTemporalOperatorBound(accexp.getConstraint().getBound(), mc.getConstantValues(), true);
+	protected final boolean constraintHolds(final AccumulationTrack<Component> track, final ExpressionAccumulation accexp, final ProbModelChecker mc) throws PrismException {
+		// Collect the weight linear combination, factor*weight+...     
+        int lhs = 0;
+        int factorNr = 0;
+        for (AccumulationFactor factor : accexp.getConstraint().getFactors()) {
+                lhs += factor.getFactor().evaluateInt(mc.getConstantValues())
+                                * track.getWeight(factorNr);
+        }
 
-           // For DIA operators, we just check the bound.
-           // For BOX operators, we check the INVERTED bound.
-           
-           // TODO: THIS MAY BE BROKEN
-           switch(accexp.getSymbol()) {
-                   case ACCBOXMINUS:
-                   case ACCBOXPLUS:
-                           if (!rhs.isInBounds(lhs)) {
-                                   isGood = true;
-                           }
-                           mc.getLog().println("WARNING: This may be wrong.");
-                           break;
-                   case ACCDIAMINUS:
-                   case ACCDIAPLUS:
-                   case ACCUNTIL:
-                           if (rhs.isInBounds(lhs)) {
-                                   isGood = true;
-                           }
-                           break;
-                   default:
-                           throw new RuntimeException("Accumulation symbol cannot be handled...");
-                   }
-           //if(isGood) {mc.getLog().print("+");} else {mc.getLog().print("-");}
-           return isGood;
-   }
-
-
-	
-	/** 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;
+        // Check the bound
+        IntegerBound rhs = IntegerBound.fromTemporalOperatorBound(accexp.getConstraint().getBound(), mc.getConstantValues(), true);
+        
+        return rhs.isInBounds(lhs);
+	}
 
 	/** Get the initial Component of the accumulation monitor.
 	 * @return
 	 */
 	protected abstract Component getInitialComponent();
 	
-	/** 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);
-	
-	/** 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 abstract AccumulationTrack<Component> updateTrack(Integer modelFromStateId, final AccumulationTrack<Component> track,
-			final ExpressionAccumulation accexp, final double[] weights, final StateModelChecker mc);
-	
-	/** 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 abstract AccumulationState<Component> updateAccumulationState(final int modelFromStateId,
-			final AccumulationState<Component> accstate, final ExpressionAccumulation accexp,
-			final double[] weights, final ProbModelChecker mc) throws PrismException;
-	
 	/**
 	 * Creates the initial state for the accumulation part of this of this accumulation product. Returns its ID.
 	 * 
@@ -164,20 +71,7 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 	 * 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
-		int initialActiveTrack = 0;
-		
-		// Generate the initial track and product state
-		AccumulationTracker<Component> initialTracker = new AccumulationTracker<Component>(numberOfTracks, numberOfWeights, initialComponent);
-		int initialTrackerId  = trackers.findOrAdd(initialTracker);
-		AccumulationState<Component> initialAccState = new AccumulationState<Component>(initialTrackerId, initialActiveTrack, numberOfTracks);
-		int initialAccStateId = accStates.findOrAdd(initialAccState);
-		
-		return initialAccStateId;
-	}
+	protected abstract int createInitialStateId();
 	
 	protected abstract String labelString(Integer stateId);
 

prism/src/explicit/AccumulationProductComplex.java

@@ -4,15 +4,12 @@ import java.util.ArrayList;
 import java.util.BitSet;
 import java.util.Iterator;
 import java.util.Map;
-import java.util.Vector;
 
 import parser.ast.ExpressionAccumulation;
 import parser.ast.Expression;
 import prism.PrismException;
 
 import common.Dottable;
-import explicit.rewards.MCRewards;
-import explicit.rewards.Rewards;
 
 /**
  * An AccumulationProduct has ProductStates, where the first component is the
@@ -49,6 +46,21 @@ public abstract class AccumulationProductComplex<M extends Model,Component> exte
 		return goalStates.get(track);
 	}
 	
+	protected final int createInitialStateId() {
+		Component initialComponent = getInitialComponent();
+		
+		// The initial active track is the first one, all tracks are non-good by default
+		int initialActiveTrack = 0;
+		
+		// Generate the initial track and product state
+		AccumulationTracker<Component> initialTracker = new AccumulationTracker<Component>(numberOfTracks, numberOfWeights, initialComponent);
+		int initialTrackerId  = trackers.findOrAdd(initialTracker);
+		AccumulationState<Component> initialAccState = new AccumulationState<Component>(initialTrackerId, initialActiveTrack, numberOfTracks, false);
+		int initialAccStateId = accStates.findOrAdd(initialAccState);
+		
+		return initialAccStateId;
+	}
+	
 	protected void generateTrackInfo(ProductState state, Integer index, ExpressionAccumulation accexp, ProbModelChecker mc) throws PrismException {
 		AccumulationState<Component> accState = accStates.getById(state.getSecondState());
 		AccumulationTracker<Component> tracker = accState.getTracker(trackers);
@@ -73,6 +85,21 @@ public abstract class AccumulationProductComplex<M extends Model,Component> exte
 		}
 	}
 	
+
+	   /** 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 isGoalTrack(final AccumulationTrack<Component> track, final ExpressionAccumulation accexp, final ProbModelChecker mc)
+	                   throws PrismException {
+	           return isFinalTrack(track,accexp,mc) && constraintHolds(track,accexp,mc);
+	   }
+	
 	/** Checks whether a track is final according to the bound in the accumulation expression and the context in mc.
 	 * @param track
 	 * @param accexp

prism/src/explicit/AccumulationProductSimple.java

@@ -0,0 +1,277 @@
+package explicit;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.HashMap;
+import java.util.Iterator;
+import java.util.Map;
+
+import parser.ast.ExpressionAccumulation;
+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 <M>
+ */
+
+public abstract class AccumulationProductSimple<M extends Model,Component> extends AccumulationProduct<M,Component> implements Dottable
+{	
+	protected final BitSet goodStates;
+	
+	public AccumulationProductSimple(M originalModel) {
+		super(originalModel);
+		goodStates = new BitSet();
+	}
+	
+	public final BitSet getGoodStates() {
+		return goodStates;
+	}
+	
+	protected final int createInitialStateId() {
+		Component initialComponent = getInitialComponent();
+		
+		// The initial active track is the first one, all tracks are non-good by default
+		int initialActiveTrack = 0;
+		
+		// Generate the initial track and product state
+		AccumulationTracker<Component> initialTracker = new AccumulationTracker<Component>(numberOfTracks, numberOfWeights, initialComponent);
+		int initialTrackerId  = trackers.findOrAdd(initialTracker);
+		AccumulationState<Component> initialAccState = new AccumulationState<Component>(initialTrackerId, initialActiveTrack, numberOfTracks, true);
+		int initialAccStateId = accStates.findOrAdd(initialAccState);
+		
+		return initialAccStateId;
+	}
+	
+	protected void generateStateInfo(ProductState state, Integer index) throws PrismException {
+		AccumulationState<Component> accState = accStates.getById(state.getSecondState());
+		goodStates.set(index, accState.hasGoodTracks());
+	}
+	
+
+	   /** 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 isGoalTrack(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; }
+	           
+	           // For DIA operators, we just check the bound.
+	           // For BOX operators, we check the INVERTED bound.
+	           
+	           // TODO: THIS MAY BE BROKEN
+	           switch(accexp.getSymbol()) {
+               case ACCBOXMINUS:
+               case ACCBOXPLUS:
+                   mc.getLog().println("WARNING: This may be wrong.");
+                   return !constraintHolds(track,accexp,mc);
+               case ACCDIAMINUS:
+               case ACCDIAPLUS:
+            	   return constraintHolds(track,accexp,mc);
+               default:
+                       throw new RuntimeException("Accumulation symbol cannot be handled...");
+               }
+	   }
+	
+	/** 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;
+
+	/** Get the initial Component of the accumulation monitor.
+	 * @return
+	 */
+	protected abstract Component getInitialComponent();
+	
+	/** 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);
+	
+	/** 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.
+		AccumulationTracker<Component> oldTracker = accstate.getTracker(trackers);
+		ArrayList<AccumulationTrack<Component>> oldTracks = oldTracker.getTracks();
+		
+		// This restart will be...
+		int newLastRestartNr = accstate.getNextRestartNr();
+		//mc.getLog().print(newLastRestartNr);
+		
+		// Build the new tracks and determine their goodness;
+		ArrayList<AccumulationTrack<Component>> newTracks = new ArrayList<>();
+		BitSet newGoodTracks = (BitSet)accstate.getGoodTracks().clone();
+		
+		int trackNr = 0;
+		for(AccumulationTrack<Component> oldTrack : oldTracks) {
+			
+			AccumulationTrack<Component> newTrack;
+			
+			// restart or advance
+			if(trackNr == newLastRestartNr) {
+				// If we have a restart, we produce an initial track and let it advance.
+				// The goodness is cleared.
+				AccumulationTrack<Component> freshTrack = new AccumulationTrack<Component>(numberOfWeights, getInitialComponent());
+				//newTrack = updateTrack(modelFromStateId, freshTrack, accexp, weights, mc);
+				newTrack = freshTrack;
+				newGoodTracks.clear(trackNr);
+			} else if (oldTrack == null) {
+				// If the old track is undefined, the new track is as well.
+				// Goodness stays!
+				newTrack = null;
+			} else {
+				// Otherwise, the track is defined and advances.
+				// If it is not good yet, we check it.
+				assert oldTrack != null;
+				newTrack = updateTrack(modelFromStateId, oldTrack, accexp, weights, mc);
+				if(!newGoodTracks.get(trackNr)) {
+					newGoodTracks.set(trackNr, isGoalTrack(newTrack, accexp, mc));
+				}
+			}
+			
+			newTracks.add(newTrack);
+			trackNr++;
+		}
+		
+		//Create a new tracker with the right tracks and add it to storage.
+		AccumulationTracker<Component> newTracker = new AccumulationTracker<>(newTracks);
+		int newTrackerId = trackers.findOrAdd(newTracker);
+		
+		//Create the new AccState and its Goodness
+		AccumulationState<Component> newAccState = new AccumulationState<>(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks);
+		return newAccState;
+	}
+		
+	protected String labelString(Integer stateId) {
+		StringBuffer result = new StringBuffer();
+		if(goodStates.get(stateId)) { result.append("G: "); }
+
+		for(int t=0; t<numberOfTracks; t++) {
+			result.append("  " + t);
+			if(accStates.getById(prod_states.get(stateId).getSecondState()).getGoodTracks().get(t))  { result.append("+"); continue; }
+			result.append("_");
+		}
+
+		return result.toString();
+	}
+
+	@Override
+	public String toDot() {
+		StringBuffer result = new StringBuffer();
+		
+		result.append("digraph " + originalModel.getModelType() + " {\n");
+		
+		for(int i = 0; i < prod_states.size(); i++) {
+			ProductState fromState = prod_states.get(i);
+			AccumulationState<Component> accState = accStates.getById(fromState.getSecondState());
+			AccumulationTracker<Component> tracker = accState.getTracker(trackers);
+			result.append(""
+					+ i
+					+ "[shape=box, color=black"
+					+ " label= < <TABLE BORDER=\"0\">"
+					+ "<TR>"
+					+ "<TD>" + i + "=" + fromState + "</TD>"
+					+ "</TR><TR>"
+					+ "<TD> " + accState + "</TD>"
+					+ "</TR><TR>"
+					+ "<TD> " + labelString(i) + "</TD>"
+					+ "</TR><TR>"
+					+ "<TD>\"" + Dottable.quoteForDot(tracker.toString()) + "\"</TD>"
+					+ "</TR>"
+					+ " </TABLE> >]\n");
+			
+			switch(productModel.getModelType()) {
+			case DTMC:
+				DTMCExplicit castDTMC = (DTMCExplicit)productModel;
+				Iterator<Map.Entry<Integer, Double>> dtmcIter = castDTMC.getTransitionsIterator(i);
+				while (dtmcIter.hasNext()) {
+					Map.Entry<Integer, Double> 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<Map.Entry<Integer, Double>> mdpIter = castMDP.getTransitionsIterator(i, c);
+					while (mdpIter.hasNext()) {
+						Map.Entry<Integer, Double> e = mdpIter.next();
+						result.append(i + " -> " + e.getKey() + " [ label=\"");
+						result.append(c + "," + e.getValue() + "\" ];\n");
+					}
+				}
+				break;
+			default:
+				break;
+			}
+		}
+		
+		result.append("}");
+		
+		return result.toString();
+	}
+}

prism/src/explicit/AccumulationProductSimpleCounting.java

@@ -0,0 +1,213 @@
+package explicit;
+
+import java.util.BitSet;
+import java.util.Vector;
+
+import explicit.rewards.MCRewards;
+import explicit.rewards.MDPRewards;
+import explicit.rewards.Rewards;
+import parser.ast.ExpressionAccumulation;
+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 <M>
+ */
+
+public class AccumulationProductSimpleCounting<M extends Model> extends AccumulationProductSimple<M,Integer>
+{
+	
+	public AccumulationProductSimpleCounting(M originalModel) {
+		super(originalModel);
+	}
+	
+	@SuppressWarnings("unchecked")
+	public static <T extends Model, R extends Rewards> AccumulationProductSimpleCounting<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
+		switch(graph.getModelType()) {
+		case DTMC:
+			return (AccumulationProductSimpleCounting<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>)  rewards, mc, statesOfInterest);
+		case MDP:
+			return (AccumulationProductSimpleCounting<T>)generate((MDP)  graph, accexp, (Vector<MDPRewards>) rewards, mc, statesOfInterest);
+		default:
+			throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
+		}
+	}
+	
+	public static AccumulationProductSimpleCounting<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
+		final AccumulationProductSimpleCounting<DTMC> result = new AccumulationProductSimpleCounting<DTMC>(graph);
+		// Create auxiliary data
+		result.createAuxData(graph, accexp, rewards, mc);
+		
+		// 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<Integer> from_accstate = result.accStates.getById(from_state.getSecondState());
+				
+				// Get step weights
+				double[] weights = new double[rewards.size()];
+				
+				for (int i=0; i < rewards.size(); i++) {
+					weights[i] = rewards.get(i).getStateReward(from_state.getFirstState());
+				}
+				
+				// Update accumulation product state, store it and get its ID.
+				AccumulationState<Integer> to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc);
+				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<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
+		// This is basically the same thing as for DTMCs
+		final AccumulationProductSimpleCounting<MDP> result = new AccumulationProductSimpleCounting<MDP>(graph);
+		
+		// Create auxiliary data
+		result.createAuxData(graph, accexp, rewards, mc);
+
+		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<Integer> from_accstate = result.accStates.getById(from_state.getSecondState());
+				
+				// Get step weights
+				// THIS IS DIFFERENT FROM ABOVE!
+				double[] weights = new double[rewards.size()];
+				
+				for (int i=0; i < rewards.size(); i++) {
+					double currentWeight = rewards.get(i).getStateReward(from_state.getFirstState());
+					currentWeight += rewards.get(i).getTransitionReward(from_state.getFirstState(), choice_i);
+					weights[i] = currentWeight;
+				}
+
+				// Update accumulation product state, store it and get its ID.
+				AccumulationState<Integer> to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc);
+				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<Integer> track, final ExpressionAccumulation accexp, final ProbModelChecker mc)
+			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(accexp.getBoundExpression(), mc.getConstantValues(), true);
+				isFinal = stepBound.isInBounds(step);
+			}
+		}
+		return isFinal;
+	}
+	
+	@Override
+	protected Integer getInitialComponent() {
+		return 0;
+	}
+	
+	@Override
+	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("...");
+		}
+		
+		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, final ExpressionAccumulation accexp, final Vector<? extends Rewards> rewards, final ProbModelChecker mc) throws PrismException {
+		numberOfTracks  = IntegerBound.fromTemporalOperatorBound(accexp.getBoundExpression(), mc.getConstantValues(), true).getHighestInteger()+2;
+		numberOfWeights = rewards.size();
+	}
+}

prism/src/explicit/AccumulationProductSimpleRegular.java

@@ -0,0 +1,244 @@
+package explicit;
+
+import java.util.ArrayList;
+import java.util.BitSet;
+import java.util.Vector;
+
+import automata.finite.DeterministicFiniteAutomaton;
+import automata.finite.EdgeLabel;
+import automata.finite.NondeterministicFiniteAutomaton;
+import automata.finite.State;
+import explicit.rewards.MCRewards;
+import explicit.rewards.MDPRewards;
+import explicit.rewards.Rewards;
+import parser.ast.ExpressionAccumulation;
+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 <M>
+ */
+
+public class AccumulationProductSimpleRegular<M extends Model> extends AccumulationProductSimple<M,State>
+{
+	protected DeterministicFiniteAutomaton<String> automaton;
+
+	public AccumulationProductSimpleRegular(M originalModel) {
+		super(originalModel);
+	}
+	
+	@SuppressWarnings("unchecked")
+	public static <T extends Model, R extends Rewards> AccumulationProductSimpleRegular<T> generate(final Model graph, final ExpressionAccumulation accexp, final Vector<R> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
+		switch(graph.getModelType()) {
+		case DTMC:
+			return (AccumulationProductSimpleRegular<T>)generate((DTMC) graph, accexp, (Vector<MCRewards>)  rewards, mc, statesOfInterest);
+		case MDP:
+			return (AccumulationProductSimpleRegular<T>)generate((MDP)  graph, accexp, (Vector<MDPRewards>) rewards, mc, statesOfInterest);
+		default:
+			throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
+		}
+	}
+	
+	public static AccumulationProductSimpleRegular<DTMC> generate(final DTMC graph, final ExpressionAccumulation accexp, final Vector<MCRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
+		final AccumulationProductSimpleRegular<DTMC> result = new AccumulationProductSimpleRegular<DTMC>(graph);
+		// Create auxiliary data
+		result.createAuxData(graph, accexp, rewards, mc);
+		
+		// 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<State> from_accstate = result.accStates.getById(from_state.getSecondState());
+				
+				// Get step weights
+				double[] weights = new double[rewards.size()];
+				
+				for (int i=0; i < rewards.size(); i++) {
+					weights[i] = rewards.get(i).getStateReward(from_state.getFirstState());
+				}
+				
+				// Update accumulation product state, store it and get its ID.
+				AccumulationState<State> to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc);
+				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<MDP> generate(final MDP graph, final ExpressionAccumulation accexp, final Vector<MDPRewards> rewards, final ProbModelChecker mc, BitSet statesOfInterest) throws PrismException {
+		// This is basically the same thing as for DTMCs
+		final AccumulationProductSimpleRegular<MDP> result = new AccumulationProductSimpleRegular<MDP>(graph);
+		
+		// Create auxiliary data
+		result.createAuxData(graph, accexp, rewards, mc);
+
+		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<State> from_accstate = result.accStates.getById(from_state.getSecondState());
+				
+				// Get step weights
+				// THIS IS DIFFERENT FROM ABOVE!
+				double[] weights = new double[rewards.size()];
+				
+				for (int i=0; i < rewards.size(); i++) {
+					double currentWeight = rewards.get(i).getStateReward(from_state.getFirstState());
+					currentWeight += rewards.get(i).getTransitionReward(from_state.getFirstState(), choice_i);
+					weights[i] = currentWeight;
+				}
+
+				// Update accumulation product state, store it and get its ID.
+				AccumulationState<State> to_accproduct = result.updateAccumulationState(from_state.getFirstState(), from_accstate, accexp, weights, mc);
+				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<State> track, ExpressionAccumulation accexp, ProbModelChecker mc) 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<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();
+		
+		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<String> 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, final ExpressionAccumulation accexp, final Vector<? extends Rewards> rewards, final ProbModelChecker mc) throws PrismException {
+		// Build labels and DFA
+		AccumulationModelChecker accMc = new AccumulationModelChecker();
+		ExpressionRegular reg = (ExpressionRegular)accMc.checkMaximalStateFormulas(mc, graph, accexp.getRegularExpression(), labels);
+		
+		// Create and store the actual DFA
+		NondeterministicFiniteAutomaton<String> nfa = NondeterministicFiniteAutomaton.fromExpressionRegular(reg);
+		//System.out.println(nfa.toDot());
+		
+		automaton = nfa.determinize();
+		automaton.trim(); // This should remove cycles.
+		
+		if(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= rewards.size();
+	}
+}

prism/src/explicit/AccumulationState.java

@@ -1,9 +1,12 @@
 package explicit;
 
+import java.util.BitSet;
+import java.util.Objects;
+
 /**
  * An AccumulationState contains a reference to an AccumulationTracker, 
- * a pointer to the latest restart and
- * the numberOfTracks in the tracker.
+ * a pointer to the latest restart and the numberOfTracks in the tracker.
+ * It can optionally contain a BitSet marking the goodTracks.
  * 
  * @author Sascha Wunderlich
  *
@@ -14,8 +17,20 @@ public class AccumulationState<Component> {
 	int lastRestartNr;
 	int numberOfTracks;
 	
+	BitSet goodTracks;
+	
 	public AccumulationState(int trackerId, int lastRestartNr, int numberOfTracks) {
+		this(trackerId, lastRestartNr, numberOfTracks, false);
+	}
+	
+	public AccumulationState(int trackerId, int lastRestartNr, int numberOfTracks, BitSet goodTracks) {
+		this(trackerId, lastRestartNr, numberOfTracks);
+		this.goodTracks = goodTracks;
+	}
+	
+	public AccumulationState(int trackerId, int lastRestartNr, int numberOfTracks, boolean withGoodTracks) {
 		super();
+		if(withGoodTracks) { goodTracks = new BitSet(numberOfTracks); }
 		this.trackerId = trackerId;
 		this.lastRestartNr = lastRestartNr;
 		this.numberOfTracks = numberOfTracks;
@@ -33,17 +48,19 @@ public class AccumulationState<Component> {
 		return (lastRestartNr + 1) % numberOfTracks;
 	}
 	
-
+	public boolean hasGoodTracks() {
+		return !goodTracks.isEmpty();
+	}
+	
+	public BitSet getGoodTracks() {
+		return goodTracks;
+	}
+	
 	@Override
 	public int hashCode() {
-		final int prime = 31;
-		int result = 1;
-		result = prime * result + lastRestartNr;
-		result = prime * result + numberOfTracks;
-		result = prime * result + trackerId;
-		return result;
+		return Objects.hash(goodTracks, lastRestartNr, numberOfTracks, trackerId);
 	}
-	
+
 	@Override
 	public boolean equals(Object obj) {
 		if (this == obj)
@@ -53,13 +70,8 @@ public class AccumulationState<Component> {
 		if (getClass() != obj.getClass())
 			return false;
 		AccumulationState other = (AccumulationState) obj;
-		if (lastRestartNr != other.lastRestartNr)
-			return false;
-		if (numberOfTracks != other.numberOfTracks)
-			return false;
-		if (trackerId != other.trackerId)
-			return false;
-		return true;
+		return Objects.equals(goodTracks, other.goodTracks) && lastRestartNr == other.lastRestartNr
+				&& numberOfTracks == other.numberOfTracks && trackerId == other.trackerId;
 	}
 
 	@Override

prism/src/explicit/AccumulationTransformation.java

@@ -10,18 +10,19 @@ import parser.ast.Expression;
 import parser.ast.ExpressionAccumulation;
 import parser.ast.ExpressionReward;
 import parser.ast.RewardStruct;
-import parser.visitor.ReplaceAccumulationExpression;
+import parser.visitor.ReplaceAccumulationExpressionComplex;
+import parser.visitor.ReplaceAccumulationExpressionSimple;
 import prism.PrismException;
 import prism.PrismSettings;
 
 public class AccumulationTransformation<M extends Model> implements ModelExpressionTransformation<M, M> {
-	final private Expression originalExpression;
-	final private M originalModel;
-	final private BitSet statesOfInterest;
-	final ProbModelChecker mc;
+	final protected Expression originalExpression;
+	final protected M originalModel;
+	final protected BitSet statesOfInterest;
+	final protected ProbModelChecker mc;
 	
-	private Expression transformedExpression;
-	private AccumulationProduct<M,?> product;
+	protected Expression transformedExpression;
+	protected AccumulationProduct<M,?> product;
 	
 	public AccumulationTransformation(
 			ProbModelChecker mc,
@@ -63,7 +64,7 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 		return product.projectToOriginalModel(svTransformedModel);
 	}
 	
-	private void doTransformation() throws PrismException {
+	protected void doTransformation() throws PrismException {
 		mc.getLog().println("Performing accumulation transformation...");
 		// We work on a copy
 		transformedExpression = originalExpression.deepCopy();
@@ -71,8 +72,8 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 		// Get the first ExpressionAccumulation
 		ExpressionAccumulation accexp = transformedExpression.getFirstAccumulationExpression();
 	    mc.getLog().println(" [AT] for " + accexp);
-	    
-		// Get the rewards and build the product   
+		
+		// Get the rewards
 	    Vector<Rewards> rewards = new Vector<Rewards>();
 		
 		for (int i=0; i < accexp.getConstraint().getFactors().size(); i++) {
@@ -85,19 +86,19 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 			Rewards reward = constructRewards.buildRewardStructure(originalModel, rewStruct, mc.getConstantValues());
 			rewards.add(i,reward);
 		}
-	    
-	    boolean isComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX) || accexp.hasFireOn() || !accexp.isNullary();
-	    if (isComplex) { 
-	    	mc.getLog().println("    ... which is COMPLEX.");
-	    	doTransformationComplex(accexp, rewards);
-	    } else {
-	    	mc.getLog().println("    ... which is SIMPLE.");
-	    	doTransformationSimple(accexp, rewards);
-	    }
+		
+		// Figure out if we need a complex or a simple trafo...
+		boolean isComplex = mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX) || accexp.hasFireOn() || !accexp.isNullary();
+		if(isComplex) {
+			mc.getLog().println(" ... which is complex!");
+			doTransformationComplex(accexp, rewards);
+		} else {
+			mc.getLog().println(" ... which is simple!");
+			doTransformationSimple(accexp, rewards);
+		}
 	}
-	
-	@SuppressWarnings("unchecked")
-	private void doTransformationComplex(ExpressionAccumulation accexp, Vector<Rewards> rewards) throws PrismException {
+
+	protected void doTransformationComplex(ExpressionAccumulation accexp, Vector<Rewards> rewards) throws PrismException {
 		// Build the product
 		if(accexp.hasRegularExpression()) {
 			product = (AccumulationProductComplexRegular<M>) AccumulationProductComplexRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest);
@@ -116,70 +117,55 @@ public class AccumulationTransformation<M extends Model> implements ModelExpress
 		ArrayList<String> runLabels  = new ArrayList<String>();
 		ArrayList<String> goalLabels = new ArrayList<String>();
 		
-		AccumulationProductComplex<M,?> productComplex = (AccumulationProductComplex<M,?>) product;
-		
-		for(int track=0; track < productComplex.getNumberOfTracks(); track++) {
-			BitSet initStates = productComplex.getInitStates(track);
-			BitSet runStates  = productComplex.getRunStates(track);
-			BitSet goalStates = productComplex.getGoalStates(track);
+		for(int track=0; track < product.getNumberOfTracks(); track++) {
+			BitSet initStates = ((AccumulationProductComplex<M,?>)product).getInitStates(track);
+			BitSet runStates  = ((AccumulationProductComplex<M,?>)product).getRunStates(track);
+			BitSet goalStates = ((AccumulationProductComplex<M,?>)product).getGoalStates(track);
 			
-			String initLabel = ((ModelExplicit)productComplex.getTransformedModel()).addUniqueLabel("init" + track, initStates, productComplex.getTransformedModel().getLabels());
+			String initLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("init" + track, initStates, product.getTransformedModel().getLabels());
 			initLabels.add(initLabel);
-			String runLabel  = ((ModelExplicit)productComplex.getTransformedModel()).addUniqueLabel("run" + track,  runStates, productComplex.getTransformedModel().getLabels());
+			String runLabel  = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("run" + track,  runStates, product.getTransformedModel().getLabels());
 			runLabels.add(runLabel);
-			String goalLabel = ((ModelExplicit)productComplex.getTransformedModel()).addUniqueLabel("goal" + track, goalStates, productComplex.getTransformedModel().getLabels());
+			String goalLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal" + track, goalStates, product.getTransformedModel().getLabels());
 			goalLabels.add(goalLabel);
-
-			//mc.getLog().println(initStates + " | " + initLabel);
-			//mc.getLog().println(runStates  + " | " + runLabel);
-			//mc.getLog().println(goalStates + " | " + goalLabel);
 		}
 		// Transform the expression
 		mc.getLog().println(" [AT] replacing the formula...");
-		ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, mc, initLabels, runLabels, goalLabels, product.getNumberOfTracks()-1);
+		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());
 		if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) {
 		product.exportToDotFile("DEBUG-product.dot");
 		}
-}
+	}	
 	
-	@SuppressWarnings("unchecked")
-	private void doTransformationSimple(ExpressionAccumulation accexp, Vector<Rewards> rewards) throws PrismException {
-		throw new PrismException("Stop, Hammer Time!");
-		/*
-		AccumulationProductSimple<M,?> productSimple = (AccumulationProductSimple<M,?>) product;
-		
+	protected void doTransformationSimple(ExpressionAccumulation accexp, Vector<Rewards> rewards) throws PrismException {
 		// Build the product
 		if(accexp.hasRegularExpression()) {
-			productSimple = (AccumulationProductSimpleRegular<M>) AccumulationProductSimpleRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest);
+			//throw new PrismException("I don't know how to do regular things...");
+			product = (AccumulationProductSimpleRegular<M>) AccumulationProductSimpleRegular.generate(originalModel, accexp, rewards, mc, statesOfInterest);
 		} else if (accexp.hasBoundExpression()) {
-			productSimple = (AccumulationProductSimpleCounting<M>) AccumulationProductSimpleCounting.generate(originalModel, accexp, rewards, mc, statesOfInterest);
+			product = (AccumulationProductSimpleCounting<M>) AccumulationProductSimpleCounting.generate(originalModel, accexp, rewards, mc, statesOfInterest);
 		} else {
 			throw new PrismException("Accumulation Expression has no valid monitor!");
 		}
 		
-		mc.getLog().println(" [AT] finished product construction: " + productSimple.getTransformedModel().getNumStates());
+		mc.getLog().println(" [AT] finished product construction: " + product.getTransformedModel().getNumStates());
 		
 		// Transform the model
-		mc.getLog().println(" [AT] getting the init/run/goal states: ");
-		
-		ArrayList<String> goalLabels = new ArrayList<String>();
-
-		BitSet goodStates = productSimple.getGoodStates();
-		String goalLabel = ((ModelExplicit)productSimple.getTransformedModel()).addUniqueLabel("good", goodStates, productSimple.getTransformedModel().getLabels());
-		goalLabels.add(goalLabel);
+		mc.getLog().println(" [AT] getting the good states: ");
 		
+		BitSet goodStates = ((AccumulationProductSimple<M,?>)product).getGoodStates();
+		String goodLabel = ((ModelExplicit)product.getTransformedModel()).addUniqueLabel("goal", goodStates, product.getTransformedModel().getLabels());
 		// Transform the expression
 		mc.getLog().println(" [AT] replacing the formula...");
-		ReplaceAccumulationExpression replace = new ReplaceAccumulationExpression(accexp, mc, null, null, goalLabels, productSimple.getNumberOfTracks()-1);
+		ReplaceAccumulationExpressionSimple replace = new ReplaceAccumulationExpressionSimple(accexp, goodLabel, product.getNumberOfTracks()-1);
 		transformedExpression = (Expression)transformedExpression.accept(replace);
 		mc.getLog().println(" [AT] " + originalExpression.toString() + "\n" +
 							"   -> " + transformedExpression.toString());
 		if(mc.getSettings().getBoolean(PrismSettings.ACC_GENERATE_DOTS)) {
-			productSimple.exportToDotFile("DEBUG-product.dot");
+		product.exportToDotFile("DEBUG-product.dot");
 		}
-		*/
 	}
-}
+}

prism/src/parser/visitor/ReplaceAccumulationExpression.java → prism/src/parser/visitor/ReplaceAccumulationExpressionComplex.java

@@ -2,34 +2,25 @@ package parser.visitor;
 
 import java.util.ArrayList;
 
-import explicit.ProbModelChecker;
-import parser.ast.AccumulationSymbol;
 import parser.ast.Expression;
 import parser.ast.ExpressionAccumulation;
 import parser.ast.ExpressionBinaryOp;
 import parser.ast.ExpressionLabel;
 import parser.ast.ExpressionTemporal;
-import parser.ast.ExpressionUnaryOp;
-import parser.ast.TemporalOperatorBound;
-import parser.ast.TemporalOperatorBounds;
-import prism.IntegerBound;
 import prism.PrismLangException;
-import prism.PrismSettings;
 
 
-public class ReplaceAccumulationExpression extends ASTTraverseModify {
+public class ReplaceAccumulationExpressionComplex extends ASTTraverseModify {
 
 	private ExpressionAccumulation accexp;
-	private ProbModelChecker mc;
 	private ArrayList<String> initLabels;
 	private ArrayList<String> runLabels;
 	private ArrayList<String> goalLabels;
 	private int accLength;
 	
-	public ReplaceAccumulationExpression(ExpressionAccumulation accexp, ProbModelChecker mc, ArrayList<String> initLabels, ArrayList<String> runLabels, ArrayList<String> goalLabels, int accLength) {
+	public ReplaceAccumulationExpressionComplex(ExpressionAccumulation accexp, ArrayList<String> initLabels, ArrayList<String> runLabels, ArrayList<String> goalLabels, int accLength) {
 		super();
 		this.accexp = accexp;
-		this.mc = mc;
 		this.initLabels = initLabels;
 		this.runLabels = runLabels;
 		this.goalLabels = goalLabels;
@@ -73,42 +64,11 @@ public class ReplaceAccumulationExpression extends ASTTraverseModify {
 		return result;
 	}
 	
-	private Object replaceWithReach(ExpressionAccumulation expr) throws PrismLangException {
-		AccumulationSymbol sym = accexp.getSymbol();
-		
-		ExpressionLabel label = new ExpressionLabel(goalLabels.get(0));
-		
-		if (sym.isPlus()) {
-			ExpressionTemporal fExpr = new ExpressionTemporal(ExpressionTemporal.P_F, null, label);
-			TemporalOperatorBounds fBounds = new TemporalOperatorBounds();
-			TemporalOperatorBound  fBound = IntegerBound.fromEqualBounds(accLength).toTemporalOperatorBound();
-			fBounds.setDefaultBound(fBound);
-			fExpr.setBounds(fBounds);
-			// If its a BOX, negate it
-			if (sym.isBox()) {
-				return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, fExpr);
-			} else {
-				return fExpr;
-			}
-		} else { //isMinus
-			if (sym.isBox()) {
-				return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, label);
-			} else {
-				return label;
-			}
-		}
-	}
-	
 	public Object visit(ExpressionAccumulation expr) throws PrismLangException
 	{
 		if (expr == accexp) {
-			if (mc.getSettings().getBoolean(PrismSettings.ACC_FORCE_COMPLEX) || accexp.hasFireOn() || !accexp.isNullary()) {
-				// This is a complex accumulation expression. Rewrite to until formula.
-				return replaceWithUntil(expr);
-			} else {
-				// This is a simple accumulation expression. Rewrite to F=....
-				return replaceWithReach(expr);
-			}
+			// This is a complex accumulation expression. Rewrite to until formula.
+			return replaceWithUntil(expr);
 		} else {
 			return expr;
 		}

prism/src/parser/visitor/ReplaceAccumulationExpressionSimple.java

@@ -0,0 +1,61 @@
+package parser.visitor;
+
+import parser.ast.AccumulationSymbol;
+import parser.ast.ExpressionAccumulation;
+import parser.ast.ExpressionLabel;
+import parser.ast.ExpressionTemporal;
+import parser.ast.ExpressionUnaryOp;
+import parser.ast.TemporalOperatorBound;
+import parser.ast.TemporalOperatorBounds;
+import prism.IntegerBound;
+import prism.PrismLangException;
+
+public class ReplaceAccumulationExpressionSimple extends ASTTraverseModify {
+
+	private ExpressionAccumulation accexp;
+	private String goodLabel;
+	private int accLength;
+	
+	public ReplaceAccumulationExpressionSimple(ExpressionAccumulation accexp, String goodLabel, int accLength) {
+		super();
+		this.accexp = accexp;
+		this.goodLabel = goodLabel;
+		this.accLength = accLength;
+	}
+	
+	private Object replaceWithReach(ExpressionAccumulation expr) throws PrismLangException {
+		AccumulationSymbol sym = accexp.getSymbol();
+		
+		ExpressionLabel label = new ExpressionLabel(goodLabel);
+		
+		if (sym.isPlus()) {
+			ExpressionTemporal fExpr = new ExpressionTemporal(ExpressionTemporal.P_F, null, label);
+			TemporalOperatorBounds fBounds = new TemporalOperatorBounds();
+			TemporalOperatorBound  fBound = IntegerBound.fromEqualBounds(accLength).toTemporalOperatorBound();
+			fBounds.setDefaultBound(fBound);
+			fExpr.setBounds(fBounds);
+			// If its a BOX, negate it
+			if (sym.isBox()) {
+				return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, fExpr);
+			} else {
+				return fExpr;
+			}
+		} else { //isMinus
+			if (sym.isBox()) {
+				return new ExpressionUnaryOp(ExpressionUnaryOp.NOT, label);
+			} else {
+				return label;
+			}
+		}
+	}
+	
+	public Object visit(ExpressionAccumulation expr) throws PrismLangException
+	{
+		if (expr == accexp) {
+			// This is a simple accumulation expression. Rewrite to F=....
+			return replaceWithReach(expr);
+		} else {
+			return expr;
+		}
+	}
+}