diff --git a/prism/src/explicit/FastAdaptiveUniformisation.java b/prism/src/explicit/FastAdaptiveUniformisation.java index a50d9036..b64c3cf3 100644 --- a/prism/src/explicit/FastAdaptiveUniformisation.java +++ b/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); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 7176b167..1ab6dded 100644 --- a/prism/src/prism/Prism.java +++ b/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()) {