From 030aa4d0d87d1a22662cb486a9288947a65816dd Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 19 Aug 2016 09:45:33 +0000
Subject: [PATCH] ParamModel: support DOT output

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11649 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/param/ParamModel.java | 54 +++++++++++++++++++--------------
 1 file changed, 32 insertions(+), 22 deletions(-)

diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java
index 72ad5b83..0e091803 100644
--- a/prism/src/param/ParamModel.java
+++ b/prism/src/param/ParamModel.java
@@ -236,34 +236,44 @@ final class ParamModel extends ModelExplicit
 		throw new UnsupportedOperationException();
 	}
 
-	@Override
-	public void exportToDotFile(String filename) throws PrismException
-	{
-		throw new UnsupportedOperationException();
-	}
 
 	@Override
-	public void exportToDotFile(String filename, BitSet mark) throws PrismException
+	protected void exportTransitionsToDotFile(int i, PrismLog out)
 	{
-		throw new UnsupportedOperationException();
-	}
+		int numChoices = getNumChoices(i);
+		for (int j = 0; j < numChoices; j++) {
+			// action = getAction(i, j);
+			String nij = null;
+			if (modelType.nondeterministic()) {
+				nij = "n" + i + "_" + j;
+				out.print(i + " -> " + nij + " [ arrowhead=none,label=\"" + j);
+				out.print("\" ];\n");
+				out.print(nij + " [ shape=point,width=0.1,height=0.1,label=\"\" ];\n");
+			}
 
-	@Override
-	public void exportToDotFile(PrismLog out)
-	{
-		throw new UnsupportedOperationException();
-	}
+			Iterator<Entry<Integer, Function>> it = getTransitionsIterator(i, j);
+			while (it.hasNext()) {
+				Entry<Integer, Function> e = it.next();
 
-	@Override
-	public void exportToDotFile(PrismLog out, BitSet mark)
-	{
-		throw new UnsupportedOperationException();
-	}
+				// Note: For CTMCs, param stores the embedded DTMC, so we output that
 
-	@Override
-	protected void exportTransitionsToDotFile(int i, PrismLog out)
-	{
-		throw new UnsupportedOperationException();
+				if (!modelType.nondeterministic()) {
+					out.print(i + " -> " + e.getKey() + " ");
+				} else {
+					out.print(nij + " -> " + e.getKey() + " ");
+				}
+
+				String value;
+				if (e.getValue().isConstant()) {
+					value = e.getValue().asBigRational().toString();
+				} else {
+					value = e.getValue().toString();
+				}
+
+				
+				out.print("[ label=\"" + value + "\" ];\n");
+			}
+		}
 	}
 	
 	@Override