Partial support for explicit engine DTMC steady-state computation.

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

prism/src/explicit/CTMCModelChecker.java

@@ -148,7 +148,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 		return probs;
 	}
 
-	// Transient/steady-state probability computation
+	// Steady-state/transient probability computation
 
 	/**
 	 * Compute transient probability distribution (forwards).
@@ -156,8 +156,11 @@ public class CTMCModelChecker extends DTMCModelChecker
 	 * If null, start from initial state (or uniform distribution over multiple initial states).
 	 * For reasons of efficiency, when a vector is passed in, it will be trampled over,
 	 * so if you wanted it, take a copy. 
+	 * @param ctmc The CTMC
+	 * @param t Time point
+	 * @param initDist Initial distribution (will be overwritten)
 	 */
-	public StateValues doTransient(CTMC ctmc, double time, double initDist[]) throws PrismException
+	public StateValues doTransient(CTMC ctmc, double t, double initDist[]) throws PrismException
 	{
 		ModelCheckerResult res = null;
 		int n;
@@ -179,7 +182,7 @@ public class CTMCModelChecker extends DTMCModelChecker
 		}
 
 		// Compute transient probabilities
-		res = computeTransientProbs(ctmc, initDistNew, time);
+		res = computeTransientProbs(ctmc, t, initDistNew);
 		probs = StateValues.createFromDoubleArray(res.soln);
 
 		return probs;
@@ -386,10 +389,10 @@ public class CTMCModelChecker extends DTMCModelChecker
 	 * For space efficiency, the initial distribution vector will be modified and values over-written,  
 	 * so if you wanted it, take a copy. 
 	 * @param ctmc The CTMC
-	 * @param initDist Initial distribution (will be overwritten)
 	 * @param t Time point
+	 * @param initDist Initial distribution (will be overwritten)
 	 */
-	public ModelCheckerResult computeTransientProbs(CTMC ctmc, double initDist[], double t) throws PrismException
+	public ModelCheckerResult computeTransientProbs(CTMC ctmc, double t, double initDist[]) throws PrismException
 	{
 		ModelCheckerResult res = null;
 		int i, n, iters;

prism/src/explicit/DTMCModelChecker.java

@@ -192,6 +192,62 @@ public class DTMCModelChecker extends ProbModelChecker
 		return rewards;
 	}
 
+	// Steady-state/transient probability computation
+
+	/**
+	 * Compute steady-state probability distribution (forwards).
+	 * Optionally, use the passed in vector initDist as the initial probability distribution (time step 0).
+	 * If null, start from initial state (or uniform distribution over multiple initial states).
+	 * For reasons of efficiency, when a vector is passed in, it will be trampled over,
+	 * so if you wanted it, take a copy. 
+	 * @param dtmc The DTMC
+	 * @param initDist Initial distribution (will be overwritten)
+	 */
+	public StateValues doSteadyState(DTMC dtmc, double initDist[]) throws PrismException
+	{
+		ModelCheckerResult res = null;
+		int n;
+		double initDistNew[] = null;
+		StateValues probs = null;
+
+		// TODO: BSCC computation
+		
+		// Store num states
+		n = dtmc.getNumStates();
+
+		// Build initial distribution (if not specified)
+		if (initDist == null) {
+			initDistNew = new double[n];
+			for (int in : dtmc.getInitialStates()) {
+				initDistNew[in] = 1 / dtmc.getNumInitialStates();
+			}
+		} else {
+			initDistNew = initDist;
+			throw new PrismException("Not implemented yet"); // TODO
+		}
+
+		// Compute transient probabilities
+		res = computeSteadyStateProbs(dtmc, initDistNew);
+		probs = StateValues.createFromDoubleArray(res.soln);
+
+		return probs;
+	}
+	
+	/**
+	 * Compute transient probability distribution (forwards).
+	 * Optionally, use the passed in vector initDist as the initial probability distribution (time step 0).
+	 * If null, start from initial state (or uniform distribution over multiple initial states).
+	 * For reasons of efficiency, when a vector is passed in, it will be trampled over,
+	 * so if you wanted it, take a copy. 
+	 * @param dtmc The DTMC
+	 * @param k Time step
+	 * @param initDist Initial distribution (will be overwritten)
+	 */
+	public StateValues doTransient(DTMC dtmc, int k, double initDist[]) throws PrismException
+	{
+		throw new PrismException("Not implemented yet");
+	}
+	
 	// Numerical computation functions
 
 	/**
@@ -871,6 +927,81 @@ public class DTMCModelChecker extends ProbModelChecker
 		return res;
 	}
 
+	/**
+	 * Compute steady-state probabilities
+	 * i.e. compute the long-run probability of being in each state,
+	 * assuming the initial distribution {@code initDist}. 
+	 * For space efficiency, the initial distribution vector will be modified and values over-written,  
+	 * so if you wanted it, take a copy. 
+	 * @param dtmc The DTMC
+	 * @param initDist Initial distribution (will be overwritten)
+	 */
+	public ModelCheckerResult computeSteadyStateProbs(DTMC dtmc, double initDist[]) throws PrismException
+	{
+		ModelCheckerResult res;
+		int n, iters;
+		double soln[], soln2[], tmpsoln[];
+		boolean done;
+		long timer;
+
+		// Start value iteration
+		timer = System.currentTimeMillis();
+		mainLog.println("Starting value iteration...");
+
+		// Store num states
+		n = dtmc.getNumStates();
+
+		// Create solution vector(s)
+		// For soln, we just use init (since we are free to modify this vector)
+		soln = initDist;
+		soln2 = new double[n];
+		
+		// No need to initialise solution vectors
+		// (soln is done, soln2 will be immediately overwritten)
+
+		// Start iterations
+		iters = 0;
+		done = false;
+		while (!done && iters < maxIters) {
+			iters++;
+			// Matrix-vector multiply
+			dtmc.vmMult(soln, soln2);
+			// Check termination
+			done = PrismUtils.doublesAreClose(soln, soln2, termCritParam, termCrit == TermCrit.ABSOLUTE);
+			// Swap vectors for next iter
+			tmpsoln = soln;
+			soln = soln2;
+			soln2 = tmpsoln;
+		}
+
+		// Finished value iteration
+		timer = System.currentTimeMillis() - timer;
+		mainLog.print("Value iteration");
+		mainLog.println(" took " + iters + " iterations and " + timer / 1000.0 + " seconds.");
+
+		// Return results
+		res = new ModelCheckerResult();
+		res.soln = soln;
+		res.numIters = iters;
+		res.timeTaken = timer / 1000.0;
+		return res;
+	}
+	
+	/**
+	 * Compute transient probabilities
+	 * i.e. compute the probability of being in each state at time step {@code k},
+	 * assuming the initial distribution {@code initDist}. 
+	 * For space efficiency, the initial distribution vector will be modified and values over-written,  
+	 * so if you wanted it, take a copy. 
+	 * @param dtmc The DTMC
+	 * @param k Time step
+	 * @param initDist Initial distribution (will be overwritten)
+	 */
+	public ModelCheckerResult computeTransientProbs(DTMC dtmc, int k, double initDist[]) throws PrismException
+	{
+		throw new PrismException("Not implemented yet");
+	}
+	
 	/**
 	 * Simple test program.
 	 */

