From e33c2b1301c87dacfca79acd3ce1574432c3b08e Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sat, 16 Jul 2011 02:12:11 +0000
Subject: [PATCH] Added action names to other MDP explicit exports (dot, PRISM
 lang).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3281 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/MDPSimple.java | 12 ++++++++++--
 prism/src/explicit/MDPSparse.java | 12 ++++++++++--
 prism/src/prism/PrismCL.java      |  1 +
 3 files changed, 21 insertions(+), 4 deletions(-)

diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java
index e726f96c..24867e25 100644
--- a/prism/src/explicit/MDPSimple.java
+++ b/prism/src/explicit/MDPSimple.java
@@ -492,6 +492,7 @@ public class MDPSimple extends ModelSimple implements MDP
 	{
 		int i, j;
 		String nij;
+		Object action;
 		try {
 			FileWriter out = new FileWriter(filename);
 			out.write("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n");
@@ -501,8 +502,12 @@ public class MDPSimple extends ModelSimple implements MDP
 				j = -1;
 				for (Distribution distr : trans.get(i)) {
 					j++;
+					action = getAction(i, j);
 					nij = "n" + i + "_" + j;
-					out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j + "\" ];\n");
+					out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j);
+					if (action != null)
+						out.write(":" + action);
+					out.write("\" ];\n");
 					out.write(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n");
 					for (Map.Entry<Integer, Double> e : distr) {
 						out.write(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\" ];\n");
@@ -523,6 +528,7 @@ public class MDPSimple extends ModelSimple implements MDP
 		boolean first;
 		FileWriter out;
 		TreeMap<Integer, Double> sorted;
+		Object action;
 		try {
 			// Output transitions to PRISM language file
 			out = new FileWriter(filename);
@@ -538,7 +544,9 @@ public class MDPSimple extends ModelSimple implements MDP
 						sorted.put(e.getKey(), e.getValue());
 					}
 					// Print out (sorted) transitions
-					out.write("[]x=" + i + "->");
+					action = getAction(i, j);
+					out.write(action != null ? ("[" + action + "]") : "[]");
+					out.write("x=" + i + "->");
 					first = true;
 					for (Map.Entry<Integer, Double> e : sorted.entrySet()) {
 						if (first)
diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java
index 619b6c16..7ee90ed0 100644
--- a/prism/src/explicit/MDPSparse.java
+++ b/prism/src/explicit/MDPSparse.java
@@ -523,6 +523,7 @@ public class MDPSparse extends ModelSparse implements MDP
 	{
 		int i, j, k, l1, h1, l2, h2;
 		String nij;
+		Object action;
 		try {
 			FileWriter out = new FileWriter(filename);
 			out.write("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n");
@@ -532,8 +533,12 @@ public class MDPSparse extends ModelSparse implements MDP
 				l1 = rowStarts[i];
 				h1 = rowStarts[i + 1];
 				for (j = l1; j < h1; j++) {
+					action = getAction(i, j - l1);
 					nij = "n" + i + "_" + (j - l1);
-					out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + (j - l1) + "\" ];\n");
+					out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j);
+					if (action != null)
+						out.write(":" + action);
+					out.write("\" ];\n");
 					out.write(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n");
 					l2 = choiceStarts[j];
 					h2 = choiceStarts[j + 1];
@@ -554,6 +559,7 @@ public class MDPSparse extends ModelSparse implements MDP
 	{
 		int i, j, k, l1, h1, l2, h2;
 		FileWriter out;
+		Object action;
 		try {
 			// Output transitions to PRISM language file
 			out = new FileWriter(filename);
@@ -564,7 +570,9 @@ public class MDPSparse extends ModelSparse implements MDP
 				h1 = rowStarts[i + 1];
 				for (j = l1; j < h1; j++) {
 					// Print out transitions
-					out.write("[]x=" + i + "->");
+					action = getAction(i, j - l1);
+					out.write(action != null ? ("[" + action + "]") : "[]");
+					out.write("x=" + i + "->");
 					l2 = choiceStarts[j];
 					h2 = choiceStarts[j + 1];
 					for (k = l2; k < h2; k++) {
diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java
index 714b4bc3..bac3b670 100644
--- a/prism/src/prism/PrismCL.java
+++ b/prism/src/prism/PrismCL.java
@@ -884,6 +884,7 @@ public class PrismCL
 		// export transition matrix graph to dot file
 		if (exporttransdot) {
 			try {
+				modelExpl.exportToDotFile(exportTransDotFilename);
 				File f = (exportTransDotFilename.equals("stdout")) ? null : new File(exportTransDotFilename);
 				prism.exportTransToFile(model, exportordered, Prism.EXPORT_DOT, f);
 			}