|
|
|
@ -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); |
|
|
|
} |
|
|
|
|
|
|
|
/** |
|
|
|
|