Small refactoring of methods to compute steady-state probabilities.

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

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. 

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.