diff --git a/prism/src/explicit/DTMCEmbeddedSimple.java b/prism/src/explicit/DTMCEmbeddedSimple.java index 2461c241..66f0626b 100644 --- a/prism/src/explicit/DTMCEmbeddedSimple.java +++ b/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"); diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index 9cab7b71..1d3f90e1 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/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 sorted; try { // Output transitions to .tra file - filename = baseFilename + ".tra"; out = new FileWriter(filename); out.write(numStates + " " + numTransitions + "\n"); sorted = new TreeMap(); @@ -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); } diff --git a/prism/src/explicit/DTMCUniformisedSimple.java b/prism/src/explicit/DTMCUniformisedSimple.java index b9d99ac0..3e5afefa 100644 --- a/prism/src/explicit/DTMCUniformisedSimple.java +++ b/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"); diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index cd5660c7..49cdd720 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/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 sorted; try { // Output transitions to .tra file - filename = baseFilename + ".tra"; out = new FileWriter(filename); out.write(numStates + " " + numDistrs + " " + numTransitions + "\n"); sorted = new TreeMap(); @@ -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 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); } diff --git a/prism/src/explicit/Model.java b/prism/src/explicit/Model.java index 694d0891..beaf5a11 100644 --- a/prism/src/explicit/Model.java +++ b/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. */ diff --git a/prism/src/explicit/ModelSimple.java b/prism/src/explicit/ModelSimple.java index e8a26d5c..92286550 100644 --- a/prism/src/explicit/ModelSimple.java +++ b/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 { diff --git a/prism/src/explicit/STPG.java b/prism/src/explicit/STPG.java index 7be9b266..365dcd18 100644 --- a/prism/src/explicit/STPG.java +++ b/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 sorted; try { // Output transitions to .tra file - filename = baseFilename + ".tra"; out = new FileWriter(filename); out.write(numStates + " " + numDistrSets + " " + numDistrs + " " + numTransitions + "\n"); sorted = new TreeMap(); @@ -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); }