prism/src/explicit/PrismExplicit.java

@@ -169,6 +169,77 @@ public class PrismExplicit
 		return result;
 	}
 
+	/**
+	 * Compute steady-state probabilities (for a DTMC or CTMC).
+	 * Output probability distribution to log. 
+	 */
+	public void doSteadyState(Model model) throws PrismException
+	{
+		doSteadyState(model, Prism.EXPORT_PLAIN, null);
+	}
+	
+	/**
+	 * Compute steady-state probabilities (for a DTMC or CTMC).
+	 * Output probability distribution to a file (or, if file is null, to log). 
+	 * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB.
+	 */
+	public void doSteadyState(Model model, int exportType, File fileOut) throws PrismException
+	{
+		long l = 0; // timer
+		StateValues probs = null;
+		PrismLog tmpLog;
+		
+		// no specific states format for MRMC
+		if (exportType == Prism.EXPORT_MRMC) exportType = Prism.EXPORT_PLAIN;
+		// rows format does not apply to states output
+		if (exportType == Prism.EXPORT_ROWS) exportType = Prism.EXPORT_PLAIN;
+		
+		mainLog.println("\nComputing steady-state probabilities...");
+		l = System.currentTimeMillis();
+
+		if (model.getModelType() == ModelType.DTMC) {
+			DTMCModelChecker mcDTMC = new DTMCModelChecker();
+			// TODO: pass settings
+			probs = mcDTMC.doSteadyState((DTMC) model, null);
+		}
+		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");
+		}
+		
+		l = System.currentTimeMillis() - l;
+		
+		// print message
+		mainLog.print("\nPrinting steady-state probabilities ");
+		switch (exportType) {
+		case Prism.EXPORT_PLAIN: mainLog.print("in plain text format "); break;
+		case Prism.EXPORT_MATLAB: mainLog.print("in Matlab format "); break;
+		}
+		if (fileOut != null) mainLog.println("to file \"" + fileOut + "\"..."); else mainLog.println("below:");
+		
+		// create new file log or use main log
+		if (fileOut != null) {
+			tmpLog = new PrismFileLog(fileOut.getPath());
+			if (!tmpLog.ready()) {
+				throw new PrismException("Could not open file \"" + fileOut + "\" for output");
+			}
+		} else {
+			tmpLog = mainLog;
+		}
+		
+		// print out or export probabilities
+		probs.print(tmpLog, fileOut == null, exportType == Prism.EXPORT_MATLAB, fileOut == null);
+		
+		// print out computation time
+		mainLog.println("\nTime for steady-state probability computation: " + l/1000.0 + " seconds.");
+		
+		// tidy up
+		probs.clear();
+		if (fileOut != null) tmpLog.close();
+	}
+	
 	/**
 	 * Compute transient probabilities (for a DTMC or CTMC).
 	 * Output probability distribution to log. 

prism/src/prism/PrismCL.java

@@ -936,7 +936,11 @@ public class PrismCL
 		
 		// compute steady-state probabilities
 		if (modelType == ModelType.CTMC || modelType == ModelType.DTMC) {
-			prism.doSteadyState(model, exportType, exportSteadyStateFile);
+			if (explicit) {
+				prismExpl.doSteadyState(modelExpl, exportType, exportSteadyStateFile);
+			} else {
+				prism.doSteadyState(model, exportType, exportSteadyStateFile);
+			}
 		} else {
 			mainLog.println("\nWarning: Steady-state probabilities only computed for DTMCs/CTMCs.");
 		}