diff --git a/prism/src/param/ParamModel.java b/prism/src/param/ParamModel.java index c2268b3b..711511be 100644 --- a/prism/src/param/ParamModel.java +++ b/prism/src/param/ParamModel.java @@ -30,6 +30,8 @@ import java.io.File; import java.util.BitSet; import java.util.Iterator; import java.util.LinkedList; +import java.util.Map; +import java.util.TreeMap; import java.util.Map.Entry; import java.util.TreeSet; @@ -264,12 +266,6 @@ public final class ParamModel extends ModelExplicit implements MDPGeneric sorted; + // Output transitions to .tra file + if (modelType.nondeterministic()) { + out.print(numStates + " " + getNumChoices() + " " + getNumTransitions() + "\n"); + } else { + out.print(numStates + " " + getNumTransitions() + "\n"); + } + sorted = new TreeMap(); + for (i = 0; i < numStates; i++) { + numChoices = getNumChoices(i); + for (j = 0; j < numChoices; j++) { + // Extract transitions and sort by destination state index (to match PRISM-exported files) + Iterator> iter = getTransitionsIterator(i, j); + while (iter.hasNext()) { + Map.Entry e = iter.next(); + sorted.put(e.getKey(), e.getValue()); + } + // Print out (sorted) transitions + for (Map.Entry e : sorted.entrySet()) { + Object value; + if (e.getValue().isConstant()) { + value = e.getValue().asBigRational(); + } else { + value = e.getValue(); + } + if (modelType.nondeterministic()) { + out.print(i + " " + j + " " + e.getKey() + " " + value); + } else { + out.print(i + " " + e.getKey() + " " + value); + } + action = getAction(i, j); + out.print(action == null ? "\n" : (" " + action + "\n")); + } + sorted.clear(); + } + } } @Override