accumulation: deduplicate the rest

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> rewards, StateModelChecker mc, boolean singleTrack) {
+	public AccumulationContext(ExpressionAccumulation accexp, Vector<Rewards> rewards, StateModelChecker mc) {
 		this.accexp = accexp;
 		this.rewards = rewards;
 		this.mc = mc;
-		this.singleTrack = singleTrack;
 	}
 	
 	// A mini reward wrapper.

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<M extends Model,Component> extends Pro
 	
 	protected int numberOfTracks;
 	protected int numberOfWeights;
+
+	protected final ArrayList<BitSet> initStates;
+	protected final ArrayList<BitSet> runStates;
+	protected final ArrayList<BitSet> goalStates;
 	
 	public AccumulationProduct(M originalModel, AccumulationContext ctx) {
 		super(originalModel);
@@ -40,6 +45,10 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 		
 		labels = new ArrayList<BitSet>();
 		
+		initStates = new ArrayList<>();
+		runStates  = new ArrayList<>();
+		goalStates = new ArrayList<>();
+		
 		this.ctx = ctx;
 	}
 	
@@ -179,8 +188,6 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 	}
 	
 	protected abstract boolean isFinalTrack(AccumulationTrack<Component> track) throws PrismException;
-	
-	protected abstract String labelString(Integer stateId);
 
 	@Override
 	public String toDot() {
@@ -237,4 +244,64 @@ public abstract class AccumulationProduct<M extends Model,Component> 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<Component> 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<Component> tracker = accState.getTracker(trackers);
+		
+		for(int trackIdx=0; trackIdx<tracker.getTracks().size(); trackIdx++) {
+			AccumulationTrack<Component> 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<numberOfTracks; t++) {
+			result.append("  " + t);
+			if(ctx.simpleMethod) {
+				AccumulationState<?> 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();
+	}
 }

prism/src/explicit/AccumulationProductComplex.java

@@ -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 <M>
- */
-
-public abstract class AccumulationProductComplex<M extends Model,Component> extends AccumulationProduct<M,Component> implements Dottable
-{	
-	protected final ArrayList<BitSet> initStates;
-	protected final ArrayList<BitSet> runStates;
-	protected final ArrayList<BitSet> 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<Component> accState = accStates.getById(state.getSecondState());
-		AccumulationTracker<Component> tracker = accState.getTracker(trackers);
-		
-		for(int trackIdx=0; trackIdx<tracker.getTracks().size(); trackIdx++) {
-			AccumulationTrack<Component> 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<numberOfTracks; t++) {
-			result.append("  " + t);
-			if(initStates.get(t).get(stateId)) { result.append("I"); continue; }
-			if(goalStates.get(t).get(stateId)) { result.append("G"); continue; }
-			if(runStates.get(t).get(stateId))  { result.append("R"); 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/AccumulationProductComplexCounting.java → prism/src/explicit/AccumulationProductCounting.java

@@ -16,27 +16,27 @@ import prism.PrismException;
  * @param <M>
  */
 
-public class AccumulationProductComplexCounting<M extends Model> extends AccumulationProductComplex<M,Integer>
+public class AccumulationProductCounting<M extends Model> extends AccumulationProduct<M,Integer>
 {
 	
-	public AccumulationProductComplexCounting(M originalModel, AccumulationContext ctx) {
+	public AccumulationProductCounting(M originalModel, AccumulationContext ctx) {
 		super(originalModel, ctx);
 	}
 	
 	@SuppressWarnings("unchecked")
-	public static <T extends Model, R extends Rewards> AccumulationProductComplexCounting<T> generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
+	public static <T extends Model, R extends Rewards> AccumulationProductCounting<T> generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
 		switch(graph.getModelType()) {
 		case DTMC:
-			return (AccumulationProductComplexCounting<T>)generate((DTMC) graph, ctx, statesOfInterest);
+			return (AccumulationProductCounting<T>)generate((DTMC) graph, ctx, statesOfInterest);
 		case MDP:
-			return (AccumulationProductComplexCounting<T>)generate((MDP)  graph, ctx, statesOfInterest);
+			return (AccumulationProductCounting<T>)generate((MDP)  graph, ctx, statesOfInterest);
 		default:
 			throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
 		}
 	}
 	
-	public static AccumulationProductComplexCounting<DTMC> generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
-		final AccumulationProductComplexCounting<DTMC> result = new AccumulationProductComplexCounting<DTMC>(graph, ctx);
+	public static AccumulationProductCounting<DTMC> generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
+		final AccumulationProductCounting<DTMC> result = new AccumulationProductCounting<DTMC>(graph, ctx);
 		// Create auxiliary data
 		result.createAuxData(graph);
 		
@@ -89,9 +89,9 @@ public class AccumulationProductComplexCounting<M extends Model> extends Accumul
 		return result;
 	}
 	
-	public static AccumulationProductComplexCounting<MDP> generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
+	public static AccumulationProductCounting<MDP> generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
 		// This is basically the same thing as for DTMCs
-		final AccumulationProductComplexCounting<MDP> result = new AccumulationProductComplexCounting<MDP>(graph, ctx);
+		final AccumulationProductCounting<MDP> result = new AccumulationProductCounting<MDP>(graph, ctx);
 		
 		// Create auxiliary data
 		result.createAuxData(graph);
@@ -182,10 +182,14 @@ public class AccumulationProductComplexCounting<M extends Model> extends Accumul
 		numberOfTracks  = IntegerBound.fromTemporalOperatorBound(ctx.accexp.getBoundExpression(), ctx.mc.getConstantValues(), true).getHighestInteger()+1;
 		numberOfWeights = ctx.rewards.size();
 		
-		for(int i=0; i<numberOfTracks; i++) {
-			initStates.add(new BitSet());
-			runStates.add(new BitSet());
+		if(ctx.simpleMethod) {
 			goalStates.add(new BitSet());
+		} else {
+			for(int i=0; i<numberOfTracks; i++) {
+				initStates.add(new BitSet());
+				runStates.add(new BitSet());
+				goalStates.add(new BitSet());
+			}
 		}
 	}
 }

prism/src/explicit/AccumulationProductComplexRegular.java → prism/src/explicit/AccumulationProductRegular.java

@@ -22,28 +22,28 @@ import prism.PrismSettings;
  * @param <M>
  */
 
-public class AccumulationProductComplexRegular<M extends Model> extends AccumulationProductComplex<M,State>
+public class AccumulationProductRegular<M extends Model> extends AccumulationProduct<M,State>
 {
 	protected DeterministicFiniteAutomaton<String> automaton;
 	
-	public AccumulationProductComplexRegular(M originalModel, AccumulationContext ctx) {
+	public AccumulationProductRegular(M originalModel, AccumulationContext ctx) {
 		super(originalModel, ctx);
 	}
 	
 	@SuppressWarnings("unchecked")
-	public static <T extends Model, R extends Rewards> AccumulationProductComplexRegular<T> generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
+	public static <T extends Model, R extends Rewards> AccumulationProductRegular<T> generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
 		switch(graph.getModelType()) {
 		case DTMC:
-			return (AccumulationProductComplexRegular<T>)generate((DTMC) graph, ctx, statesOfInterest);
+			return (AccumulationProductRegular<T>)generate((DTMC) graph, ctx, statesOfInterest);
 		case MDP:
-			return (AccumulationProductComplexRegular<T>)generate((MDP)  graph, ctx, statesOfInterest);
+			return (AccumulationProductRegular<T>)generate((MDP)  graph, ctx, statesOfInterest);
 		default:
 			throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
 		}
 	}
 	
-	public static AccumulationProductComplexRegular<DTMC> generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
-		final AccumulationProductComplexRegular<DTMC> result = new AccumulationProductComplexRegular<DTMC>(graph, ctx);
+	public static AccumulationProductRegular<DTMC> generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
+		final AccumulationProductRegular<DTMC> result = new AccumulationProductRegular<DTMC>(graph, ctx);
 		// Create auxiliary data
 		result.createAuxData(graph);
 		
@@ -97,9 +97,9 @@ public class AccumulationProductComplexRegular<M extends Model> extends Accumula
 		return result;
 	}
 	
-	public static AccumulationProductComplexRegular<MDP> generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
+	public static AccumulationProductRegular<MDP> generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
 		// This is basically the same thing as for DTMCs
-		final AccumulationProductComplexRegular<MDP> result = new AccumulationProductComplexRegular<MDP>(graph, ctx);
+		final AccumulationProductRegular<MDP> result = new AccumulationProductRegular<MDP>(graph, ctx);
 		// Create auxiliary data
 		result.createAuxData(graph);
 
@@ -226,10 +226,14 @@ public class AccumulationProductComplexRegular<M extends Model> extends Accumula
 		numberOfTracks = automaton.getLongestPathLength()+1;
 		numberOfWeights= ctx.rewards.size();
 		
-		for(int i=0; i<numberOfTracks; i++) {
-			initStates.add(new BitSet());
-			runStates.add(new BitSet());
+		if(ctx.simpleMethod) {
 			goalStates.add(new BitSet());
+		} else {
+			for(int i=0; i<numberOfTracks; i++) {
+				initStates.add(new BitSet());
+				runStates.add(new BitSet());
+				goalStates.add(new BitSet());
+			}
 		}
 	}
 }

prism/src/explicit/AccumulationProductSimple.java

@@ -1,107 +0,0 @@
-package explicit;
-
-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 <M>
- */
-
-public abstract class AccumulationProductSimple<M extends Model,Component> extends AccumulationProduct<M,Component> 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<Component> 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<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

@@ -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 <M>
- */
-
-public class AccumulationProductSimpleCounting<M extends Model> extends AccumulationProductSimple<M,Integer>
-{
-	
-	public AccumulationProductSimpleCounting(M originalModel, AccumulationContext ctx) {
-		super(originalModel, ctx);
-	}
-	
-	@SuppressWarnings("unchecked")
-	public static <T extends Model, R extends Rewards> AccumulationProductSimpleCounting<T> generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
-		switch(graph.getModelType()) {
-		case DTMC:
-			return (AccumulationProductSimpleCounting<T>)generate((DTMC) graph, ctx, statesOfInterest);
-		case MDP:
-			return (AccumulationProductSimpleCounting<T>)generate((MDP)  graph, ctx, statesOfInterest);
-		default:
-			throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
-		}
-	}
-	
-	public static AccumulationProductSimpleCounting<DTMC> generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
-		final AccumulationProductSimpleCounting<DTMC> result = new AccumulationProductSimpleCounting<DTMC>(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<Integer> 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<Integer> 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<MDP> generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
-		// This is basically the same thing as for DTMCs
-		final AccumulationProductSimpleCounting<MDP> result = new AccumulationProductSimpleCounting<MDP>(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<Integer> 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<Integer> 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<Integer> 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<Integer> 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();
-	}
-}

prism/src/explicit/AccumulationProductSimpleRegular.java

@@ -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 <M>
- */
-
-public class AccumulationProductSimpleRegular<M extends Model> extends AccumulationProductSimple<M,State>
-{
-	protected DeterministicFiniteAutomaton<String> automaton;
-
-	public AccumulationProductSimpleRegular(M originalModel, AccumulationContext ctx) {
-		super(originalModel, ctx);
-	}
-	
-	@SuppressWarnings("unchecked")
-	public static <T extends Model, R extends Rewards> AccumulationProductSimpleRegular<T> generate(final Model graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
-		switch(graph.getModelType()) {
-		case DTMC:
-			return (AccumulationProductSimpleRegular<T>)generate((DTMC) graph, ctx, statesOfInterest);
-		case MDP:
-			return (AccumulationProductSimpleRegular<T>)generate((MDP)  graph, ctx, statesOfInterest);
-		default:
-			throw new PrismException("Can't handle accumulation product for " + graph.getModelType());
-		}
-	}
-	
-	public static AccumulationProductSimpleRegular<DTMC> generate(final DTMC graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
-		final AccumulationProductSimpleRegular<DTMC> result = new AccumulationProductSimpleRegular<DTMC>(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<State> 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<State> 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<MDP> generate(final MDP graph, AccumulationContext ctx, BitSet statesOfInterest) throws PrismException {
-		// This is basically the same thing as for DTMCs
-		final AccumulationProductSimpleRegular<MDP> result = new AccumulationProductSimpleRegular<MDP>(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<State> 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<State> 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<State> 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<State> track) {
-		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) 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<String> 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();
-	}
-}

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<M extends ModelExplicit> implements Mode
 	protected Expression transformedExpression;
 	protected AccumulationProduct<M,?> product;
 	
+	ArrayList<String> initLabels;
+	ArrayList<String> runLabels;
+	ArrayList<String> goalLabels;
+	
 	public AccumulationTransformation(
 			StateModelChecker mc,
 			M originalModel, Expression expr,
@@ -35,6 +40,11 @@ public class AccumulationTransformation<M extends ModelExplicit> 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<M extends ModelExplicit> 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<M extends ModelExplicit> 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<M extends ModelExplicit> 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<M extends ModelExplicit> 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<M>) AccumulationProductComplexRegular.generate(originalModel, ctx, statesOfInterest);
+			product = AccumulationProductRegular.generate(originalModel, ctx, statesOfInterest);
 		} else if (ctx.accexp.hasBoundExpression()) {
-			product = (AccumulationProductComplexCounting<M>) 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<String> initLabels = new ArrayList<String>();
-		ArrayList<String> runLabels  = new ArrayList<String>();
-		ArrayList<String> goalLabels = new ArrayList<String>();
-		
-		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)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<M>) AccumulationProductSimpleRegular.generate(originalModel, ctx, statesOfInterest);
-		} else if (ctx.accexp.hasBoundExpression()) {
-			product = (AccumulationProductSimpleCounting<M>) 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<M,?>)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");
 		}
 	}
 }