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; }