Add DTMC transient probability computation for explicit engine.

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

prism/src/explicit/DTMCModelChecker.java

@@ -40,7 +40,6 @@ import prism.Prism;
 import prism.PrismComponent;
 import prism.PrismException;
 import prism.PrismFileLog;
-import prism.PrismNotSupportedException;
 import prism.PrismUtils;
 import acceptance.AcceptanceReach;
 import acceptance.AcceptanceType;
@@ -398,6 +397,29 @@ public class DTMCModelChecker extends ProbModelChecker
 		return StateValues.createFromDoubleArray(res.soln, dtmc);
 	}
 
+	/**
+	 * Compute transient probability distribution (forwards).
+	 * Start from initial state (or uniform distribution over multiple initial states).
+	 */
+	public StateValues doTransient(DTMC dtmc, int k) throws PrismException
+	{
+		return doTransient(dtmc, k, (StateValues) null);
+	}
+
+	/**
+	 * Compute transient probability distribution (forwards).
+	 * Optionally, use the passed in file initDistFile to give the initial probability distribution (time 0).
+	 * If null, start from initial state (or uniform distribution over multiple initial states).
+	 * @param dtmc The DTMC
+	 * @param k Time step
+	 * @param initDistFile File containing initial distribution
+	 */
+	public StateValues doTransient(DTMC dtmc, int k, File initDistFile) throws PrismException
+	{
+		StateValues initDist = readDistributionFromFile(initDistFile, dtmc);
+		return doTransient(dtmc, k, initDist);
+	}
+
 	/**
 	 * Compute transient probability distribution (forwards).
 	 * Optionally, use the passed in vector initDist as the initial probability distribution (time step 0).
@@ -408,9 +430,11 @@ public class DTMCModelChecker extends ProbModelChecker
 	 * @param k Time step
 	 * @param initDist Initial distribution (will be overwritten)
 	 */
-	public StateValues doTransient(DTMC dtmc, int k, double initDist[]) throws PrismException
+	public StateValues doTransient(DTMC dtmc, int k, StateValues initDist) throws PrismException
 	{
-		throw new PrismNotSupportedException("Not implemented yet");
+		StateValues initDistNew = (initDist == null) ? buildInitialDistribution(dtmc) : initDist;
+		ModelCheckerResult res = computeTransientProbs(dtmc, k, initDistNew.getDoubleArray());
+		return StateValues.createFromDoubleArray(res.soln, dtmc);
 	}
 
 	// Numerical computation functions
@@ -1600,7 +1624,44 @@ public class DTMCModelChecker extends ProbModelChecker
 	 */
 	public ModelCheckerResult computeTransientProbs(DTMC dtmc, int k, double initDist[]) throws PrismException
 	{
-		throw new PrismNotSupportedException("Not implemented yet");
+		ModelCheckerResult res;
+		int n, iters;
+		double soln[], soln2[], tmpsoln[];
+		long timer;
+
+		// Start transient probability computation
+		timer = System.currentTimeMillis();
+		mainLog.println("Starting transient probability computation...");
+
+		// Store num states
+		n = dtmc.getNumStates();
+
+		// Create solution vector(s)
+		// Use the passed in vector, if present
+		soln = initDist;
+		soln2 = new double[n];
+
+		// Start iterations
+		for (iters = 0; iters < k; iters++) {
+			// Matrix-vector multiply
+			dtmc.vmMult(soln, soln2);
+			// Swap vectors for next iter
+			tmpsoln = soln;
+			soln = soln2;
+			soln2 = tmpsoln;
+		}
+
+		// Finished transient probability computation
+		timer = System.currentTimeMillis() - timer;
+		mainLog.print("Transient probability computation");
+		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;
 	}
 
 	/**

prism/src/prism/Prism.java

@@ -3382,7 +3382,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 		else {
 			buildModelIfRequired();
 			if (currentModelType == ModelType.DTMC) {
-				throw new PrismException("Not implemented yet");
+				DTMCModelChecker mcDTMC = new DTMCModelChecker(this);
+				probsExpl = mcDTMC.doTransient((DTMC) currentModelExpl, (int) time, fileIn);
 			} else if (currentModelType == ModelType.CTMC) {
 				CTMCModelChecker mcCTMC = new CTMCModelChecker(this);
 				probsExpl = mcCTMC.doTransient((CTMC) currentModelExpl, time, fileIn);
@@ -3509,7 +3510,12 @@ public class Prism extends PrismComponent implements PrismSettingsListener
 					}
 					probsExpl = mc.doTransient((CTMC) currentModelExpl, timeDouble - initTimeDouble, initDistExpl);
 				} else {
-					throw new PrismException("Not implemented yet");
+					DTMCModelChecker mc = new DTMCModelChecker(this);
+					if (i == 0) {
+						initDistExpl = mc.readDistributionFromFile(fileIn, currentModelExpl);
+						initTimeInt = 0;
+					}
+					probsExpl = mc.doTransient((DTMC) currentModelExpl, timeInt - initTimeInt, initDistExpl);
 				}
 			}