diff --git a/prism/src/explicit/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index 2cc0ca3c..cb681014 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/prism/src/explicit/PrismExplicit.java @@ -257,18 +257,7 @@ public class PrismExplicit extends PrismComponent mainLog.println("\nComputing steady-state probabilities..."); l = System.currentTimeMillis(); - - if (model.getModelType() == ModelType.DTMC) { - DTMCModelChecker mcDTMC = new DTMCModelChecker(this); - probs = mcDTMC.doSteadyState((DTMC) model); - } - else if (model.getModelType() == ModelType.CTMC) { - throw new PrismException("Not implemented yet"); // TODO - } - else { - throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); - } - + probs = computeSteadyStateProbabilities(model); l = System.currentTimeMillis() - l; // print message @@ -299,7 +288,27 @@ public class PrismExplicit extends PrismComponent probs.clear(); if (fileOut != null) tmpLog.close(); } - + + /** + * Compute steady-state probabilities (for a DTMC or CTMC). + * Start from initial state or a uniform distribution over multiple initial states. + */ + public StateValues computeSteadyStateProbabilities(Model model) throws PrismException + { + StateValues probs; + if (model.getModelType() == ModelType.DTMC) { + DTMCModelChecker mcDTMC = new DTMCModelChecker(this); + probs = mcDTMC.doSteadyState((DTMC) model); + } + else if (model.getModelType() == ModelType.CTMC) { + throw new PrismException("Not implemented yet"); // TODO + } + else { + throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); + } + return probs; + } + /** * Compute transient probabilities (for a DTMC or CTMC). * Output probability distribution to log. diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index b0abae84..bf8b0fe0 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3062,7 +3062,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener public void doSteadyState(int exportType, File fileOut, File fileIn) throws PrismException { long l = 0; // timer - ModelChecker mc = null; StateValues probs = null; explicit.StateValues probsExpl = null; PrismLog tmpLog; @@ -3086,29 +3085,11 @@ public class Prism extends PrismComponent implements PrismSettingsListener buildModelIfRequired(); l = System.currentTimeMillis(); - if (!getExplicit()) { - if (currentModel.getModelType() == ModelType.DTMC) { - mc = new ProbModelChecker(this, currentModel, null); - probs = ((ProbModelChecker) mc).doSteadyState(fileIn); - } else if (currentModel.getModelType() == ModelType.CTMC) { - mc = new StochModelChecker(this, currentModel, null); - probs = ((StochModelChecker) mc).doSteadyState(fileIn); - } else { - throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); - } + probs = computeSteadyStateProbabilities(currentModel, fileIn); } else { - if (currentModelExpl.getModelType() == ModelType.DTMC) { - DTMCModelChecker mcDTMC = new DTMCModelChecker(this); - probsExpl = mcDTMC.doSteadyState((DTMC) currentModelExpl, (File) null); - //TODO: probsExpl = mcDTMC.doSteadyState((DTMC) currentModelExpl, fileIn); - } else if (currentModelType == ModelType.CTMC) { - throw new PrismException("Not implemented yet"); - } else { - throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); - } + probsExpl = computeSteadyStateProbabilitiesExplicit(currentModelExpl, fileIn); } - l = System.currentTimeMillis() - l; // print message @@ -3137,6 +3118,47 @@ public class Prism extends PrismComponent implements PrismSettingsListener tmpLog.close(); } + /** + * Compute steady-state probabilities (for a DTMC or CTMC) using symbolic engines. + * Optionally (if non-null), read in the initial probability distribution from a file. + * If null, start from initial state (or uniform distribution over multiple initial states). + */ + protected StateValues computeSteadyStateProbabilities(Model model, File fileIn) throws PrismException + { + ProbModelChecker mc; + if (model.getModelType() == ModelType.DTMC) { + mc = new ProbModelChecker(this, model, null); + } + else if (model.getModelType() == ModelType.CTMC) { + mc = new StochModelChecker(this, model, null); + } + else { + throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); + } + return mc.doSteadyState(fileIn); + } + + /** + * Compute steady-state probabilities (for a DTMC or CTMC) using the explicit engine. + * Optionally (if non-null), read in the initial probability distribution from a file. + * If null, start from initial state (or uniform distribution over multiple initial states). + */ + protected explicit.StateValues computeSteadyStateProbabilitiesExplicit(explicit.Model model, File fileIn) throws PrismException + { + DTMCModelChecker mcDTMC; + explicit.StateValues probs; + if (model.getModelType() == ModelType.DTMC) { + mcDTMC = new DTMCModelChecker(this); + //TODO: probs = mcDTMC.doSteadyState((DTMC) model, fileIn); + probs = mcDTMC.doSteadyState((DTMC) model, (File) null); + } else if (model.getModelType() == ModelType.CTMC) { + throw new PrismException("Not implemented yet"); + } else { + throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); + } + return probs; + } + /** * Compute transient probabilities (forwards) for the current model (DTMCs/CTMCs only). * Output probability distribution to log.