diff --git a/prism/src/explicit/MDPSimple.java b/prism/src/explicit/MDPSimple.java index 20b20421..e726f96c 100644 --- a/prism/src/explicit/MDPSimple.java +++ b/prism/src/explicit/MDPSimple.java @@ -455,6 +455,7 @@ public class MDPSimple extends ModelSimple implements MDP public void exportToPrismExplicitTra(String filename) throws PrismException { int i, j; + Object action; FileWriter out; TreeMap sorted; try { @@ -473,7 +474,9 @@ public class MDPSimple extends ModelSimple implements MDP // 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"); + out.write(i + " " + j + " " + e.getKey() + " " + PrismUtils.formatDouble(e.getValue())); + action = getAction(i, j); + out.write(action == null ? "\n" : (" " + action + "\n")); } sorted.clear(); } diff --git a/prism/src/explicit/MDPSparse.java b/prism/src/explicit/MDPSparse.java index 7a4b065d..619b6c16 100644 --- a/prism/src/explicit/MDPSparse.java +++ b/prism/src/explicit/MDPSparse.java @@ -493,6 +493,7 @@ public class MDPSparse extends ModelSparse implements MDP // Note: In PRISM .tra files, transitions are usually sorted by column index within choices // (to ensure this is the case, you may need to sort the model when constructing) int i, j, k, l1, h1, l2, h2; + Object action; FileWriter out; try { // Output transitions to .tra file @@ -505,7 +506,9 @@ public class MDPSparse extends ModelSparse implements MDP l2 = choiceStarts[j]; h2 = choiceStarts[j + 1]; for (k = l2; k < h2; k++) { - out.write(i + " " + (j - l1) + " " + cols[k] + " " + PrismUtils.formatDouble(nonZeros[k]) + "\n"); + out.write(i + " " + (j - l1) + " " + cols[k] + " " + PrismUtils.formatDouble(nonZeros[k])); + action = getAction(i, j - l1); + out.write(action == null ? "\n" : (" " + action + "\n")); } } }