diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index 23acbc32..f4a24c43 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -26,10 +26,9 @@ package explicit; +import java.io.File; import java.util.*; -import jdd.JDD; - import explicit.rewards.MCRewards; import explicit.rewards.StateRewardsArray; import parser.ast.*; @@ -150,6 +149,38 @@ public class CTMCModelChecker extends DTMCModelChecker // Steady-state/transient probability computation + /** + * Compute transient probability distribution (forwards). + * Start from initial state (or uniform distribution over multiple initial states). + */ + public StateValues doTransient(CTMC ctmc, double time) throws PrismException + { + return doTransient(ctmc, time, (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 ctmc The CTMC + * @param t Time point + * @param initDistFile File containing initial distribution + */ + public StateValues doTransient(CTMC ctmc, double t, File initDistFile) throws PrismException + { + StateValues initDist = null; + + if (initDistFile != null) { + mainLog.println("\nImporting initial probability distribution from file \"" + initDistFile + "\"..."); + // Build an empty vector + initDist = new StateValues(TypeDouble.getInstance(), ctmc); + // Populate vector from file + initDist.readFromFile(initDistFile); + } + + return doTransient(ctmc, t, initDist); + } + /** * Compute transient probability distribution (forwards). * Optionally, use the passed in vector initDist as the initial probability distribution (time 0). @@ -160,29 +191,24 @@ public class CTMCModelChecker extends DTMCModelChecker * @param t Time point * @param initDist Initial distribution (will be overwritten) */ - public StateValues doTransient(CTMC ctmc, double t, double initDist[]) throws PrismException + public StateValues doTransient(CTMC ctmc, double t, StateValues initDist) throws PrismException { ModelCheckerResult res = null; - int n; - double initDistNew[] = null; - StateValues probs = null; - - // Store num states - n = ctmc.getNumStates(); + StateValues initDistNew = null, probs = null; // Build initial distribution (if not specified) if (initDist == null) { - initDistNew = new double[n]; + initDistNew = new StateValues(TypeDouble.getInstance(), new Double(0.0), ctmc); + double initVal = 1.0 / ctmc.getNumInitialStates(); for (int in : ctmc.getInitialStates()) { - initDistNew[in] = 1 / ctmc.getNumInitialStates(); + initDistNew.setDoubleValue(in, initVal); } } else { initDistNew = initDist; - throw new PrismException("Not implemented yet"); // TODO } // Compute transient probabilities - res = computeTransientProbs(ctmc, t, initDistNew); + res = computeTransientProbs(ctmc, t, initDistNew.getDoubleArray()); probs = StateValues.createFromDoubleArray(res.soln, ctmc); return probs; diff --git a/prism/src/explicit/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index d4a4978c..5a64bf8f 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/prism/src/explicit/PrismExplicit.java @@ -344,7 +344,7 @@ public class PrismExplicit CTMCModelChecker mcCTMC = new CTMCModelChecker(); mcCTMC.setLog(mainLog); mcCTMC.setSettings(settings); - probs = mcCTMC.doTransient((CTMC) model, time, null); + probs = mcCTMC.doTransient((CTMC) model, time, fileIn); } else { throw new PrismException("Transient probabilities only computed for DTMCs/CTMCs"); @@ -371,7 +371,7 @@ public class PrismExplicit } // print out or export probabilities - probs.print(tmpLog, fileOut == null, exportType == Prism.EXPORT_MATLAB, fileOut == null, true); + probs.print(tmpLog, fileOut == null, exportType == Prism.EXPORT_MATLAB, fileOut == null, fileOut == null); // print out computation time mainLog.println("\nTime for transient probability computation: " + l/1000.0 + " seconds.");