s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Code tidy. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7575 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
cdb6b005d5
commit
d8fb4ef1cc
1 changed files with 19 additions and 29 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 48
      prism/src/prism/Prism.java

48
prism/src/prism/Prism.java
View File

@ -2935,26 +2935,24 @@ public class Prism extends PrismComponent implements PrismSettingsListener
explicit.StateValues probsExpl = null;
PrismLog tmpLog;
// Do some checks
if (!(currentModelType == ModelType.CTMC || currentModelType == ModelType.DTMC))
throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs");
if (fileOut != null && getEngine() == MTBDD)
// TODO: auto-switch?
throw new PrismException("Steady-state probability export not supported for MTBDD engine");
// TODO: auto-switch?
if (exportType == EXPORT_MRMC)
exportType = EXPORT_PLAIN; // no specific states format for MRMC
if (exportType == EXPORT_ROWS)
exportType = EXPORT_PLAIN; // rows format does not apply to states output
// Print message
mainLog.printSeparator();
mainLog.println("\nComputing steady-state probabilities...");
// Build model, if necessary
buildModelIfRequired();
// 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;
l = System.currentTimeMillis();
if (!getExplicit()) {
@ -3032,32 +3030,26 @@ public class Prism extends PrismComponent implements PrismSettingsListener
explicit.StateValues probsExpl = null;
PrismLog tmpLog;
// Do some checks
if (!(currentModelType == ModelType.CTMC || currentModelType == ModelType.DTMC))
throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs");
if (time < 0)
throw new PrismException("Cannot compute transient probabilities for negative time value");
if (fileOut != null && getEngine() == MTBDD)
throw new PrismException("Transient probability export only supported for sparse/hybrid engines");
if (exportType == EXPORT_MRMC)
exportType = EXPORT_PLAIN; // no specific states format for MRMC
if (exportType == EXPORT_ROWS)
exportType = EXPORT_PLAIN; // rows format does not apply to states output
// Print message
mainLog.printSeparator();
if (currentModelType.continuousTime()) {
mainLog.println("\nComputing transient probabilities (time = " + time + ")...");
} else {
mainLog.println("\nComputing transient probabilities (time = " + (int) time + ")...");
}
String strTime = currentModelType.continuousTime() ? Double.toString(time) : Integer.toString((int) time);
mainLog.println("\nComputing transient probabilities (time = " + strTime + ")...");
// Build model, if necessary
buildModelIfRequired();
// 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;
l = System.currentTimeMillis();
if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) {
@ -3135,18 +3127,15 @@ public class Prism extends PrismComponent implements PrismSettingsListener
PrismLog tmpLog = null;
File fileOutActual = null;
// Do some checks
if (!(currentModelType == ModelType.CTMC || currentModelType == ModelType.DTMC))
throw new PrismException("Steady-state probabilities only computed for DTMCs/CTMCs");
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
exportType = EXPORT_PLAIN; // no specific states format for MRMC
if (exportType == EXPORT_ROWS)
exportType = EXPORT_PLAIN;
exportType = EXPORT_PLAIN; // rows format does not apply to states output
// Step through required time points
for (i = 0; i < times.getNumPropertyIterations(); i++) {
@ -3160,6 +3149,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
if (currentModelType.continuousTime() ? (((Double) time).doubleValue() < 0) : (((Integer) time).intValue() < 0))
throw new PrismException("Cannot compute transient probabilities for negative time value");
// Print message
mainLog.printSeparator();
mainLog.println("\nComputing transient probabilities (time = " + time + ")...");

Write Preview
Loading…
Cancel
Save