From d9a49aba4237959f7ef3c865d7cd90e91a8e143f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 12 Nov 2013 01:14:40 +0000 Subject: [PATCH] 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 --- prism/src/prism/Prism.java | 27 +++++++++++++++++---------- prism/src/prism/PrismCL.java | 19 +++++++++---------- 2 files changed, 26 insertions(+), 20 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 62e810d0..9f2f38cf 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -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) { diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 7b09b173..63a2a737 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -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 \n");