SMG model export (.tra file) + regression tests.

prism-tests/functionality/export/smg/smg_example.prism

@@ -0,0 +1,36 @@
+smg
+
+player p1
+  host, [send1], [send2]
+endplayer
+
+player p2
+  client
+endplayer
+
+module host
+	h : [0..2] init 0;
+	[send1] h=0 -> (h'=1);	// send message 1
+	[send2] h=0 -> (h'=2);  // send message 2
+	[] c=0 -> (h'=0); // restart
+endmodule
+
+module client
+	c : [0..2] init 0;
+	[send1] c=0 -> 0.85 : (c'=1) + 0.15 : (c'=0); // receive message 1
+	[send2] c=0 -> 0.85 : (c'=2) + 0.15 : (c'=0); // receive message 2 
+	[] c!=0 -> (c'=0); // request another message
+	[] c!=0 -> true;   // wait
+endmodule
+
+label "two" = c=2;
+
+rewards "time"
+	true : 1;
+endrewards
+
+rewards "sends"
+	[send1] true : 1;
+	[send2] true : 1;
+endrewards
+

prism-tests/functionality/export/smg/smg_example.prism.exportmodel.auto

@@ -0,0 +1,11 @@
+# Export all model info
+
+-exportmodel smg_example.prism.all -ex
+
+# Export model info separately
+
+-exportmodel smg_example.prism.tra -ex
+-exportmodel smg_example.prism.sta -ex
+-exportmodel smg_example.prism.lab -ex
+-exportmodel smg_example.prism.srew -ex
+-exportmodel smg_example.prism.trew -ex

prism-tests/functionality/export/smg/smg_example.prism.lab

@@ -0,0 +1,3 @@
+0="init" 1="deadlock" 2="two"
+0: 0
+4: 2

prism-tests/functionality/export/smg/smg_example.prism.sta

@@ -0,0 +1,6 @@
+(h,c)
+0:(0,0)
+1:(1,0)
+2:(1,1)
+3:(2,0)
+4:(2,2)

prism-tests/functionality/export/smg/smg_example.prism.tra

@@ -0,0 +1,12 @@
+5:2 9 11
+0:0 0 0 1
+0:0 1 1 0.15 send1
+0:0 1 2 0.85 send1
+0:0 2 3 0.15 send2
+0:0 2 4 0.85 send2
+1:0 0 0 1
+2:1 0 1 1
+2:1 1 2 1
+3:0 0 0 1
+4:1 0 3 1
+4:1 1 4 1

prism-tests/functionality/export/smg/smg_example.prism1.srew

@@ -0,0 +1,8 @@
+# Reward structure "time"
+# State rewards
+5 5
+0 1
+1 1
+2 1
+3 1
+4 1

prism-tests/functionality/export/smg/smg_example.prism1.trew

@@ -0,0 +1,3 @@
+# Reward structure "time"
+# Transition rewards
+5 9 0

prism-tests/functionality/export/smg/smg_example.prism2.srew

@@ -0,0 +1,3 @@
+# Reward structure "sends"
+# State rewards
+5 0

prism-tests/functionality/export/smg/smg_example.prism2.trew

@@ -0,0 +1,7 @@
+# Reward structure "sends"
+# Transition rewards
+5 9 4
+0 1 1 1
+0 1 2 1
+0 2 3 1
+0 2 4 1

prism/src/explicit/SMG.java

@@ -28,13 +28,17 @@
 package explicit;
 
 import java.util.BitSet;
+import java.util.Iterator;
 import java.util.List;
+import java.util.Map;
+import java.util.TreeMap;
 
 import explicit.rewards.SMGRewards;
 import prism.ModelType;
 import prism.PlayerInfo;
 import prism.PlayerInfoOwner;
 import prism.PrismException;
+import prism.PrismLog;
 
 /**
  * Interface for classes that provide (read) access to an explicit-state SMG.
@@ -58,6 +62,33 @@ default ModelType getModelType()
 		return ModelType.SMG;
 	}
 
+	@Override
+	default void exportToPrismExplicitTra(PrismLog out, int precision)
+	{
+		// Output transitions to .tra file
+		int numStates = getNumStates();
+		out.print(numStates + ":" + getNumPlayers() + " " + getNumChoices() + " " + getNumTransitions() + "\n");
+		TreeMap<Integer, Value> sorted = new TreeMap<Integer, Value>();
+		for (int i = 0; i < numStates; i++) {
+			int numChoices = getNumChoices(i);
+			for (int j = 0; j < numChoices; j++) {
+				// Extract transitions and sort by destination state index (to match PRISM-exported files)
+				Iterator<Map.Entry<Integer, Value>> iter = getTransitionsIterator(i, j);
+				while (iter.hasNext()) {
+					Map.Entry<Integer, Value> e = iter.next();
+					sorted.put(e.getKey(), e.getValue());
+				}
+				// Print out (sorted) transitions
+				for (Map.Entry<Integer, Value> e : sorted.entrySet()) {
+					out.print(i + ":" + getPlayer(i) + " " + j + " " + e.getKey() + " " + getEvaluator().toStringExport(e.getValue(), precision));
+					Object action = getAction(i, j);
+					out.print(action == null ? "\n" : (" " + action + "\n"));
+				}
+				sorted.clear();
+			}
+		}
+	}
+
 	// Accessors
 
 	/**