From f3a3faed33254c256d62cc82507c0cb2a2ff831b Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 8 Dec 2010 09:52:28 +0000 Subject: [PATCH] Added -exportsteadystate switch to export steady-state probs to a file. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2325 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Prism.java | 61 ++++++++++++++++++++++++++++++------ prism/src/prism/PrismCL.java | 20 +++++++++++- 2 files changed, 70 insertions(+), 11 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index eaee968f..7515c24f 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -1510,12 +1510,33 @@ public class Prism implements PrismSettingsListener genPath.generateSimulationPath(modulesFile, modulesFile.getInitialValues(), details, maxPathLength, file); } - // do steady state - + /** + * Compute steady-state probabilities (for a DTMC or CTMC). + * Output probability distribution to log. + */ public void doSteadyState(Model model) throws PrismException + { + doSteadyState(model, 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; + + if (fileOut != null && getEngine() == MTBDD) + throw new PrismException("Transient probability export only supported for sparse/hybrid engines"); + + // no specific states format for MRMC + if (exportType == EXPORT_MRMC) exportType = EXPORT_PLAIN; + // rows format does not apply to states output + if (exportType == EXPORT_ROWS) exportType = EXPORT_PLAIN; mainLog.println("\nComputing steady-state probabilities..."); l = System.currentTimeMillis(); @@ -1534,17 +1555,37 @@ public class Prism implements PrismSettingsListener l = System.currentTimeMillis() - l; - // print out probabilities - mainLog.print("\nProbabilities: \n"); - probs.print(mainLog); - probs.clear(); + // print message + mainLog.print("\nPrinting steady-state probabilities "); + switch (exportType) { + case EXPORT_PLAIN: mainLog.print("in plain text format "); break; + case 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 model checking time + // print out or export probabilities + probs.print(tmpLog, fileOut == null, exportType == 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 DTMC or CTMC). + * Compute transient probabilities (for a DTMC or CTMC). * Output probability distribution to log. */ public void doTransient(Model model, double time) throws PrismException @@ -1553,7 +1594,7 @@ public class Prism implements PrismSettingsListener } /** - * Compute transient probabilities (for DTMC or CTMC). + * Compute transient 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. * Optionally (if non-null), read in the initial probability distribution from a file. @@ -1616,7 +1657,7 @@ public class Prism implements PrismSettingsListener // print out or export probabilities probs.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null); - // print out model checking time + // print out computation time mainLog.println("\nTime for transient probability computation: " + l/1000.0 + " seconds."); // tidy up diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index a85b0dc2..9c18eb9e 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -98,6 +98,7 @@ public class PrismCL private String exportTransDotStatesFilename = null; private String exportBSCCsFilename = null; private String exportResultsFilename = null; + private String exportSteadyStateFilename = null; private String exportTransientFilename = null; private String exportPrismFilename = null; private String exportPrismConstFilename = null; @@ -835,9 +836,17 @@ public class PrismCL private void doSteadyState() throws PrismException { + File exportSteadyStateFile = null; + + // choose destination for output (file or log) + if (exportSteadyStateFilename == null || exportSteadyStateFilename.equals("stdout")) + exportSteadyStateFile = null; + else + exportSteadyStateFile = new File(exportSteadyStateFilename); + // compute steady-state probabilities if (model.getModelType() == ModelType.CTMC || model.getModelType() == ModelType.DTMC) { - prism.doSteadyState(model); + prism.doSteadyState(model, exportType, exportSteadyStateFile); } else { mainLog.println("\nWarning: Steady-state probabilities only computed for DTMCs/CTMCs."); } @@ -1125,6 +1134,14 @@ public class PrismCL errorAndExit("No file specified for -" + sw + " switch"); } } + // export steady-state probs (as opposed to displaying on screen) + else if (sw.equals("exportsteadystate") || sw.equals("exportss")) { + if (i < args.length - 1) { + exportSteadyStateFilename = args[++i]; + } else { + errorAndExit("No file specified for -" + sw + " switch"); + } + } // export transient probs (as opposed to displaying on screen) else if (sw.equals("exporttransient") || sw.equals("exporttr")) { if (i < args.length - 1) { @@ -1788,6 +1805,7 @@ public class PrismCL mainLog.println("-exporttransdotstates ... Export the transition matrix graph to a dot file, with state info"); mainLog.println("-exportdot .............. Export the transition matrix MTBDD to a dot file"); mainLog.println("-exportbsccs ............ Compute and export all BSCCs of the model"); + mainLog.println("-exportsteadystate ...... Export steady-state probabilities to a file"); mainLog.println("-exporttransient ........ Export transient probabilities to a file"); mainLog.println("-exportprism ............ Export final PRISM model to a file"); mainLog.println("-exportprismconst ....... Export final PRISM model with expanded constants to a file");