diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index f30877ac..381e2e1a 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/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; diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index e8a4174b..fbb5d887 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/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. */ diff --git a/prism/src/explicit/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index 40a4ce7e..3b3ecac5 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/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. diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index f034f742..95c5d6fc 100644 --- a/prism/src/prism/PrismCL.java +++ b/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."); }