fix for fau

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

prism/src/explicit/FastAdaptiveUniformisation.java

@@ -28,7 +28,10 @@
 
 package explicit;
 
+import java.io.BufferedReader;
 import java.io.File;
+import java.io.FileReader;
+import java.io.IOException;
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.HashMap;
@@ -37,15 +40,20 @@ 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;
 
 /*
  * TODO
@@ -597,13 +605,60 @@ public class FastAdaptiveUniformisation extends PrismComponent
 	 * If null, start from initial state (or uniform distribution over multiple initial states).
 	 * @param t Time point
 	 * @param initDistFile File containing initial distribution
+	 * @param currentModel 
 	 */
-	public StateValues doTransient(double t, File initDistFile) throws PrismException
+	public StateValues doTransient(double t, File initDistFile, Model model)
+			throws PrismException
 	{
 		StateValues initDist = null;
+		if (initDistFile != null) {
+			int numValues = countNumStates(initDistFile);
+			initDist = new StateValues(TypeDouble.getInstance(), numValues);
+			initDist.readFromFile(initDistFile);
+		}
 		return doTransient(t, initDist);
 	}
 
+	/**
+	 * Counts number of states in a file.
+	 * We need this function because the functions to read values into
+	 * StateValues object expect that these objects have been initialised with
+	 * the right number of states.
+	 * 
+	 * @param file file to count states of
+	 * @return number of states in file
+	 * @throws PrismException thrown in case of I/O errors
+	 */
+	private int countNumStates(File file) throws PrismException {
+		BufferedReader in;
+		String s;
+		int lineNum = 0, count = 0;
+
+		try {
+			// open file for reading
+			in = new BufferedReader(new FileReader(file));
+			// read remaining lines
+			s = in.readLine();
+			lineNum++;
+			while (s != null) {
+				s = s.trim();
+				if (!("".equals(s))) {
+					count++;
+				}
+				s = in.readLine();
+				lineNum++;
+			}
+			// close file
+			in.close();
+		} catch (IOException e) {
+			throw new PrismException("File I/O error reading from \"" + file + "\"");
+		} catch (NumberFormatException e) {
+			throw new PrismException("Error detected at line " + lineNum + " of file \"" + file + "\"");
+		}
+
+		return count;
+	}
+
 	/**
 	 * Compute transient probability distribution (forwards).
 	 * Use the passed in vector initDist as the initial probability distribution (time 0).
@@ -638,6 +693,10 @@ public class FastAdaptiveUniformisation extends PrismComponent
 		for (int stateNr = 0; stateNr < initDist.size; stateNr++) {
 			State initState = it.next();
 			addToModel(initState);
+		}
+		it = initDist.statesList.listIterator();
+		for (int stateNr = 0; stateNr < initDist.size; stateNr++) {
+			State initState = it.next();
 			computeStateRatesAndRewards(initState);
 			states.get(initState).setProb(values[stateNr]);
 			maxRate = Math.max(maxRate, states.get(initState).sumRates() * 1.02);			

prism/src/prism/Prism.java

@@ -3157,7 +3157,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 			PrismModelExplorer modelExplorer = new PrismModelExplorer(getSimulator(), currentModulesFile);
 			FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, modelExplorer);
 			fau.setConstantValues(currentModulesFile.getConstantValues());
-			probsExpl = fau.doTransient(time, fileIn);
+			probsExpl = fau.doTransient(time, fileIn, currentModel);
 		}
 		// Symbolic
 		else if (!getExplicit()) {
@@ -3261,11 +3261,15 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 
 			// FAU
 			if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) {
-				// For FAU, we don't do computation incrementally
 				PrismModelExplorer modelExplorer = new PrismModelExplorer(getSimulator(), currentModulesFile);
 				FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, modelExplorer);
 				fau.setConstantValues(currentModulesFile.getConstantValues());
-				probsExpl = fau.doTransient(timeDouble, fileIn);
+				if (i == 0) {
+					probsExpl = fau.doTransient(timeDouble, fileIn, currentModel);
+					initTimeDouble = 0.0;
+				} else {
+					probsExpl = fau.doTransient(timeDouble - initTimeDouble, probsExpl);
+				}
 			}
 			// Symbolic
 			else if (!getExplicit()) {