diff --git a/prism/src/explicit/FastAdaptiveUniformisation.java b/prism/src/explicit/FastAdaptiveUniformisation.java index b47c1f59..771cdb7c 100644 --- a/prism/src/explicit/FastAdaptiveUniformisation.java +++ b/prism/src/explicit/FastAdaptiveUniformisation.java @@ -72,12 +72,9 @@ import prism.*; */ /** - * Implementation of fast adaptive uniformisation - * @author Dave Parker (University of Oxford) - * @author Frits Dannenberg (University of Oxford) - * @author Ernst Moritz Hahn (University of Oxford) + * Implementation of fast adaptive uniformisation (FAU). */ -public class FastAdaptiveUniformisation +public class FastAdaptiveUniformisation extends PrismComponent { /** * Stores properties of states needed for fast adaptive method. @@ -87,8 +84,6 @@ public class FastAdaptiveUniformisation * states and the rates to them, the number of incoming transitions * (references) and a flag whether the state has a significant probability * mass (alive). - * - * @author Ernst Moritz Hahn (University of Oxford) */ private final class StateProp { @@ -410,8 +405,6 @@ public class FastAdaptiveUniformisation REW_CUMUL } - /** PRISM settings to read analysis parameters from */ - private PrismSettings settings = null; /** model exploration component to generate new states */ private ModelExplorer modelExplorer; /** probability allowed to drop birth process */ @@ -466,11 +459,12 @@ public class FastAdaptiveUniformisation /** * Constructor. */ - public FastAdaptiveUniformisation(PrismSettings settings, ModelExplorer modelExplorer) throws PrismException + public FastAdaptiveUniformisation(PrismComponent parent, ModelExplorer modelExplorer) throws PrismException { - maxNumStates = 0; - this.settings = settings; + super(parent); + this.modelExplorer = modelExplorer; + maxNumStates = 0; termCritParam = settings.getDouble(PrismSettings.PRISM_TERM_CRIT_PARAM); delta = settings.getDouble(PrismSettings.PRISM_FAU_DELTA); @@ -621,6 +615,8 @@ public class FastAdaptiveUniformisation */ public StateValues doTransient(double time, StateValues initDist) throws PrismException { + mainLog.println("\nComputing probabilities (fast adaptive uniformisation)..."); + if (initDist == null) { initDist = new StateValues(); initDist.type = TypeDouble.getInstance(); @@ -665,6 +661,10 @@ public class FastAdaptiveUniformisation probs.size = probsArr.length; probs.valuesD = probsArr; probs.statesList = statesList; + + mainLog.println("\nTotal probability lost is : " + getTotalDiscreteLoss()); + mainLog.println("Maximal number of states stored during analysis : " + getMaxNumStates()); + return probs; } diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 798af5db..f6bcf544 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3054,12 +3054,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) { PrismModelExplorer modelExplorer = new PrismModelExplorer(getSimulator(), currentModulesFile); - FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(settings, modelExplorer); + FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, modelExplorer); fau.setConstantValues(currentModulesFile.getConstantValues()); - mainLog.println("Starting transient probability computation using fast adaptive uniformisation..."); probsExpl = fau.doTransient(time, fileIn); - mainLog.println("\nTotal probability lost is : " + fau.getTotalDiscreteLoss()); - mainLog.println("Maximal number of states stored during analysis : " + fau.getMaxNumStates()); } else if (!getExplicit()) { if (currentModelType == ModelType.DTMC) { mc = new ProbModelChecker(this, currentModel, null);