From b34d66cc1793c68ac4e253c1227e46574abe99f7 Mon Sep 17 00:00:00 2001
From: Chris Novakovic <c.novakovic@cs.bham.ac.uk>
Date: Mon, 1 Oct 2018 22:07:17 +0100
Subject: [PATCH] explicit.graphviz: generate HTML-like node/edge labels

Graphviz implements a subset of HTML that can be used in node and edge
labels (see https://graphviz.gitlab.io/_pages/doc/info/shapes.html#html
for a description of the subset) as an alternative to the plain-text
default style. The HTML-like style uses different attribute value
delimiters (<>) to the plain text style (""), but the latter is
hardcoded in explicit.graphviz.Decoration. The line delimiters also
differ (<br/> and \n respectively).

Provide support for both plain text and HTML-like labels in Decorator;
the label type can be changed by calling setLabelType() before appending
any label content via labelAddBelow() or labelAddAbove().
---
 prism/src/explicit/graphviz/Decoration.java | 50 +++++++++++++++++++--
 1 file changed, 47 insertions(+), 3 deletions(-)

diff --git a/prism/src/explicit/graphviz/Decoration.java b/prism/src/explicit/graphviz/Decoration.java
index 11d45a99..e3bc62b9 100644
--- a/prism/src/explicit/graphviz/Decoration.java
+++ b/prism/src/explicit/graphviz/Decoration.java
@@ -27,6 +27,7 @@
 package explicit.graphviz;
 
 import java.util.Collections;
+import java.util.EnumMap;
 import java.util.Map;
 import java.util.Map.Entry;
 import java.util.TreeMap;
@@ -37,8 +38,32 @@ import java.util.TreeMap;
  */
 public class Decoration
 {
+	/** An indication of how the node or edge's label should be rendered by Graphviz */
+	public enum LabelType
+	{
+		/**
+		 * Plain text
+		 * */
+		PLAIN,
+		/**
+		 * HTML-like (a restricted subset of HTML supported by Graphviz, as documented in the
+		 * <a href="https://graphviz.gitlab.io/_pages/doc/info/shapes.html#html">Node Shapes</a>
+		 * section of the Graphviz manual)
+		 */
+		 HTML
+	}
+
+	private static final EnumMap<LabelType, String[]> LABEL_DELIMITERS = new EnumMap<>(LabelType.class);
+	static
+	{
+		LABEL_DELIMITERS.put(LabelType.PLAIN, new String[]{ "\"", "\\n", "\"" });
+		LABEL_DELIMITERS.put(LabelType.HTML, new String[]{ "<", "<br/>", ">" });
+	}
+
 	/** The label */
 	private String label;
+	/** How the label should be rendered by Graphviz (by plain text, as default) */
+	private LabelType labelType = LabelType.PLAIN;
 	/** Map from attribute keys to values (apart from the label attribute) */
 	private TreeMap<String, String> attributes;
 
@@ -114,7 +139,8 @@ public class Decoration
 	{
 		StringBuffer buf = new StringBuffer();
 
-		append(buf, "label", "\"" + label + "\"");
+		String[] delimiters = LABEL_DELIMITERS.get(labelType);
+		append(buf, "label", delimiters[0] + label + delimiters[2]);
 
 		for (Entry<String, String> e : attributesRO().entrySet()) {
 			if (defaults != null) {
@@ -160,10 +186,27 @@ public class Decoration
 		this.label = label;
 	}
 
+	/** Get the label type */
+	public LabelType getLabelType()
+	{
+		return labelType;
+	}
+
+	/**
+	 * Set the label type (this should be done before calling the {@link labelAddBelow(String) labelAddBelow}
+	 * or {@link labelAddAbove(String) labelAddAbove} methods, to ensure that the correct line delimiter is
+	 * inserted)
+	 */
+	public void setLabelType(LabelType labelType)
+	{
+		this.labelType = labelType;
+	}
+
 	/** Add some additional information below the currently existing label */
 	public void labelAddBelow(String additional)
 	{
-		setLabel(getLabel() + "\\n" + additional);
+		String[] delimiters = LABEL_DELIMITERS.get(labelType);
+		setLabel(getLabel() + delimiters[1] + additional);
 	}
 
 	/**
@@ -172,7 +215,8 @@ public class Decoration
 	 */
 	public void labelAddAbove(String additional)
 	{
-		setLabel(additional + "\\n" + getLabel());
+		String[] delimiters = LABEL_DELIMITERS.get(labelType);
+		setLabel(additional + delimiters[1] + getLabel());
 	}
 
 	/**