From d1f8a87aeb714bbddc5eb6c9c1f1ffb177771c59 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 25 Apr 2019 22:50:11 +0100 Subject: [PATCH] First version of -exportvector switch for the command-line. Exports the value of a model checked property for all states as a vector. If is "stdout", this is displayed to the log instead of a file. Currently, only works for a single property: if there is more than one, then the file gets overwritten each time a property is checked. Also fixes a bug in the underlying mechanism for storing results vectors in the explicit engine (within Results objects). --- .../export/vector/exportvector.prism | 11 +++++++ .../export/vector/exportvector.prism.args | 4 +++ .../export/vector/exportvector.prism.props | 2 ++ .../vector/exportvector.prism.props.args | 1 + .../vector/exportvector.prism.props.txt | 7 +++++ prism/src/explicit/StateModelChecker.java | 1 - prism/src/prism/PrismCL.java | 30 +++++++++++++++++++ prism/src/prism/StateVector.java | 5 ++++ 8 files changed, 60 insertions(+), 1 deletion(-) create mode 100644 prism-tests/functionality/export/vector/exportvector.prism create mode 100644 prism-tests/functionality/export/vector/exportvector.prism.args create mode 100644 prism-tests/functionality/export/vector/exportvector.prism.props create mode 100644 prism-tests/functionality/export/vector/exportvector.prism.props.args create mode 100644 prism-tests/functionality/export/vector/exportvector.prism.props.txt diff --git a/prism-tests/functionality/export/vector/exportvector.prism b/prism-tests/functionality/export/vector/exportvector.prism new file mode 100644 index 00000000..9742a74a --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism @@ -0,0 +1,11 @@ +dtmc + +const int N; + +module M + + x : [-N..N] init 0; + + [] true -> 0.5:(x'=max(x-1,-N)) + 0.5:(x'=min(x+1,N)); + +endmodule diff --git a/prism-tests/functionality/export/vector/exportvector.prism.args b/prism-tests/functionality/export/vector/exportvector.prism.args new file mode 100644 index 00000000..d885285b --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism.args @@ -0,0 +1,4 @@ +-ex +#-m +-s +-h diff --git a/prism-tests/functionality/export/vector/exportvector.prism.props b/prism-tests/functionality/export/vector/exportvector.prism.props new file mode 100644 index 00000000..ee5082e4 --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism.props @@ -0,0 +1,2 @@ +// RESULT: 1.0 +P=? [ F<=3 x=0 ]; diff --git a/prism-tests/functionality/export/vector/exportvector.prism.props.args b/prism-tests/functionality/export/vector/exportvector.prism.props.args new file mode 100644 index 00000000..f1342bd8 --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism.props.args @@ -0,0 +1 @@ +-const N=3 -exportvector exportvector.prism.props.txt diff --git a/prism-tests/functionality/export/vector/exportvector.prism.props.txt b/prism-tests/functionality/export/vector/exportvector.prism.props.txt new file mode 100644 index 00000000..041417a4 --- /dev/null +++ b/prism-tests/functionality/export/vector/exportvector.prism.props.txt @@ -0,0 +1,7 @@ +0.125 +0.25 +0.625 +1.0 +0.625 +0.25 +0.125 diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index 4fb25030..dbc727f4 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -572,7 +572,6 @@ public class StateModelChecker extends PrismComponent // Clean up //vals.clear(); - result.setVector(vals); // Return result return result; diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 9f30eb72..41ff6de2 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -86,6 +86,7 @@ public class PrismCL implements PrismModelListener private boolean exportresults = false; private boolean exportresultsmatrix = false; private String exportResultsFormat = "plain"; + private boolean exportvector = false; private boolean exportPlainDeprecated = false; private boolean exportModelNoBasename = false; private int exportType = Prism.EXPORT_PLAIN; @@ -140,6 +141,7 @@ public class PrismCL implements PrismModelListener private String exportBSCCsFilename = null; private String exportMECsFilename = null; private String exportResultsFilename = null; + private String exportVectorFilename = null; private String exportSteadyStateFilename = null; private String exportTransientFilename = null; private String exportStratFilename = null; @@ -446,6 +448,24 @@ public class PrismCL implements PrismModelListener } } + // if a results vector was stored, and we need to export it, do so + if (exportvector && res.getVector() != null) { + mainLog.print("\nExporting vector of results for all states "); + mainLog.println(exportVectorFilename.equals("stdout") ? "below:" : "to file \"" + exportVectorFilename + "\"..."); + PrismFileLog tmpLog = new PrismFileLog(exportVectorFilename); + if (!tmpLog.ready()) { + errorAndExit("Couldn't open file \"" + exportVectorFilename + "\" for output"); + } + boolean toStdout = exportVectorFilename.equals("stdout"); + try { + res.getVector().print(tmpLog, false, false, toStdout, toStdout); + } catch (PrismException e) { + error(e.getMessage()); + } + res.getVector().clear(); + tmpLog.close(); + } + // if required, check result against expected value if (test) { doResultTest(propertiesToCheck.get(j), res); @@ -1360,6 +1380,16 @@ public class PrismCL implements PrismModelListener errorAndExit("No file/options specified for -" + sw + " switch"); } } + // export vector of results + else if (sw.equals("exportvector")) { + if (i < args.length - 1) { + exportvector = true; + exportVectorFilename = args[++i]; + prism.setStoreVector(true); + } else { + errorAndExit("No file specified for -" + sw + " switch"); + } + } // export model to explicit file(s) else if (sw.equals("exportmodel")) { if (i < args.length - 1) { diff --git a/prism/src/prism/StateVector.java b/prism/src/prism/StateVector.java index b2da1826..04a29480 100644 --- a/prism/src/prism/StateVector.java +++ b/prism/src/prism/StateVector.java @@ -45,4 +45,9 @@ public interface StateVector * Clear the vector, i.e. free any used memory. */ public void clear(); + + /** + * Print vector to a log/file (non-zero/non-false entries only). + */ + public void print(PrismLog log, boolean printSparse, boolean printMatlab, boolean printStates, boolean printIndices) throws PrismException; }