From ac4eac3719bd39264a67f19a259735d044481305 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sat, 16 Jul 2011 01:45:40 +0000 Subject: [PATCH] Action names included in explicit MDP export to tra file (from prism-qar). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3280 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/explicit/MDPSimple.java | 5 ++++- prism/src/explicit/MDPSparse.java | 5 ++++- 2 files changed, 8 insertions(+), 2 deletions(-) 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")); } } }