From d7e06f569edd4d7e492e99f81f05104d9cbd65e7 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 25 Jan 2012 10:21:15 +0000
Subject: [PATCH] Improvements/fixes to export of results in matrix form: -
 header now printed for 1D matrix (only 1 const) - no extra column for 1D
 matrix - matrices preceded by constant values/index names

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4475 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/ResultsCollection.java | 50 ++++++++++++++++++++------
 1 file changed, 39 insertions(+), 11 deletions(-)

diff --git a/prism/src/prism/ResultsCollection.java b/prism/src/prism/ResultsCollection.java
index 267e5c67..7d85deff 100644
--- a/prism/src/prism/ResultsCollection.java
+++ b/prism/src/prism/ResultsCollection.java
@@ -516,30 +516,58 @@ public class ResultsCollection
 		 */
 		public String toStringMatrix(String sep)
 		{
-			return toStringMatrixRec(sep);
+			return toStringMatrixRec(sep, "");
 		}
 
-		public String toStringMatrixRec(String sep)
+		public String toStringMatrixRec(String sep, String head)
 		{
 			int i, n;
 			String res;
 
 			res = "";
 			n = constant.getNumSteps();
+			
+			// Print constants/indices for matrix
+			// NB: need to enclose in quotes for CSV
+			if (rangingConstants.size() == 1 || rangingConstants.size() - level == 2) {
+				if (sep.equals(", "))
+					res += "\"";
+				if (rangingConstants.size() > 2)
+					res += head+", ";
+				if (rangingConstants.size() == 1)
+					res += constant.getName() + ":";
+				else
+					res += constant.getName() + "\\" + kids[0].constant.getName() + ":";
+				if (sep.equals(", "))
+					res += "\"";
+				res += "\n";
+			}
 			// Print top row of values
-			if (rangingConstants.size() - level == 2 && n > 0) {
-				TreeNode child = kids[0];
-				int nChild = child.constant.getNumSteps();
-				for (i = 0; i < nChild; i++) {
-					res += sep + child.constant.getValue(i);
+			if (rangingConstants.size() == 1 || rangingConstants.size() - level == 2) {
+				TreeNode node = rangingConstants.size() == 1 ? this : kids[0];
+				int nSteps = node.constant.getNumSteps();
+				for (i = 0; i < nSteps; i++) {
+					res += sep + node.constant.getValue(i);
 				}
 				res += "\n";
 			}
 			for (i = 0; i < n; i++) {
 				// Print first item of row: value
 				if (rangingConstants.size() - level == 2)
-					res += constant.getValue(i);
-				res += kids[i].toStringMatrixRec(sep);
+					res += constant.getValue(i) + sep;
+				// Print separator between row elements 
+				if (rangingConstants.size() - level == 1 && i > 0)
+					res += sep;
+				// Recurse
+				if (rangingConstants.size() - level <= 2) {
+					res += kids[i].toStringMatrixRec(sep, head);
+				} else {
+					String headNew = head;
+					if (!("".equals(head)))
+						headNew += ",";
+					headNew += constant.getName() + "=" + constant.getValue(i);
+					res += kids[i].toStringMatrixRec(sep, headNew);
+				}
 				// Print new line after row (except last one)
 				if ((rangingConstants.size() - level == 2) && i < n - 1)
 					res += "\n";
@@ -568,9 +596,9 @@ public class ResultsCollection
 			return val;
 		}
 
-		public String toStringMatrixRec(String sep)
+		public String toStringMatrixRec(String sep, String head)
 		{
-			return sep + val;
+			return val.toString();
 		}
 
 		public String toStringRec(boolean pv, String sep, String eq, String head)