From b76fe0e8b142ddf7de5723844d0e7acf7acc0fdc Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Mon, 18 Apr 2016 16:38:38 +0000 Subject: [PATCH] Add -exportprodvector switch, which exports solution vector over product model after checking LTL-based properties. Currently, supported in explicit engine, or symbolic engines where the result ends up being a vector of doubles (not an MTBDD). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11305 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/DTMCModelChecker.java | 16 +++++++++++++++ prism/src/explicit/MDPModelChecker.java | 16 +++++++++++++++ prism/src/explicit/StateModelChecker.java | 24 +++++++++++++++++++++++ prism/src/prism/NondetModelChecker.java | 8 ++++++++ prism/src/prism/Prism.java | 24 +++++++++++++++++++++++ prism/src/prism/PrismCL.java | 9 +++++++++ 6 files changed, 97 insertions(+) diff --git a/prism/src/explicit/DTMCModelChecker.java b/prism/src/explicit/DTMCModelChecker.java index 8b17bcae..e6c5b305 100644 --- a/prism/src/explicit/DTMCModelChecker.java +++ b/prism/src/explicit/DTMCModelChecker.java @@ -114,6 +114,14 @@ public class DTMCModelChecker extends ProbModelChecker mcProduct.inheritSettings(this); probsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachProbs(product.getProductModel(), acc).soln, product.getProductModel()); + // Output vector over product, if required + if (getExportProductVector()) { + mainLog.println("\nExporting product solution vector matrix to file \"" + getExportProductVectorFilename() + "\"..."); + PrismFileLog out = new PrismFileLog(getExportProductVectorFilename()); + probsProduct.print(out, false, false, false, false); + out.close(); + } + // Mapping probabilities in the original model probs = product.projectToOriginalModel(probsProduct); probsProduct.clear(); @@ -177,6 +185,14 @@ public class DTMCModelChecker extends ProbModelChecker mcProduct.inheritSettings(this); rewardsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachRewards(product.getProductModel(), productRewards, acc).soln, product.getProductModel()); + // Output vector over product, if required + if (getExportProductVector()) { + mainLog.println("\nExporting product solution vector matrix to file \"" + getExportProductVectorFilename() + "\"..."); + PrismFileLog out = new PrismFileLog(getExportProductVectorFilename()); + rewardsProduct.print(out, false, false, false, false); + out.close(); + } + // Mapping rewards in the original model rewards = product.projectToOriginalModel(rewardsProduct); rewardsProduct.clear(); diff --git a/prism/src/explicit/MDPModelChecker.java b/prism/src/explicit/MDPModelChecker.java index 194f27dd..30879e73 100644 --- a/prism/src/explicit/MDPModelChecker.java +++ b/prism/src/explicit/MDPModelChecker.java @@ -131,6 +131,14 @@ public class MDPModelChecker extends ProbModelChecker probsProduct.plusConstant(1.0); } + // Output vector over product, if required + if (getExportProductVector()) { + mainLog.println("\nExporting product solution vector matrix to file \"" + getExportProductVectorFilename() + "\"..."); + PrismFileLog out = new PrismFileLog(getExportProductVectorFilename()); + probsProduct.print(out, false, false, false, false); + out.close(); + } + // Mapping probabilities in the original model probs = product.projectToOriginalModel(probsProduct); probsProduct.clear(); @@ -196,6 +204,14 @@ public class MDPModelChecker extends ProbModelChecker mcProduct.inheritSettings(this); rewardsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachRewards(product.getProductModel(), productRewards, acc, minMax.isMin()).soln, product.getProductModel()); + // Output vector over product, if required + if (getExportProductVector()) { + mainLog.println("\nExporting product solution vector matrix to file \"" + getExportProductVectorFilename() + "\"..."); + PrismFileLog out = new PrismFileLog(getExportProductVectorFilename()); + rewardsProduct.print(out, false, false, false, false); + out.close(); + } + // Mapping rewards in the original model rewards = product.projectToOriginalModel(rewardsProduct); rewardsProduct.clear(); diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 6b8d828b..90b1ce3f 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -101,6 +101,8 @@ public class StateModelChecker extends PrismComponent protected String exportProductTransFilename = null; protected boolean exportProductStates = false; protected String exportProductStatesFilename = null; + protected boolean exportProductVector = false; + protected String exportProductVectorFilename = null; // Store the final results vector after model checking? protected boolean storeVector = false; @@ -200,6 +202,8 @@ public class StateModelChecker extends PrismComponent setExportProductTransFilename(other.getExportProductTransFilename()); setExportProductStates(other.getExportProductStates()); setExportProductStatesFilename(other.getExportProductStatesFilename()); + setExportProductVector(other.getExportProductVector()); + setExportProductVectorFilename(other.getExportProductVectorFilename()); setStoreVector(other.getStoreVector()); setGenStrat(other.getGenStrat()); setDoBisim(other.getDoBisim()); @@ -253,6 +257,16 @@ public class StateModelChecker extends PrismComponent exportProductStatesFilename = s; } + public void setExportProductVector(boolean b) + { + exportProductVector = b; + } + + public void setExportProductVectorFilename(String s) + { + exportProductVectorFilename = s; + } + /** * Specify whether or not to store the final results vector after model checking. */ @@ -314,6 +328,16 @@ public class StateModelChecker extends PrismComponent return exportProductStatesFilename; } + public boolean getExportProductVector() + { + return exportProductVector; + } + + public String getExportProductVectorFilename() + { + return exportProductVectorFilename; + } + /** * Whether or not to store the final results vector after model checking. */ diff --git a/prism/src/prism/NondetModelChecker.java b/prism/src/prism/NondetModelChecker.java index 6d9f6026..4b13f856 100644 --- a/prism/src/prism/NondetModelChecker.java +++ b/prism/src/prism/NondetModelChecker.java @@ -1224,6 +1224,14 @@ public class NondetModelChecker extends NonProbModelChecker probsProduct.subtractFromOne(); } + // Output vector over product, if required + if (prism.getExportProductVector()) { + mainLog.println("\nExporting product solution vector matrix to file \"" + prism.getExportProductVectorFilename() + "\"..."); + PrismFileLog out = new PrismFileLog(prism.getExportProductVectorFilename()); + probsProduct.print(out, false, false, false, false); + out.close(); + } + // Convert probability vector to original model // First, filter over DRA start states startMask = mcLtl.buildStartMask(da, labelDDs, daDDRowVars); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 34b8cde7..49741959 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -191,6 +191,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener protected String exportProductTransFilename = null; protected boolean exportProductStates = false; protected String exportProductStatesFilename = null; + protected boolean exportProductVector = false; + protected String exportProductVectorFilename = null; // Store the final results vector after model checking? protected boolean storeVector = false; // Generate/store a strategy during model checking? @@ -568,6 +570,16 @@ public class Prism extends PrismComponent implements PrismSettingsListener exportProductStatesFilename = s; } + public void setExportProductVector(boolean b) throws PrismException + { + exportProductVector = b; + } + + public void setExportProductVectorFilename(String s) throws PrismException + { + exportProductVectorFilename = s; + } + /** * Specify whether or not to store the final results vector after model checking. */ @@ -883,6 +895,16 @@ public class Prism extends PrismComponent implements PrismSettingsListener return exportProductStatesFilename; } + public boolean getExportProductVector() + { + return exportProductVector; + } + + public String getExportProductVectorFilename() + { + return exportProductVectorFilename; + } + /** * Whether or not to store the final results vector after model checking. */ @@ -3625,6 +3647,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener mc.setExportProductTransFilename(exportProductTransFilename); mc.setExportProductStates(exportProductStates); mc.setExportProductStatesFilename(exportProductStatesFilename); + mc.setExportProductVector(exportProductVector); + mc.setExportProductVectorFilename(exportProductVectorFilename); mc.setStoreVector(storeVector); mc.setGenStrat(genStrat); mc.setDoBisim(doBisim); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 72aab5db..c4ae4b20 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -1471,6 +1471,15 @@ public class PrismCL implements PrismModelListener errorAndExit("No file specified for -" + sw + " switch"); } } + // export product vector to file (hidden option) + else if (sw.equals("exportprodvector")) { + if (i < args.length - 1) { + prism.setExportProductVector(true); + prism.setExportProductVectorFilename(args[++i]); + } else { + errorAndExit("No file specified for -" + sw + " switch"); + } + } // export model to plain text file (deprecated option so hidden) else if (sw.equals("exportplain")) { if (i < args.length - 1) {