Export to PRISM language from explicit models.

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

prism/src/explicit/CTMCSimple.java

@@ -28,6 +28,8 @@ package explicit;
 
 import java.util.Map;
 
+import prism.ModelType;
+
 /**
  * Simple explicit-state representation of a CTMC.
  */
@@ -70,6 +72,14 @@ public class CTMCSimple extends DTMCSimple implements CTMC
 		super(ctmc, permut);
 	}
 
+	// Accessors (for ModelSimple, overrides DTMCSimple)
+	
+	@Override
+	public ModelType getModelType()
+	{
+		return ModelType.CTMC;
+	}
+
 	// Accessors (for CTMC)
 	
 	@Override

prism/src/explicit/DTMCSimple.java

@@ -376,6 +376,45 @@ public class DTMCSimple extends ModelSimple implements DTMC
 		}
 	}
 
+	@Override
+	public void exportToPrismLanguage(String filename) throws PrismException
+	{
+		int i;
+		boolean first;
+		FileWriter out;
+		TreeMap<Integer, Double> sorted;
+		try {
+			// Output transitions to PRISM language file
+			out = new FileWriter(filename);
+			out.write(getModelType().keyword() + "\n");
+			out.write("module M\nx : [0.." + (numStates-1) + "];\n");
+			sorted = new TreeMap<Integer, Double>();
+			for (i = 0; i < numStates; i++) {
+				// Extract transitions and sort by destination state index (to match PRISM-exported files)
+				for (Map.Entry<Integer, Double> e : trans.get(i)) {
+					sorted.put(e.getKey(), e.getValue());
+				}
+				// Print out (sorted) transitions
+				out.write("[]x=" + i + "->");
+				first = true;
+				for (Map.Entry<Integer, Double> e : sorted.entrySet()) {
+					if (first)
+						first = false;
+					else
+						out.write("+");
+					// Note use of PrismUtils.formatDouble to match PRISM-exported files
+					out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")");
+				}
+				out.write(";\n");
+				sorted.clear();
+			}
+			out.write("endmodule\n");
+			out.close();
+		} catch (IOException e) {
+			throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
+		}
+	}
+
 	@Override
 	public String infoString()
 	{

prism/src/explicit/MDPSimple.java

@@ -500,6 +500,49 @@ public class MDPSimple extends ModelSimple implements MDP
 		}
 	}
 
+	@Override
+	public void exportToPrismLanguage(String filename) throws PrismException
+	{
+		int i, j;
+		boolean first;
+		FileWriter out;
+		TreeMap<Integer, Double> sorted;
+		try {
+			// Output transitions to PRISM language file
+			out = new FileWriter(filename);
+			out.write(getModelType().keyword() + "\n");
+			out.write("module M\nx : [0.." + (numStates-1) + "];\n");
+			sorted = new TreeMap<Integer, Double>();
+			for (i = 0; i < numStates; i++) {
+				j = -1;
+				for (Distribution distr : trans.get(i)) {
+					j++;
+					// Extract transitions and sort by destination state index (to match PRISM-exported files)
+					for (Map.Entry<Integer, Double> e : distr) {
+						sorted.put(e.getKey(), e.getValue());
+					}
+					// Print out (sorted) transitions
+					out.write("[]x=" + i + "->");
+					first = true;
+					for (Map.Entry<Integer, Double> e : sorted.entrySet()) {
+						if (first)
+							first = false;
+						else
+							out.write("+");
+						// Note use of PrismUtils.formatDouble to match PRISM-exported files
+						out.write(PrismUtils.formatDouble(e.getValue()) + ":(x'=" + e.getKey() + ")");
+					}
+					out.write(";\n");
+					sorted.clear();
+				}
+			}
+			out.write("endmodule\n");
+			out.close();
+		} catch (IOException e) {
+			throw new PrismException("Could not export " + getModelType() + " to file \"" + filename + "\"" + e);
+		}
+	}
+
 	@Override
 	public String infoString()
 	{

prism/src/explicit/ModelSimple.java

@@ -140,6 +140,8 @@ public abstract class ModelSimple implements Model
 
 	public abstract void exportToDotFile(String filename, BitSet mark) throws PrismException;
 	
+	public abstract void exportToPrismLanguage(String filename) throws PrismException;
+	
 	public abstract String infoString();
 
 	@Override