From a50a25480533015442e3515dccfc41407a57cc5c Mon Sep 17 00:00:00 2001
From: Ernst Moritz Hahn <emhahn@cs.ox.ac.uk>
Date: Fri, 22 Aug 2014 03:08:37 +0000
Subject: [PATCH] bugfix fau

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9122 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 .../explicit/FastAdaptiveUniformisation.java  | 26 ++++++++++++++-----
 ...astAdaptiveUniformisationModelChecker.java |  3 ++-
 2 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/prism/src/explicit/FastAdaptiveUniformisation.java b/prism/src/explicit/FastAdaptiveUniformisation.java
index b64c3cf3..eccc8d25 100644
--- a/prism/src/explicit/FastAdaptiveUniformisation.java
+++ b/prism/src/explicit/FastAdaptiveUniformisation.java
@@ -40,17 +40,12 @@ import java.util.LinkedHashMap;
 import java.util.ListIterator;
 import java.util.Map;
 
-import dv.DoubleVector;
-
 import parser.ast.Expression;
 import parser.ast.ExpressionIdent;
 import parser.ast.LabelList;
 import parser.ast.RewardStruct;
-import parser.type.TypeBool;
 import parser.type.TypeDouble;
-import parser.type.TypeInt;
 import parser.Values;
-
 import parser.State;
 import prism.*;
 import prism.Model;
@@ -93,7 +88,7 @@ public class FastAdaptiveUniformisation extends PrismComponent
 	 * (references) and a flag whether the state has a significant probability
 	 * mass (alive).
 	 */
-	private final class StateProp
+	private final static class StateProp
 	{
 		/** current-step probability.
 		 * should contain initial probability before actual analysis is started.
@@ -1113,6 +1108,25 @@ public class FastAdaptiveUniformisation extends PrismComponent
 	{
 		return totalProbLoss;
 	}
+
+	/**
+	 * Sets the probability of sink states to zero.
+	 * @throws PrismException 
+	 */
+	public void clearSinkStates() throws PrismException {
+		for (Map.Entry<State,StateProp> statePair : states.entrySet()) {
+			State state = statePair.getKey();
+			StateProp prop = statePair.getValue();
+			modelExplorer.queryState(state);
+			specialLabels.setLabel(0, modelExplorer.getNumTransitions() == 0 ? Expression.True() : Expression.False());
+			specialLabels.setLabel(1, initStates.contains(state) ? Expression.True() : Expression.False());
+			Expression evSink = sink.deepCopy();
+			evSink = (Expression) evSink.expandLabels(specialLabels);
+			if (evSink.evaluateBoolean(constantValues, state)) {
+				prop.setProb(0.0);
+			}
+		}
+	}
 	
 	/**
 	 * Adds @a state to model.
diff --git a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java b/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java
index 2289995a..43e1e17c 100644
--- a/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java
+++ b/prism/src/explicit/FastAdaptiveUniformisationModelChecker.java
@@ -189,9 +189,10 @@ public class FastAdaptiveUniformisationModelChecker extends PrismComponent
 		default:
 			throw new PrismException("operator currently not supported for fast adaptive uniformisation");
 		}
-		
 		fau.setSink(sink);
 		fau.computeTransientProbsAdaptive(timeLower);
+		fau.clearSinkStates();
+
 		switch (operator) {
 		case ExpressionTemporal.P_U:
 		case ExpressionTemporal.P_F: