From ab831c8a6cd54b054e977350610fbb65963e3ef1 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 11 Aug 2012 09:53:51 +0000 Subject: [PATCH] Allow -importinitdist for steady-state (as well as transient). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5545 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Prism.java | 28 +++++++++++++++------------- prism/src/prism/PrismCL.java | 2 +- 2 files changed, 16 insertions(+), 14 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 984753ca..1056c7a2 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -2570,15 +2570,16 @@ public class Prism implements PrismSettingsListener */ public void doSteadyState() throws PrismException { - doSteadyState(EXPORT_PLAIN, null); + doSteadyState(EXPORT_PLAIN, null, null); } /** * Compute steady-state probabilities for the current model (DTMCs/CTMCs only). - * Output probability distribution to a file (or, if file is null, to log). + * Output probability distribution to a file (or, if {@code fileOut} is null, to log). * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB. + * Optionally (if non-null), read in the initial probability distribution from a file. */ - public void doSteadyState(int exportType, File file) throws PrismException + public void doSteadyState(int exportType, File fileOut, File fileIn) throws PrismException { long l = 0; // timer ModelChecker mc = null; @@ -2589,7 +2590,7 @@ public class Prism implements PrismSettingsListener if (!(currentModelType == ModelType.CTMC || currentModelType == ModelType.DTMC)) throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); - if (file != null && getEngine() == MTBDD) + if (fileOut != null && getEngine() == MTBDD) throw new PrismException("Steady-state probability export not supported for MTBDD engine"); // TODO: auto-switch? @@ -2611,10 +2612,10 @@ public class Prism implements PrismSettingsListener if (!getExplicit()) { if (currentModel.getModelType() == ModelType.DTMC) { mc = new ProbModelChecker(this, currentModel, null); - probs = ((ProbModelChecker) mc).doSteadyState(); + probs = ((ProbModelChecker) mc).doSteadyState(fileIn); } else if (currentModel.getModelType() == ModelType.CTMC) { mc = new StochModelChecker(this, currentModel, null); - probs = ((StochModelChecker) mc).doSteadyState(); + probs = ((StochModelChecker) mc).doSteadyState(fileIn); } else { throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); } @@ -2623,6 +2624,7 @@ public class Prism implements PrismSettingsListener DTMCModelChecker mcDTMC = new DTMCModelChecker(); mcDTMC.setLog(mainLog); mcDTMC.setSettings(settings); + // TODO: pass in init dist file probsExpl = mcDTMC.doSteadyState((DTMC) currentModelExpl, null); } else if (currentModelType == ModelType.CTMC) { throw new PrismException("Not implemented yet"); @@ -2636,16 +2638,16 @@ public class Prism implements PrismSettingsListener // print message mainLog.print("\nPrinting steady-state probabilities "); mainLog.print(getStringForExportType(exportType) + " "); - mainLog.println(getDestinationStringForFile(file)); + mainLog.println(getDestinationStringForFile(fileOut)); // create new file log or use main log - tmpLog = getPrismLogForFile(file); + tmpLog = getPrismLogForFile(fileOut); // print out or export probabilities if (!getExplicit()) - probs.print(tmpLog, file == null, exportType == EXPORT_MATLAB, file == null); + probs.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null); else - probsExpl.print(tmpLog, file == null, exportType == EXPORT_MATLAB, file == null, true); + probsExpl.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null, true); // print out computation time mainLog.println("\nTime for steady-state probability computation: " + l / 1000.0 + " seconds."); @@ -2655,7 +2657,7 @@ public class Prism implements PrismSettingsListener probs.clear(); else probsExpl.clear(); - if (file != null) + if (fileOut != null) tmpLog.close(); } @@ -2671,7 +2673,7 @@ public class Prism implements PrismSettingsListener /** * Compute transient probabilities (forwards) for the current model (DTMCs/CTMCs only). - * Output probability distribution to a file (or, if file is null, to log). + * Output probability distribution to a file (or, if {@code fileOut} is null, to log). * For a discrete-time model, {@code time} will be cast to an integer. * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB. * Optionally (if non-null), read in the initial probability distribution from a file. @@ -3273,7 +3275,7 @@ public class Prism implements PrismSettingsListener public void doSteadyState(Model model, int exportType, File file) throws PrismException { loadBuiltModel(model); - doSteadyState(exportType, file); + doSteadyState(exportType, file, null); } /** diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 98d29cf8..a1f0190b 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -728,7 +728,7 @@ public class PrismCL implements PrismModelListener else exportSteadyStateFile = new File(exportSteadyStateFilename); // Compute steady-state probabilities - prism.doSteadyState(exportType, exportSteadyStateFile); + prism.doSteadyState(exportType, exportSteadyStateFile, importinitdist ? new File(importInitDistFilename) : null); } catch (PrismException e) { // In case of error, report it and proceed error(e.getMessage());