Explicit model export has option to just do tra file.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1850 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/DTMCEmbeddedSimple.java

@@ -133,6 +133,11 @@ public class DTMCEmbeddedSimple implements DTMC
 		throw new PrismException("Export not yet supported");
 	}
 
+	public void exportToPrismExplicitTra(String filename) throws PrismException
+	{
+		throw new PrismException("Export not yet supported");
+	}
+
 	public void exportToDotFile(String filename) throws PrismException
 	{
 		throw new PrismException("Export not yet supported");

prism/src/explicit/DTMCSimple.java

@@ -303,14 +303,19 @@ public class DTMCSimple extends ModelSimple implements DTMC
 
 	@Override
 	public void exportToPrismExplicit(String baseFilename) throws PrismException
+	{
+		exportToPrismExplicitTra(baseFilename + ".tra");
+		// TODO: Output transition rewards to .trew file, etc.
+	}
+
+	@Override
+	public void exportToPrismExplicitTra(String filename) throws PrismException
 	{
 		int i;
-		String filename = null;
 		FileWriter out;
 		TreeMap<Integer, Double> sorted;
 		try {
 			// Output transitions to .tra file
-			filename = baseFilename + ".tra";
 			out = new FileWriter(filename);
 			out.write(numStates + " " + numTransitions + "\n");
 			sorted = new TreeMap<Integer, Double>();
@@ -327,9 +332,6 @@ public class DTMCSimple extends ModelSimple implements DTMC
 				sorted.clear();
 			}
 			out.close();
-			// Output transition rewards to .trew file
-			// TODO
-			out.close();
 		} catch (IOException e) {
 			throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
 		}

prism/src/explicit/DTMCUniformisedSimple.java

@@ -144,6 +144,11 @@ public class DTMCUniformisedSimple implements DTMC
 		throw new PrismException("Export not yet supported");
 	}
 
+	public void exportToPrismExplicitTra(String filename) throws PrismException
+	{
+		throw new PrismException("Export not yet supported");
+	}
+
 	public void exportToDotFile(String filename) throws PrismException
 	{
 		throw new PrismException("Export not yet supported");

prism/src/explicit/MDPSimple.java

@@ -399,15 +399,13 @@ public class MDPSimple extends ModelSimple implements MDP
 	}
 
 	@Override
-	public void exportToPrismExplicit(String baseFilename) throws PrismException
+	public void exportToPrismExplicitTra(String filename) throws PrismException
 	{
 		int i, j;
-		String filename = null;
 		FileWriter out;
 		TreeMap<Integer, Double> sorted;
 		try {
 			// Output transitions to .tra file
-			filename = baseFilename + ".tra";
 			out = new FileWriter(filename);
 			out.write(numStates + " " + numDistrs + " " + numTransitions + "\n");
 			sorted = new TreeMap<Integer, Double>();
@@ -428,21 +426,6 @@ public class MDPSimple extends ModelSimple implements MDP
 				}
 			}
 			out.close();
-			// Output transition rewards to .trew file
-			// TODO
-			filename = baseFilename + ".trew";
-			out = new FileWriter(filename);
-			out.write(numStates + " " + "?" + " " + "?" + "\n");
-			for (i = 0; i < numStates; i++) {
-				j = -1;
-				for (Distribution distr : trans.get(i)) {
-					j++;
-					for (Map.Entry<Integer, Double> e : distr) {
-						out.write(i + " " + j + " " + e.getKey() + " " + "1.0" + "\n");
-					}
-				}
-			}
-			out.close();
 		} catch (IOException e) {
 			throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
 		}

prism/src/explicit/Model.java

@@ -115,6 +115,11 @@ public interface Model
 	 */
 	public void exportToPrismExplicit(String baseFilename) throws PrismException;
 
+	/**
+	 * Export transition matrix to explicit format readable by PRISM (i.e. a .tra file).
+	 */
+	public void exportToPrismExplicitTra(String traFilename) throws PrismException;
+
 	/**
 	 * Export to a dot file.
 	 */

prism/src/explicit/ModelSimple.java

@@ -122,7 +122,16 @@ public abstract class ModelSimple implements Model
 	
 	public abstract void checkForDeadlocks(BitSet except) throws PrismException;
 	
-	public abstract void exportToPrismExplicit(String baseFilename) throws PrismException;
+	@Override
+	public void exportToPrismExplicit(String baseFilename) throws PrismException
+	{
+		// Default implementation - just output .tra file
+		// (some models might override this)
+		exportToPrismExplicitTra(baseFilename + ".tra");
+		// TODO: Also output transition rewards to .trew file, etc.
+	}
+
+	public abstract void exportToPrismExplicitTra(String filename) throws PrismException;
 
 	public void exportToDotFile(String filename) throws PrismException
 	{

prism/src/explicit/STPG.java

@@ -574,18 +574,14 @@ public class STPG extends ModelSimple
 		exportToDotFile(filename, null);
 	}
 
-	/**
-	 * Export to explicit format readable by PRISM (i.e. a .tra file, etc.).
-	 */
-	public void exportToPrismExplicit(String baseFilename) throws PrismException
+	@Override
+	public void exportToPrismExplicitTra(String filename) throws PrismException
 	{
 		int i, j, k;
-		String filename = null;
 		FileWriter out;
 		TreeMap<Integer, Double> sorted;
 		try {
 			// Output transitions to .tra file
-			filename = baseFilename + ".tra";
 			out = new FileWriter(filename);
 			out.write(numStates + " " + numDistrSets + " " + numDistrs + " " + numTransitions + "\n");
 			sorted = new TreeMap<Integer, Double>();
@@ -611,7 +607,6 @@ public class STPG extends ModelSimple
 				}
 			}
 			out.close();
-			// TODO: rewards
 		} catch (IOException e) {
 			throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
 		}