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

Do not build the model when doing transient probability computation via FAU (+ some code tidying). 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7580 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 12 years ago
parent
e99167b755
commit
d9a49aba42
2 changed files with 26 additions and 20 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. 27
      prism/src/prism/Prism.java
  2. 19
      prism/src/prism/PrismCL.java

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

@ -1779,7 +1779,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
private void doBuildModel() throws PrismException
{
long l; // timer
new Exception().printStackTrace();
// Clear any existing built model(s)
clearBuiltModel();
@ -3047,17 +3047,18 @@ public class Prism extends PrismComponent implements PrismSettingsListener
String strTime = currentModelType.continuousTime() ? Double.toString(time) : Integer.toString((int) time);
mainLog.println("\nComputing transient probabilities (time = " + strTime + ")...");
// Build model, if necessary
buildModelIfRequired();
l = System.currentTimeMillis();
// FAU
if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) {
PrismModelExplorer modelExplorer = new PrismModelExplorer(getSimulator(), currentModulesFile);
FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, modelExplorer);
fau.setConstantValues(currentModulesFile.getConstantValues());
probsExpl = fau.doTransient(time, fileIn);
} else if (!getExplicit()) {
}
// Symbolic
else if (!getExplicit()) {
buildModelIfRequired();
if (currentModelType == ModelType.DTMC) {
mc = new ProbModelChecker(this, currentModel, null);
probs = ((ProbModelChecker) mc).doTransient((int) time, fileIn);
@ -3065,7 +3066,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener
mc = new StochModelChecker(this, currentModel, null);
probs = ((StochModelChecker) mc).doTransient(time, fileIn);
}
} else {
}
// Explicit
else {
buildModelIfRequired();
if (currentModelType == ModelType.DTMC) {
throw new PrismException("Not implemented yet");
} else if (currentModelType == ModelType.CTMC) {
@ -3150,11 +3154,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
mainLog.printSeparator();
mainLog.println("\nComputing transient probabilities (time = " + time + ")...");
// Build model, if necessary
buildModelIfRequired();
l = System.currentTimeMillis();
// FAU
if (currentModelType == ModelType.CTMC && settings.getString(PrismSettings.PRISM_TRANSIENT_METHOD).equals("Fast adaptive uniformisation")) {
// For FAU, we don't do computation incrementally
PrismModelExplorer modelExplorer = new PrismModelExplorer(getSimulator(), currentModulesFile);
@ -3162,7 +3164,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener
fau.setConstantValues(currentModulesFile.getConstantValues());
probsExpl = fau.doTransient(timeDouble, fileIn);
}
// Symbolic
else if (!getExplicit()) {
buildModelIfRequired();
if (currentModelType.continuousTime()) {
StochModelChecker mc = new StochModelChecker(this, currentModel, null);
if (i == 0) {
@ -3178,7 +3182,10 @@ public class Prism extends PrismComponent implements PrismSettingsListener
}
probs = ((ProbModelChecker) mc).doTransient(timeInt - initTimeInt, initDist);
}
} else {
}
// Explicit
else {
buildModelIfRequired();
if (currentModelType.continuousTime()) {
CTMCModelChecker mc = new CTMCModelChecker(this);
if (i == 0) {

19
prism/src/prism/PrismCL.java
View File

@ -356,7 +356,7 @@ public class PrismCL implements PrismModelListener
// store result of model checking
results[j].setResult(definedMFConstants, definedPFConstants, res.getResult());
// if a counterexample was generated, display it
Object cex = res.getCounterexample();
if (cex != null) {
@ -386,7 +386,7 @@ public class PrismCL implements PrismModelListener
error(e.getMessage());
}
}
// if required, check result against expected value
if (test) {
try {
@ -419,7 +419,7 @@ public class PrismCL implements PrismModelListener
}
// Explicitly request a build if necessary
if (propertiesToCheck.size() == 0 && !simpath && !nobuild && prism.modelCanBeBuilt() && !prism.modelIsBuilt()) {
if (propertiesToCheck.size() == 0 && !steadystate && !dotransient && !simpath && !nobuild && prism.modelCanBeBuilt() && !prism.modelIsBuilt()) {
try {
prism.buildModel();
} catch (PrismException e) {
@ -775,7 +775,7 @@ public class PrismCL implements PrismModelListener
error(e.getMessage());
}
}
// export BSCCs to a file
if (exportbsccs) {
try {
@ -1124,18 +1124,17 @@ public class PrismCL implements PrismModelListener
s = args[++i];
// Assume use of : to split filename/options but check for , if : not found
// (this was the old notation)
String halves[] = splitFilesAndOptions(s);
String halves[] = splitFilesAndOptions(s);
if (halves[1].length() == 0 && halves[0].indexOf(',') > -1) {
int comma = halves[0].indexOf(',');
halves[1] = halves[0].substring(comma + 1);
halves[1] = halves[0].substring(comma + 1);
halves[0] = halves[0].substring(0, comma);
}
exportResultsFilename = halves[0];
String ss[] = halves[1].split(",");
for (j = 0; j < ss.length; j++) {
if (ss[j].equals("")) {
}
else if (ss[j].equals("csv"))
} else if (ss[j].equals("csv"))
exportresultscsv = true;
else if (ss[j].equals("matrix"))
exportresultsmatrix = true;
@ -1926,7 +1925,7 @@ public class PrismCL implements PrismModelListener
}
}
}
// plug in basename for -exportmodel switch if needed
if (exportModelNoBasename) {
String modelFileBasename = modelFilename;
@ -2155,7 +2154,7 @@ public class PrismCL implements PrismModelListener
// Remove "-" from start of switch, in case present (it shouldn't be really)
if (sw.charAt(0) == '-')
sw = sw.substring(1);
// -const
if (sw.equals("const")) {
mainLog.println("Switch: -const <vals>\n");

Write Preview
Loading…
Cancel
Save