From e99167b755b13e9090e0eb6b588b11ad17cb30fa Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 12 Nov 2013 00:37:08 +0000 Subject: [PATCH] Connect FAU to normal (command-line) transient probability computation. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7579 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/Prism.java | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index c3592830..62e810d0 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -3087,7 +3087,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener tmpLog = getPrismLogForFile(fileOut); // print out or export probabilities - if (!getExplicit()) + if (probs != null) probs.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null, fileOut == null); else probsExpl.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null, fileOut == null); @@ -3096,9 +3096,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener mainLog.println("\nTime for transient probability computation: " + l / 1000.0 + " seconds."); // tidy up - if (!getExplicit()) + if (probs != null) probs.clear(); - else + if (probsExpl != null) probsExpl.clear(); if (fileOut != null) tmpLog.close(); @@ -3155,7 +3155,14 @@ public class Prism extends PrismComponent implements PrismSettingsListener l = System.currentTimeMillis(); - if (!getExplicit()) { + 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); + FastAdaptiveUniformisation fau = new FastAdaptiveUniformisation(this, modelExplorer); + fau.setConstantValues(currentModulesFile.getConstantValues()); + probsExpl = fau.doTransient(timeDouble, fileIn); + } + else if (!getExplicit()) { if (currentModelType.continuousTime()) { StochModelChecker mc = new StochModelChecker(this, currentModel, null); if (i == 0) { @@ -3202,7 +3209,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener tmpLog = getPrismLogForFile(fileOutActual); // print out or export probabilities - if (!getExplicit()) + if (probs != null) probs.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null); else probsExpl.print(tmpLog, fileOut == null, exportType == EXPORT_MATLAB, fileOut == null, true); @@ -3219,9 +3226,9 @@ public class Prism extends PrismComponent implements PrismSettingsListener } // tidy up - if (!getExplicit()) + if (probs != null) probs.clear(); - else + if (probsExpl != null) probsExpl.clear(); if (fileOut != null) tmpLog.close();