From bd4b2f3f3a88f4e5b32904a33c984a1f7c29c2c6 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 22 Mar 2012 22:50:55 +0000
Subject: [PATCH] New exportToDotFileWithAdv method for MDPs in explicit
 engine.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4935 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/explicit/MDP.java         |  7 +++++
 prism/src/explicit/MDPExplicit.java | 41 +++++++++++++++++++++++++++--
 2 files changed, 46 insertions(+), 2 deletions(-)

diff --git a/prism/src/explicit/MDP.java b/prism/src/explicit/MDP.java
index b70724e2..b9b31fb5 100644
--- a/prism/src/explicit/MDP.java
+++ b/prism/src/explicit/MDP.java
@@ -29,6 +29,8 @@ package explicit;
 import java.util.*;
 import java.util.Map.Entry;
 
+import prism.PrismException;
+
 import explicit.rewards.*;
 
 /**
@@ -234,4 +236,9 @@ public interface MDP extends Model
 	 * @param dest Vector to write result to.
 	 */
 	public void mvMultRight(int[] states, int[] adv, double[] source, double[] dest);
+
+	/**
+	 * Export to a dot file, highlighting states in 'mark' and choices for a (memoryless) adversary.
+	 */
+	public void exportToDotFileWithAdv(String filename, BitSet mark, int adv[]) throws PrismException;
 }
diff --git a/prism/src/explicit/MDPExplicit.java b/prism/src/explicit/MDPExplicit.java
index 567ea3c7..2dc226be 100644
--- a/prism/src/explicit/MDPExplicit.java
+++ b/prism/src/explicit/MDPExplicit.java
@@ -42,7 +42,7 @@ import prism.PrismUtils;
 public abstract class MDPExplicit extends ModelExplicit implements MDP
 {
 	// Accessors (for Model)
-	
+
 	@Override
 	public ModelType getModelType()
 	{
@@ -136,6 +136,43 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP
 		}
 	}
 
+	@Override
+	public void exportToDotFileWithAdv(String filename, BitSet mark, int adv[]) throws PrismException
+	{
+		int i, j, numChoices;
+		String nij;
+		Object action;
+		String style;
+		try {
+			FileWriter out = new FileWriter(filename);
+			out.write("digraph " + getModelType() + " {\nsize=\"8,5\"\nnode [shape=box];\n");
+			for (i = 0; i < numStates; i++) {
+				if (mark != null && mark.get(i))
+					out.write(i + " [style=filled  fillcolor=\"#cccccc\"]\n");
+				numChoices = getNumChoices(i);
+				for (j = 0; j < numChoices; j++) {
+					style = (adv[i] == j) ? ",color=\"#ff0000\",fontcolor=\"#ff0000\"" : "";
+					action = getAction(i, j);
+					nij = "n" + i + "_" + j;
+					out.write(i + " -> " + nij + " [ arrowhead=none,label=\"" + j);
+					if (action != null)
+						out.write(":" + action);
+					out.write("\"" + style + " ];\n");
+					out.write(nij + " [ shape=point,height=0.1,label=\"\"" + style + " ];\n");
+					Iterator<Map.Entry<Integer, Double>> iter = getTransitionsIterator(i, j);
+					while (iter.hasNext()) {
+						Map.Entry<Integer, Double> e = iter.next();
+						out.write(nij + " -> " + e.getKey() + " [ label=\"" + e.getValue() + "\"" + style + " ];\n");
+					}
+				}
+			}
+			out.write("}\n");
+			out.close();
+		} catch (IOException e) {
+			throw new PrismException("Could not write " + getModelType() + " to file \"" + filename + "\"" + e);
+		}
+	}
+
 	@Override
 	public void exportToPrismLanguage(String filename) throws PrismException
 	{
@@ -258,7 +295,7 @@ public abstract class MDPExplicit extends ModelExplicit implements MDP
 				result[s] = mvMultRewMinMaxSingle(s, vect, mdpRewards, min, adv);
 		}
 	}
-	
+
 	@Override
 	public double mvMultRewGSMinMax(double vect[], MDPRewards mdpRewards, boolean min, BitSet subset, boolean complement, boolean absolute)
 	{