diff --git a/prism/src/explicit/CTMCModelChecker.java b/prism/src/explicit/CTMCModelChecker.java index bdad7cf1..2ae0b99e 100644 --- a/prism/src/explicit/CTMCModelChecker.java +++ b/prism/src/explicit/CTMCModelChecker.java @@ -168,16 +168,7 @@ public class CTMCModelChecker extends DTMCModelChecker */ 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); - } - + StateValues initDist = readDistributionFromFile(initDistFile, ctmc); return doTransient(ctmc, t, initDist); } diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 7efa1e62..33c985c2 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -26,12 +26,14 @@ package explicit; +import java.io.File; import java.util.*; import prism.*; import explicit.StateValues; import explicit.rewards.*; import parser.ast.*; +import parser.type.TypeDouble; /** * Explicit-state model checker for discrete-time Markov chains (DTMCs). @@ -248,6 +250,25 @@ public class DTMCModelChecker extends ProbModelChecker throw new PrismException("Not implemented yet"); } + /** + * Generate a probability distribution, stored as a StateValues object, from a file. + * If {@code distFile} is null, so is the return value. + */ + public StateValues readDistributionFromFile(File distFile, Model model) throws PrismException + { + StateValues dist = null; + + if (distFile != null) { + mainLog.println("\nImporting probability distribution from file \"" + distFile + "\"..."); + // Build an empty vector + dist = new StateValues(TypeDouble.getInstance(), model); + // Populate vector from file + dist.readFromFile(distFile); + } + + return dist; + } + // Numerical computation functions /** diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 2bfee359..1b121a8b 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -150,9 +150,9 @@ public class Prism implements PrismSettingsListener // Round-off threshold for places where doubles are summed and compared to integers // (e.g. checking that probabilities sum to 1 in an update). private double sumRoundOff = 1e-5; - + // Method to use for (symbolic) state-space reachability - private int reachMethod = REACH_BFS; + private int reachMethod = REACH_BFS; //------------------------------------------------------------------------------ // Logs @@ -494,7 +494,7 @@ public class Prism implements PrismSettingsListener public static int REACH_BFS = 1; public static int REACH_FRONTIER = 2; - + public void setReachMethod(int reachMethod) { this.reachMethod = reachMethod; @@ -754,7 +754,7 @@ public class Prism implements PrismSettingsListener { return reachMethod; } - + public void addModelListener(PrismModelListener listener) { modelListeners.add(listener); @@ -2588,8 +2588,9 @@ public class Prism implements PrismSettingsListener } /** - * Compute transient probabilities for the current model (DTMCs/CTMCs only). - * Output probability distribution to log. + * Compute transient probabilities (forwards) for the current model (DTMCs/CTMCs only). + * Output probability distribution to log. + * For a discrete-time model, {@code time} will be cast to an integer. */ public void doTransient(double time) throws PrismException { @@ -2597,8 +2598,9 @@ public class Prism implements PrismSettingsListener } /** - * Compute transient probabilities for the current model (DTMCs/CTMCs only). + * Compute transient probabilities (forwards) for the current model (DTMCs/CTMCs only). * Output probability distribution to a file (or, if file 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. */ @@ -2687,6 +2689,125 @@ public class Prism implements PrismSettingsListener tmpLog.close(); } + /** + * Compute transient probabilities (forwards) for the current model (DTMCs/CTMCs only) + * for a range of time points. Each distribution is computed incrementally. + * Output probability distribution to a file (or, if file is null, to log). + * Time points are specified using an UndefinedConstants with a single ranging variable + * (of the appropriate type (int/double) and with arbitrary name). + * The exportType should be EXPORT_PLAIN or EXPORT_MATLAB. + * Optionally (if non-null), read in the initial probability distribution from a file. + */ + public void doTransient(UndefinedConstants times, int exportType, File file, File fileIn) throws PrismException + { + int i, timeInt = 0, initTimeInt = 0; + double timeDouble = 0, initTimeDouble = 0; + Object time; + long l = 0; // timer + StateValues probs = null, initDist = null; + explicit.StateValues probsExpl = null, initDistExpl = null; + PrismLog tmpLog = null; + + if (!(currentModelType == ModelType.CTMC || currentModelType == ModelType.DTMC)) + throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs"); + + if (file != 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; + + // Step through required time points + for (i = 0; i < times.getNumPropertyIterations(); i++) { + + // Get time, check non-negative + time = times.getPFConstantValues().getValue(0); + if (currentModelType.continuousTime()) + timeDouble = ((Double) time).doubleValue(); + else + timeInt = ((Integer) time).intValue(); + if (currentModelType.continuousTime() ? (((Double) time).doubleValue() < 0) : (((Integer) time).intValue() < 0)) + throw new PrismException("Cannot compute transient probabilities for negative time value"); + + mainLog.printSeparator(); + mainLog.println("\nComputing transient probabilities (time = " + time + ")..."); + + // Build model, if necessary + buildModelIfRequired(); + + l = System.currentTimeMillis(); + + if (!getExplicit()) { + if (currentModelType.continuousTime()) { + StochModelChecker mc = new StochModelChecker(this, currentModel, null); + if (i == 0) { + initDist = mc.readDistributionFromFile(fileIn); + initTimeDouble = 0; + } + probs = ((StochModelChecker) mc).doTransient(timeDouble - initTimeDouble, initDist); + } else { + ProbModelChecker mc = new ProbModelChecker(this, currentModel, null); + if (i == 0) { + initDist = mc.readDistributionFromFile(fileIn); + initTimeInt = 0; + } + probs = ((ProbModelChecker) mc).doTransient(timeInt - initTimeInt, initDist); + } + } else { + if (currentModelType.continuousTime()) { + CTMCModelChecker mc = new CTMCModelChecker(); + mc.setLog(mainLog); + mc.setSettings(settings); + if (i == 0) { + initDistExpl = mc.readDistributionFromFile(fileIn, currentModelExpl); + initTimeDouble = 0; + } + probsExpl = mc.doTransient((CTMC) currentModelExpl, timeDouble - initTimeDouble, initDistExpl); + } else { + throw new PrismException("Not implemented yet"); + } + } + + l = System.currentTimeMillis() - l; + + // print message + mainLog.print("\nPrinting transient probabilities "); + mainLog.print(getStringForExportType(exportType) + " "); + mainLog.println(getDestinationStringForFile(file)); + + // create new file log or use main log + tmpLog = getPrismLogForFile(file); + + // print out or export probabilities + if (!getExplicit()) + probs.print(tmpLog, file == null, exportType == EXPORT_MATLAB, file == null); + else + probsExpl.print(tmpLog, file == null, exportType == EXPORT_MATLAB, file == null, true); + + // print out computation time + mainLog.println("\nTime for transient probability computation: " + l / 1000.0 + " seconds."); + + // Prepare for next iteration + initDist = probs; + initDistExpl = probsExpl; + initTimeInt = timeInt; + initTimeDouble = timeDouble; + times.iterateProperty(); + } + + // tidy up + if (!getExplicit()) + probs.clear(); + else + probsExpl.clear(); + if (file != null) + tmpLog.close(); + } + public void explicitBuildTest() throws PrismException { /* old code... @@ -2721,7 +2842,7 @@ public class Prism implements PrismSettingsListener throw new PrismException("Could not create temporary file \"" + tmpFile + "\""); }*/ } - + /** * Clear the built model if needed (free/deallocate memory etc) */ diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 4571bab9..7d64e36a 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -732,8 +732,6 @@ public class PrismCL implements PrismModelListener private void doTransient() { ModelType modelType; - double d; - int i; File exportTransientFile = null; if (dotransient) { @@ -747,24 +745,20 @@ public class PrismCL implements PrismModelListener // Determine model type modelType = prism.getModelType(); - // Compute transient probabilities - if (modelType == ModelType.CTMC) { - try { - d = Double.parseDouble(transientTime); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value \"" + transientTime + "\" for transient probability computation"); - } - prism.doTransient(d, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null); - } else if (modelType == ModelType.DTMC) { - try { - i = Integer.parseInt(transientTime); - } catch (NumberFormatException e) { - throw new PrismException("Invalid value \"" + transientTime + "\" for transient probability computation"); - } - prism.doTransient(i, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null); - } else { - mainLog.printWarning("Transient probabilities only computed for DTMCs/CTMCs."); + // Parse time specification, store as UndefinedConstant for constant T + String timeType = modelType.continuousTime() ? "double" : "int"; + UndefinedConstants ucTransient = new UndefinedConstants(null, prism.parsePropertiesString(null, "const " + timeType + " T; T;")); + try { + ucTransient.defineUsingConstSwitch("T=" + transientTime); + } catch (PrismException e) { + if (transientTime.contains(":")) + errorAndExit("\"" + transientTime + "\" is not a valid time range for a " + modelType); + else + errorAndExit("\"" + transientTime + "\" is not a valid time for a " + modelType); } + + // Compute transient probabilities + prism.doTransient(ucTransient, exportType, exportTransientFile, importinitdist ? new File(importInitDistFilename) : null); } // In case of error, report it and proceed catch (PrismException e) { @@ -814,7 +808,6 @@ public class PrismCL implements PrismModelListener private void parseArguments(String[] args) throws PrismException { int i, j; - double d; String sw, s; PrismLog log; @@ -886,16 +879,8 @@ public class PrismCL implements PrismModelListener // do transient probability computation else if (sw.equals("transient") || sw.equals("tr")) { if (i < args.length - 1) { - try { - dotransient = true; - transientTime = args[++i]; - // Make sure transient time parses as a +ve double - d = Double.parseDouble(transientTime); - if (d < 0) - throw new NumberFormatException(""); - } catch (NumberFormatException e) { - errorAndExit("Invalid value for -" + sw + " switch"); - } + dotransient = true; + transientTime = args[++i]; } else { errorAndExit("No value specified for -" + sw + " switch"); } @@ -1418,8 +1403,7 @@ public class PrismCL implements PrismModelListener // reachability options (hidden options) else if (sw.equals("frontier")) { prism.setReachMethod(Prism.REACH_FRONTIER); - } - else if (sw.equals("bfs")) { + } else if (sw.equals("bfs")) { prism.setReachMethod(Prism.REACH_BFS); } diff --git a/prism/src/prism/ProbModelChecker.java b/prism/src/prism/ProbModelChecker.java index e3db35c3..8a886e3a 100644 --- a/prism/src/prism/ProbModelChecker.java +++ b/prism/src/prism/ProbModelChecker.java @@ -1225,20 +1225,7 @@ public class ProbModelChecker extends NonProbModelChecker */ public StateValues doTransient(int time, File initDistFile) throws PrismException { - StateValues initDist = null; - - if (initDistFile != null) { - mainLog.println("\nImporting initial probability distribution from file \"" + initDistFile + "\"..."); - // Build an empty vector of the appropriate type - if (engine == Prism.MTBDD) { - initDist = new StateValuesMTBDD(JDD.Constant(0), model); - } else { - initDist = new StateValuesDV(new DoubleVector((int) model.getNumStates()), model); - } - // Populate vector from file - initDist.readFromFile(initDistFile); - } - + StateValues initDist = readDistributionFromFile(initDistFile); return doTransient(time, initDist); } @@ -1283,6 +1270,30 @@ public class ProbModelChecker extends NonProbModelChecker return probs; } + /** + * Generate a probability distribution, stored as a StateValues object, from a file. + * The type of storage (MTBDD or double vector) matches the current engine. + * If {@code distFile} is null, so is the return value. + */ + public StateValues readDistributionFromFile(File distFile) throws PrismException + { + StateValues dist = null; + + if (distFile != null) { + mainLog.println("\nImporting probability distribution from file \"" + distFile + "\"..."); + // Build an empty vector of the appropriate type + if (engine == Prism.MTBDD) { + dist = new StateValuesMTBDD(JDD.Constant(0), model); + } else { + dist = new StateValuesDV(new DoubleVector((int) model.getNumStates()), model); + } + // Populate vector from file + dist.readFromFile(distFile); + } + + return dist; + } + // ----------------------------------------------------------------------------------- // probability computation methods // -----------------------------------------------------------------------------------