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

@@ -67,6 +67,16 @@ public class Values //implements Comparable
 		values = (ArrayList<Object>)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.

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();

prism/src/prism/ResultsExporter.java

@@ -93,7 +93,8 @@ public class ResultsExporter
 		}
 	};
 
-	private List<DefinedConstant> constants;
+	private List<DefinedConstant> 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<DefinedConstant> constants)
+	public void setRangingConstants(final List<DefinedConstant> 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";
 		}

prism/src/prism/UndefinedConstants.java

@@ -710,14 +710,11 @@ public class UndefinedConstants
 	 */
 	public Vector<DefinedConstant> getRangingConstants()
 	{
-		int i;
-		Vector<DefinedConstant> res;
-
-		res = new Vector<DefinedConstant>();
-		for (i = 0; i < mfNumConsts; i++)
+		Vector<DefinedConstant> res = new Vector<DefinedConstant>();
+		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;
+	}
 }