diff --git a/prism/src/explicit/DTMCSimple.java b/prism/src/explicit/DTMCSimple.java index d9ecaccf..9cab7b71 100644 --- a/prism/src/explicit/DTMCSimple.java +++ b/prism/src/explicit/DTMCSimple.java @@ -307,15 +307,24 @@ public class DTMCSimple extends ModelSimple implements DTMC 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(); for (i = 0; i < numStates; i++) { + // Extract transitions and sort by destination state index (to match PRISM-exported files) for (Map.Entry e : trans.get(i)) { + sorted.put(e.getKey(), e.getValue()); + } + // Print out (sorted) transitions + for (Map.Entry e : sorted.entrySet()) { + // Note use of PrismUtils.formatDouble to match PRISM-exported files out.write(i + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue()) + "\n"); } + sorted.clear(); } out.close(); // Output transition rewards to .trew file diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 43ae30da..cd5660c7 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -404,18 +404,27 @@ public class MDPSimple extends ModelSimple implements MDP 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(); 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 e : distr) { + sorted.put(e.getKey(), e.getValue()); + } + // Print out (sorted) transitions + for (Map.Entry e : sorted.entrySet()) { + // Note use of PrismUtils.formatDouble to match PRISM-exported files out.write(i + " " + j + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue()) + "\n"); } + sorted.clear(); } } out.close(); diff --git a/prism/src/explicit/STPG.java b/prism/src/explicit/STPG.java index f89cd483..7be9b266 100644 --- a/prism/src/explicit/STPG.java +++ b/prism/src/explicit/STPG.java @@ -582,11 +582,13 @@ public class STPG extends ModelSimple 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(); for (i = 0; i < numStates; i++) { j = -1; for (DistributionSet distrs : trans.get(i)) { @@ -594,10 +596,17 @@ public class STPG extends ModelSimple k = -1; for (Distribution distr : distrs) { k++; + // Extract transitions and sort by destination state index (to match PRISM-exported files) for (Map.Entry e : distr) { + sorted.put(e.getKey(), e.getValue()); + } + // Print out (sorted) transitions + for (Map.Entry e : distr) { + // Note use of PrismUtils.formatDouble to match PRISM-exported files out.write(i + " " + j + " " + k + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue()) + "\n"); } + sorted.clear(); } } }