Action names included in explicit MDP export to tra file (from prism-qar).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3280 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/MDPSimple.java

@@ -455,6 +455,7 @@ public class MDPSimple extends ModelSimple implements MDP
 	public void exportToPrismExplicitTra(String filename) throws PrismException
 	{
 		int i, j;
+		Object action;
 		FileWriter out;
 		TreeMap<Integer, Double> sorted;
 		try {
@@ -473,7 +474,9 @@ public class MDPSimple extends ModelSimple implements MDP
 					// Print out (sorted) transitions
 					for (Map.Entry<Integer, Double> e : sorted.entrySet()) {
 						// Note use of PrismUtils.formatDouble to match PRISM-exported files
-						out.write(i + " " + j + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue()) + "\n");
+						out.write(i + " " + j + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue()));
+						action = getAction(i, j);
+						out.write(action == null ? "\n" : (" " + action + "\n"));
 					}
 					sorted.clear();
 				}

prism/src/explicit/MDPSparse.java

@@ -493,6 +493,7 @@ public class MDPSparse extends ModelSparse implements MDP
 		// Note: In PRISM .tra files, transitions are usually sorted by column index within choices
 		// (to ensure this is the case, you may need to sort the model when constructing)
 		int i, j, k, l1, h1, l2, h2;
+		Object action;
 		FileWriter out;
 		try {
 			// Output transitions to .tra file
@@ -505,7 +506,9 @@ public class MDPSparse extends ModelSparse implements MDP
 					l2 = choiceStarts[j];
 					h2 = choiceStarts[j + 1];
 					for (k = l2; k < h2; k++) {
-						out.write(i + " " + (j - l1) + " " + cols[k] + " " + PrismUtils.formatDouble(nonZeros[k]) + "\n");
+						out.write(i + " " + (j - l1) + " " + cols[k] + " " + PrismUtils.formatDouble(nonZeros[k]));
+						action = getAction(i, j - l1);
+						out.write(action == null ? "\n" : (" " + action + "\n"));
 					}
 				}
 			}