From dc844e2fab23dc227e79e9123bedd7ad0a6b3f00 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 16 Oct 2020 15:43:47 +0100 Subject: [PATCH] Add improved Dot export for LTSs, including action labels. --- prism/src/explicit/LTS.java | 27 ++++++++++++++++++++------- 1 file changed, 20 insertions(+), 7 deletions(-) diff --git a/prism/src/explicit/LTS.java b/prism/src/explicit/LTS.java index d82fffd7..a3d1df96 100644 --- a/prism/src/explicit/LTS.java +++ b/prism/src/explicit/LTS.java @@ -27,8 +27,8 @@ package explicit; import java.util.BitSet; -import java.util.Iterator; +import explicit.graphviz.Decorator; import prism.ModelType; import prism.PrismException; import prism.PrismLog; @@ -53,15 +53,28 @@ public interface LTS extends NondetModel } @Override - default void exportTransitionsToDotFile(int s, PrismLog out, Iterable decorators) + default void exportTransitionsToDotFile(int i, PrismLog out, Iterable decorators) { - for (Iterator it = getSuccessorsIterator(s); it.hasNext(); ) { - Integer successor = it.next(); - // we ignore decorators here - out.println(s + " -> " + successor + ";"); + // Iterate through outgoing transitions (i.e. choices) for this state + int numChoices = getNumChoices(i); + for (int j = 0; j < numChoices; j++) { + Object action = getAction(i, j); + // Print a new dot file line for the arrow for this transition + out.print(i + " -> " + getSuccessor(i, j)); + // Annotate this with the choice index/action + explicit.graphviz.Decoration d = new explicit.graphviz.Decoration(); + d.setLabel(j + (action != null ? ":" + action : "")); + // Apply any other decorators requested + if (decorators != null) { + for (Decorator decorator : decorators) { + d = decorator.decorateTransition(i, j, d); + } + } + // Append to the dot file line + out.println(" " + d.toString() + ";"); } } - + @Override default void exportToPrismLanguage(String filename) throws PrismException {