From 327952ab5268fa1b709a5aa9455c5a7828087c55 Mon Sep 17 00:00:00 2001
From: Sascha Wunderlich <sascha.wunderlich@tu-dresden.de>
Date: Tue, 15 Nov 2016 12:52:31 +0100
Subject: [PATCH] accumulation: some fixes

* use Dottable interface
* rewrite the way tracks and their goodness are updated
---
 prism/src/explicit/AccumulationProduct.java   | 57 +++++++------------
 .../explicit/AccumulationProductRegular.java  |  1 +
 prism/src/explicit/AccumulationState.java     |  1 +
 3 files changed, 24 insertions(+), 35 deletions(-)

diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java
index 112ef195..46adf7c6 100644
--- a/prism/src/explicit/AccumulationProduct.java
+++ b/prism/src/explicit/AccumulationProduct.java
@@ -9,8 +9,8 @@ import parser.ast.AccumulationFactor;
 import parser.ast.ExpressionAccumulation;
 import prism.IntegerBound;
 import prism.PrismException;
-import prism.PrismFileLog;
-import prism.PrismLog;
+
+import common.Dottable;
 
 /**
  * An AccumulationProduct has ProductStates, where the first component is the
@@ -22,7 +22,7 @@ import prism.PrismLog;
  * @param <M>
  */
 
-public abstract class AccumulationProduct<M extends Model,Component> extends ProductWithProductStates<M>
+public abstract class AccumulationProduct<M extends Model,Component> extends ProductWithProductStates<M> implements Dottable
 {
 	final StoragePool<AccumulationTracker<Component>> trackers;
 	final StoragePool<AccumulationState<Component>> accStates;
@@ -113,69 +113,56 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 		ArrayList<AccumulationTrack<Component>> oldTracks = oldTracker.getTracks();
 		
 		BitSet oldGoodTracks = accstate.getGoodTracks();
-		BitSet newGoodTracks = (BitSet) oldGoodTracks.clone();
+		BitSet newGoodTracks = new BitSet();
 		
 		// This restart will be...
 		int newLastRestartNr = accstate.getNextRestartNr();
 		//mc.getLog().print(newLastRestartNr);
 		
-		// Build the new tracks.
+		// Build the new tracks and determine their goodness;
 		ArrayList<AccumulationTrack<Component>> newTracks = new ArrayList<>();
 		
 		int trackNr = 0;
 		for(AccumulationTrack<Component> oldTrack : oldTracks) {
+			
 			AccumulationTrack<Component> newTrack;
+			boolean oldTrackGood = oldGoodTracks.get(trackNr);
+			boolean newTrackGood;
 			
 			// restart or advance
 			if(trackNr == newLastRestartNr) {
-				//assert oldTrack == null : "Track " + newLastRestartNr + " is not null!";
+				// If we have a restart, we produce an initial track and reset its goodness.
 				newTrack = new AccumulationTrack<Component>(numberOfWeights, getInitialComponent());
-				newGoodTracks.clear(trackNr);
-			} else if (oldTrack == null) {
-				newTrack = null;
-			} else if (oldGoodTracks.get(trackNr)) {
+				newTrackGood = false;
+			} else if (oldTrackGood || oldTrack == null) {
+				// If the old track is already good or undefined, the new track is as well. Goodness indicators stay.
 				newTrack = null;
+				newTrackGood = oldTrackGood;
 			} else {
+				// Otherwise, the track is defined and not good yet.
 				assert oldTrack != null;
 				newTrack = updateTrack(modelFromStateId, oldTrack, accexp, weights, mc);
+				newTrackGood = isGoodTrack(newTrack, accexp, mc);
 			}
 			
-			// check whether the track is good
-			if(oldGoodTracks.get(trackNr) || isGoodTrack(newTrack,accexp,mc)) {
-				newGoodTracks.set(trackNr);
+			// if the new track is good, we can forget about its contents and set the new goodness
+			if(newTrackGood) {
 				newTrack = null;
-			}
+				newGoodTracks.set(trackNr);
+			};
 			
 			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);
 		
 		return new AccumulationState<>(newTrackerId, newLastRestartNr, numberOfTracks, newGoodTracks);
 	}
 	
-	public void exportToDotFile(String filename) throws PrismException {
-		try (PrismFileLog log = PrismFileLog.create(filename)) {
-			exportToDotFile(log);
-		}
-	}
-	
-	public void exportToDotFile(PrismLog out) {
-		out.print(toDot());
-	}
-	
-	public String quoteForDot(String original) {
-		String result = original;
-		result = result.replaceAll("&", "&amp;");
-		result = result.replaceAll("<", "&lt;");
-		result = result.replaceAll(">", "&gt;");
-		return result;
-	}
-	
+	@Override
 	public String toDot() {
 		StringBuffer result = new StringBuffer();
 		
@@ -194,7 +181,7 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 					+ "</TR><TR>"
 					+ "<TD>" + accState	+ "</TD>"
 					+ "</TR><TR>"
-					+ "<TD>\"" + quoteForDot(tracker.toString()) + "\"</TD>"
+					+ "<TD>\"" + Dottable.quoteForDot(tracker.toString()) + "\"</TD>"
 					+ "</TR>"
 					+ " </TABLE> >]\n");
 			
diff --git a/prism/src/explicit/AccumulationProductRegular.java b/prism/src/explicit/AccumulationProductRegular.java
index a5214a74..18913919 100644
--- a/prism/src/explicit/AccumulationProductRegular.java
+++ b/prism/src/explicit/AccumulationProductRegular.java
@@ -127,6 +127,7 @@ public class AccumulationProductRegular<M extends Model> extends AccumulationPro
 				
 				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;
 				}
diff --git a/prism/src/explicit/AccumulationState.java b/prism/src/explicit/AccumulationState.java
index 108b47a1..82365044 100644
--- a/prism/src/explicit/AccumulationState.java
+++ b/prism/src/explicit/AccumulationState.java
@@ -58,6 +58,7 @@ public class AccumulationState<Component> {
 		return result;
 	}
 
+	@SuppressWarnings("rawtypes")
 	@Override
 	public boolean equals(Object obj) {
 		if (this == obj)