bugfix fau

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9122 bbc10eb1-c90d-0410-af57-cb519fbb1720

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.

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: