From 1d6d52f9a7816dba112fddd0c43d49ca9d3fefd4 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 3 Jul 2015 12:58:35 +0000 Subject: [PATCH] Export results in "comment" mode now also shows values of non-ranging contants. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10176 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/parser/Values.java | 10 ++++++++++ prism/src/prism/ResultsCollection.java | 14 ++++++++++++-- prism/src/prism/ResultsExporter.java | 23 +++++++++++++++-------- prism/src/prism/UndefinedConstants.java | 24 ++++++++++++++++++------ 4 files changed, 55 insertions(+), 16 deletions(-) diff --git a/prism/src/parser/Values.java b/prism/src/parser/Values.java index 64e12b0f..8d38adeb 100644 --- a/prism/src/parser/Values.java +++ b/prism/src/parser/Values.java @@ -67,6 +67,16 @@ public class Values //implements Comparable values = (ArrayList)v.values.clone(); } + /** + * Construct a new Values object by merging two existing ones. + * There is no checking for duplicates. + */ + public Values(Values v1, Values v2) + { + this(v1); + addValues(v2); + } + /** * Construct a new Values object by copying existing State object. * Need access to a ModulesFile for variable names. diff --git a/prism/src/prism/ResultsCollection.java b/prism/src/prism/ResultsCollection.java index 9bf30a1d..29357ad8 100644 --- a/prism/src/prism/ResultsCollection.java +++ b/prism/src/prism/ResultsCollection.java @@ -43,6 +43,9 @@ public class ResultsCollection private int numMFRangingConstants; private int numPFRangingConstants; + // Info about other constants (over which these results do *not* range) + private Values nonRangingConstantValues; + // Storage of the actual results private TreeNode root; private int currentIteration = 0; @@ -69,7 +72,8 @@ public class ResultsCollection rangingConstants.add(tmpRangingConstants.get(i)); } numMFRangingConstants = uCons.getNumModelRangingConstants(); - numPFRangingConstants = uCons.getNumPropertyRangingConstants(); + numPFRangingConstants = uCons.getNumPropertyRangingConstants(); + nonRangingConstantValues = uCons.getNonRangingConstantValues(); this.root = (rangingConstants.size() > 0) ? new TreeNode(0) : new TreeLeaf(); this.resultName = (resultName == null) ? "Result" : resultName; @@ -95,6 +99,11 @@ public class ResultsCollection return numPFRangingConstants; } + public Values getNonRangingConstantValues() + { + return nonRangingConstantValues; + } + public boolean addResultListener(ResultListener resultListener) { return resultListeners.add(resultListener); @@ -280,7 +289,8 @@ public class ResultsCollection */ public ResultsExporter export(ResultsExporter exporter) { - exporter.setConstantsInfo(rangingConstants); + exporter.setRangingConstants(rangingConstants); + exporter.setNonRangingConstantValues(nonRangingConstantValues); exporter.start(); root.export(exporter); exporter.end(); diff --git a/prism/src/prism/ResultsExporter.java b/prism/src/prism/ResultsExporter.java index 07e53910..851570d2 100644 --- a/prism/src/prism/ResultsExporter.java +++ b/prism/src/prism/ResultsExporter.java @@ -93,7 +93,8 @@ public class ResultsExporter } }; - private List constants; + private List rangingConstants; + private Values nonRangingConstantValues; private Property property; private ResultsExportFormat format = ResultsExportFormat.PLAIN; @@ -170,9 +171,14 @@ public class ResultsExporter this.equals = equals; }*/ - public void setConstantsInfo(final List constants) + public void setRangingConstants(final List rangingConstants) { - this.constants = constants; + this.rangingConstants = rangingConstants; + } + + public void setNonRangingConstantValues(final Values nonRangingConstantValues) + { + this.nonRangingConstantValues = nonRangingConstantValues; } public void setProperty(final Property property) @@ -215,12 +221,12 @@ public class ResultsExporter } } // Print header, if needed - if (printHeader && constants != null) { - for (int i = 0; i < constants.size(); i++) { + if (printHeader && rangingConstants != null) { + for (int i = 0; i < rangingConstants.size(); i++) { if (i > 0) { exportString += separator; } - exportString += constants.get(i).getName(); + exportString += rangingConstants.get(i).getName(); } exportString += equals + "Result\n"; } @@ -237,9 +243,10 @@ public class ResultsExporter exportString += values.toString(printNames, separator) + equals + result + "\n"; break; case COMMENT: + Values mergedValues = new Values(nonRangingConstantValues, values); exportString += "// RESULT"; - if (values.getNumValues() > 0) { - exportString += " (" + values.toString(true, ",") + ")"; + if (mergedValues.getNumValues() > 0) { + exportString += " (" + mergedValues.toString(true, ",") + ")"; } exportString += ": " + result + "\n"; } diff --git a/prism/src/prism/UndefinedConstants.java b/prism/src/prism/UndefinedConstants.java index c17fef1c..29887631 100644 --- a/prism/src/prism/UndefinedConstants.java +++ b/prism/src/prism/UndefinedConstants.java @@ -710,14 +710,11 @@ public class UndefinedConstants */ public Vector getRangingConstants() { - int i; - Vector res; - - res = new Vector(); - for (i = 0; i < mfNumConsts; i++) + Vector res = new Vector(); + for (int i = 0; i < mfNumConsts; i++) if (mfConsts.get(i).getNumSteps() > 1) res.addElement(mfConsts.get(i)); - for (i = 0; i < pfNumConsts; i++) + for (int i = 0; i < pfNumConsts; i++) if (pfConsts.get(i).getNumSteps() > 1) res.addElement(pfConsts.get(i)); @@ -799,4 +796,19 @@ public class UndefinedConstants { return pfValues; } + + /** + * Get the values for non-ranging model constants, i.e. each constant that has range 1. + */ + public Values getNonRangingConstantValues() + { + Values vals = new Values(); + for (int i = 0; i < mfNumConsts; i++) + if (mfConsts.get(i).getNumSteps() == 1) + vals.addValue(mfConsts.get(i).getName(), mfConsts.get(i).getValue()); + for (int i = 0; i < pfNumConsts; i++) + if (pfConsts.get(i).getNumSteps() == 1) + vals.addValue(pfConsts.get(i).getName(), pfConsts.get(i).getValue()); + return vals; + } }