From bb47b0a8198f67d92b521ab580735a1de4996fbd Mon Sep 17 00:00:00 2001
From: Sascha Wunderlich <sascha.wunderlich@tu-dresden.de>
Date: Fri, 21 Dec 2018 18:17:43 +0100
Subject: [PATCH] accumulation: fix simple method

---
 prism/src/explicit/AccumulationProduct.java        | 2 +-
 prism/src/explicit/AccumulationState.java          | 4 ++++
 prism/src/explicit/AccumulationTransformation.java | 4 +++-
 3 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/prism/src/explicit/AccumulationProduct.java b/prism/src/explicit/AccumulationProduct.java
index ee8907c6..c731b338 100644
--- a/prism/src/explicit/AccumulationProduct.java
+++ b/prism/src/explicit/AccumulationProduct.java
@@ -262,7 +262,7 @@ public abstract class AccumulationProduct<M extends Model,Component> extends Pro
 		
 		// If this is a simple Product, we only set the GoalState and return
 		if(ctx.simpleMethod) {
-			goalStates.get(0).set(index, accState.hasGoodTracks());
+			goalStates.get(0).set(index, accState.importantTrackIsGood());
 			return;
 		}
 		
diff --git a/prism/src/explicit/AccumulationState.java b/prism/src/explicit/AccumulationState.java
index 6bd17095..0e0b6742 100644
--- a/prism/src/explicit/AccumulationState.java
+++ b/prism/src/explicit/AccumulationState.java
@@ -48,6 +48,10 @@ public class AccumulationState<Component> {
 		return !goodTracks.isEmpty();
 	}
 	
+	public boolean importantTrackIsGood() {
+		return goodTracks.get(getNextRestartNr());
+	}
+	
 	public BitSet getGoodTracks() {
 		return goodTracks;
 	}
diff --git a/prism/src/explicit/AccumulationTransformation.java b/prism/src/explicit/AccumulationTransformation.java
index f635d82c..fb240ab9 100644
--- a/prism/src/explicit/AccumulationTransformation.java
+++ b/prism/src/explicit/AccumulationTransformation.java
@@ -133,7 +133,9 @@ public class AccumulationTransformation<M extends ModelExplicit> implements Mode
 		// Build the AccumulationContext
 		AccumulationContext ctx = new AccumulationContext(accexp, rewards, mc);
 		ctx.singleTrack  = isSingleTrack && !forceMulti;
-		ctx.simpleMethod = isSimple      && !forceComplex && !forceMulti;
+		ctx.simpleMethod = isSimple      && !forceComplex;
+		
+		mc.getLog().println("Using optimizations single/simple " + ctx.singleTrack + "/" + ctx.simpleMethod);
 		
 		// Build the product
 		clock.start("accumulation product construction");