Add tra file export to ParamModel (but not connected to -exportmodel etc.).

prism/src/param/ParamModel.java

@@ -30,6 +30,8 @@ import java.io.File;
 import java.util.BitSet;
 import java.util.Iterator;
 import java.util.LinkedList;
+import java.util.Map;
+import java.util.TreeMap;
 import java.util.Map.Entry;
 import java.util.TreeSet;
 
@@ -264,12 +266,6 @@ public final class ParamModel extends ModelExplicit implements MDPGeneric<Functi
 		throw new UnsupportedOperationException();
 	}
 
-	@Override
-	public void exportToPrismExplicitTra(String filename) throws PrismException
-	{
-		throw new UnsupportedOperationException();
-	}
-
 	@Override
 	public void exportToPrismExplicitTra(File file) throws PrismException
 	{
@@ -277,9 +273,46 @@ public final class ParamModel extends ModelExplicit implements MDPGeneric<Functi
 	}
 
 	@Override
-	public void exportToPrismExplicitTra(PrismLog log)
-	{
-		throw new UnsupportedOperationException();
+	public void exportToPrismExplicitTra(PrismLog out)
+	{
+		int i, j, numChoices;
+		Object action;
+		TreeMap<Integer, Function> sorted;
+		// Output transitions to .tra file
+		if (modelType.nondeterministic()) {
+			out.print(numStates + " " + getNumChoices() + " " + getNumTransitions() + "\n");
+		} else {
+			out.print(numStates + " " + getNumTransitions() + "\n");
+		}
+		sorted = new TreeMap<Integer, Function>();
+		for (i = 0; i < numStates; i++) {
+			numChoices = getNumChoices(i);
+			for (j = 0; j < numChoices; j++) {
+				// Extract transitions and sort by destination state index (to match PRISM-exported files)
+				Iterator<Map.Entry<Integer, Function>> iter = getTransitionsIterator(i, j);
+				while (iter.hasNext()) {
+					Map.Entry<Integer, Function> e = iter.next();
+					sorted.put(e.getKey(), e.getValue());
+				}
+				// Print out (sorted) transitions
+				for (Map.Entry<Integer, Function> e : sorted.entrySet()) {
+					Object value;
+					if (e.getValue().isConstant()) {
+						value = e.getValue().asBigRational();
+					} else {
+						value = e.getValue();
+					}
+					if (modelType.nondeterministic()) {
+						out.print(i + " " + j + " " + e.getKey() + " " + value);
+					} else {
+						out.print(i + " " + e.getKey() + " " + value);
+					}
+					action = getAction(i, j);
+					out.print(action == null ? "\n" : (" " + action + "\n"));
+				}
+				sorted.clear();
+			}
+		}
 	}
 
 	@Override