explicit.graphviz: infrastructure for more flexible DOT exports

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12114 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/explicit/graphviz/Decoration.java

@@ -0,0 +1,198 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit.graphviz;
+
+import java.util.Collections;
+import java.util.Map;
+import java.util.Map.Entry;
+import java.util.TreeMap;
+
+/**
+ * A Decoration stores the attributes (label and style information)
+ * that can be attached to a GraphViz node or edge.
+ */
+public class Decoration
+{
+	/** The label */
+	private String label;
+	/** Map from attribute keys to values (apart from the label attribute) */
+	private TreeMap<String, String> attributes;
+
+	/** A Decoration that provides default attributes, e.g., node shape */
+	private Decoration defaults;
+
+	/** Constructor, no defaults */
+	public Decoration()
+	{
+		this.defaults = null;
+		this.label = "";
+	}
+
+	/** Constructor, with defaults decoration */
+	public Decoration(Decoration defaults)
+	{
+		this.defaults = defaults;
+	}
+
+	/**
+	 * Returns a map for accessing attributes (apart from the label attribute)
+	 */
+	public Map<String, String> attributes()
+	{
+		if (attributes == null) {
+			// If there have been no attributes before, initialise empty map
+			attributes = new TreeMap<String, String>();
+		}
+		return attributes;
+	}
+
+	/**
+	 * Returns a read-only map for accessing attributes (apart from the label attribute).
+	 * <br>
+	 * Note: If you only need read access, it might be more efficient to use this
+	 * method instead of {@code attributes()}.
+	 */
+	public Map<String, String> attributesRO()
+	{
+		if (attributes == null) {
+			// If there have been no attributes before, return empty map
+			return Collections.emptyMap();
+		} else {
+			return Collections.unmodifiableMap(attributes);
+		}
+	}
+
+	/**
+	 * Get the effective value for the given key.
+	 * <br>
+	 * If the key equals "label", returns the label.
+	 * Otherwise, if there is an attribute with the given key,
+	 * return its value. If there is none, try the defaults
+	 * decoration.
+	 * @param key the attribute key
+	 * @return the value, if there is one ({@code null} otherwise)
+	 */
+	public String getEffectiveValue(String key)
+	{
+		if (key.equals("label")) {
+			return label;
+		}
+
+		String value = attributesRO().get(key);
+		if (value == null && defaults != null) {
+			return defaults.getEffectiveValue(key);
+		}
+		return value;
+	}
+
+	@Override
+	public String toString()
+	{
+		StringBuffer buf = new StringBuffer();
+
+		append(buf, "label", "\"" + label + "\"");
+
+		for (Entry<String, String> e : attributesRO().entrySet()) {
+			if (defaults != null) {
+				String defaultValue = defaults.getEffectiveValue(e.getKey());
+				if (defaultValue != null && defaultValue.equals(e.getValue())) {
+					// skip, as it's the default value and we don't want to pollute the output
+					continue;
+				}
+			}
+
+			String value = e.getValue();
+			value = "\"" + value + "\"";
+			append(buf, e.getKey(), value);
+		}
+
+		if (buf.length() == 0) {
+			return "";
+		} else {
+			return "[" + buf.toString() + "]";
+		}
+	}
+
+	/** Append the given key/value pair to the StringBuffer, with a ',' if necessary */
+	protected void append(StringBuffer buffer, String key, String value)
+	{
+		if (buffer.length() != 0) {
+			buffer.append(",");
+		}
+		buffer.append(key);
+		buffer.append("=");
+		buffer.append(value);
+	}
+
+	/** Get the label */
+	public String getLabel()
+	{
+		return label;
+	}
+
+	/** Set the label */
+	public void setLabel(String label)
+	{
+		this.label = label;
+	}
+
+	/** Add some additional information below the currently existing label */
+	public void labelAddBelow(String additional)
+	{
+		setLabel(getLabel() + "\\n" + additional);
+	}
+
+	/**
+	 * Add some additional information above the currently existing label.
+	 * @param additional the additional text
+	 */
+	public void labelAddAbove(String additional)
+	{
+		setLabel(additional + "\\n" + getLabel());
+	}
+
+	/**
+	 * Add some additional information to the right of the currently existing label.
+	 * @param additional the additional text
+	 * @param separator the separator between the old label and the additional text (may be {@code null})
+	 */
+	public void labelAddRight(String additional, String separator)
+	{
+		setLabel(getLabel() + (separator == null ? " " : separator) + additional);
+	}
+
+	/**
+	 * Add some additional information to the left of the currently existing label.
+	 * @param additional the additional text
+	 * @param separator the separator between the old label and the additional text (may be {@code null})
+	 */
+	public void labelAddLeft(String additional, String separator)
+	{
+		setLabel(additional + (separator == null ? " " : separator) + getLabel());
+	}
+
+}

prism/src/explicit/graphviz/Decorator.java

@@ -0,0 +1,109 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit.graphviz;
+
+import java.util.BitSet;
+
+/**
+ * A Decorator is called from the DOT output routines and
+ * can modify the decoration that is attached at the
+ * given node or edge in the GraphViz file.
+ * <br>
+ * Default implementations are provided that simply pass
+ * through the decoration given as input, without any modification.
+ */
+public interface Decorator
+{
+	/**
+	 * Called to allow modification of the decoration
+	 * attached to a state.
+	 * @param state the state index in the model
+	 * @param d the current decoration
+	 * @return an updated decoration (may return {@code d} and modify it)
+	 */
+	default Decoration decorateState(int state, Decoration d)
+	{
+		return d;
+	}
+
+	/**
+	 * Called to allow modification of the decoration
+	 * attached to non-deterministic transition choice.
+	 * @param from the state index in the model of the originating state
+	 * @param choice the choice index
+	 * @param d the current decoration
+	 * @return an updated decoration (may return {@code d} and modify it)
+	 */
+	default Decoration decorateTransition(int from, int choice, Decoration d)
+	{
+		return d;
+	}
+
+	/**
+	 * Called to allow modification of the decoration
+	 * attached to a probabilistic transition for a non-deterministic choice.
+	 * @param from the state index in the model of the originating state
+	 * @param to the state index in the model of the target state
+	 * @param choice the choice index
+	 * @param probability the probability (e.g., a Double, param.BigRational, param.Function)
+	 * @param d the current decoration
+	 * @return an updated decoration (may return {@code d} and modify it)
+	 */
+	default Decoration decorateProbability(int from, int to, int choice, Object probability, Decoration d)
+	{
+		return d;
+	}
+
+	/**
+	 * Called to allow modification of the decoration
+	 * attached to a probabilistic transition in a model without non-deterministic choices (e.g., DTMC, CTMC).
+	 * @param from the state index in the model of the originating state
+	 * @param to the state index in the model of the target state
+	 * @param probability the probability (e.g., a Double, param.BigRational, param.Function)
+	 * @param d the current decoration
+	 * @return an updated decoration (may return {@code d} and modify it)
+	 */
+	default Decoration decorateProbability(int from, int to, Object probability, Decoration d)
+	{
+		return d;
+	}
+
+	/**
+	 * Called to allow modification of the decoration
+	 * attached to an automaton edge.
+	 * @param from the state index in the automaton of the originating state
+	 * @param to the state index in the automaton of the target state
+	 * @param apElement a BitSet representing the current element of the alphabet (2^AP)
+	 * @param d the current decoration
+	 * @return an updated decoration (may return {@code d} and modify it)
+	 */
+	default Decoration decorateAutomatonEdge(int from, int to, BitSet apElement, Decoration d)
+	{
+		return d;
+	}
+
+}

prism/src/explicit/graphviz/MarkStateSetDecorator.java

@@ -0,0 +1,76 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit.graphviz;
+
+import java.util.BitSet;
+
+/**
+ * A decorator for states: Given a BitSet of state indizes, fills
+ * the nodes corresponding to these states with a given color.
+ */
+public class MarkStateSetDecorator implements Decorator
+{
+	/** The set of states to be marked */
+	private BitSet stateSet;
+	/** The fill colour for the node */
+	private String fillColour = "#cccccc";
+
+	/**
+	 * Constructor, default colour grey.
+	 * @param stateSet the set of state indices to be marked.
+	 */
+	public MarkStateSetDecorator(BitSet stateSet)
+	{
+		this.stateSet = stateSet;
+	}
+
+	/**
+	 * Constructor, default colour grey.
+	 * @param stateSet the set of state indices to be marked.
+	 * @param fillColor HTML colour string for the fill colour
+	 */
+	public MarkStateSetDecorator(BitSet set, String fillColor)
+	{
+		this.stateSet = set;
+		this.fillColour = fillColor;
+	}
+
+	/**
+	 * Add "style=filled" and "fillcolor=..." attributes
+	 * to the decoration.
+	 */
+	@Override
+	public Decoration decorateState(int state, Decoration d)
+	{
+		if (stateSet.get(state)) {
+			d.attributes().put("style", "filled");
+			d.attributes().put("fillcolor", fillColour);
+		}
+		return d;
+	}
+
+}

prism/src/explicit/graphviz/ShowRewardDecorator.java

@@ -0,0 +1,105 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit.graphviz;
+
+import explicit.rewards.MCRewards;
+import explicit.rewards.MDPRewards;
+import explicit.rewards.Rewards;
+
+/**
+ * A decorator that attaches rewards
+ * to the labels of nodes / edges, according to the
+ * given reward structure.
+ */
+public class ShowRewardDecorator implements Decorator
+{
+	/** The reward structure */
+	private Rewards rewards;
+	/** Flag: should zero rewards be output? */
+	private boolean showZero;
+
+	/**
+	 * Constructor, suppress zero rewards in output.
+	 * @param rewards the reward structure
+	 */
+	public ShowRewardDecorator(explicit.rewards.Rewards rewards)
+	{
+		this(rewards, false);
+
+	}
+
+	/**
+	 * Constructor.
+	 * @param rewards the reward structure
+	 * @param showZero should zero rewards be output?
+	 */
+	public ShowRewardDecorator(explicit.rewards.Rewards rewards, boolean showZero)
+	{
+		this.rewards = rewards;
+		this.showZero = showZero;
+	}
+
+	/**
+	 * Decorate state node by appending state reward to state label.
+	 */
+	@Override
+	public Decoration decorateState(int state, Decoration d)
+	{
+		double reward = 0;
+		if (rewards instanceof MCRewards) {
+			reward = ((MCRewards) rewards).getStateReward(state);
+		} else if (rewards instanceof MDPRewards) {
+			reward = ((MDPRewards) rewards).getStateReward(state);
+		}
+		if (reward == 0 && !showZero) {
+			return d;
+		}
+
+		d.labelAddBelow("+" + reward);
+		return d;
+	}
+
+	/**
+	 * Decorate choice edge by appending transition reward to transition label.
+	 */
+	@Override
+	public Decoration decorateTransition(int state, int choice, Decoration d)
+	{
+		if (!(rewards instanceof MDPRewards)) {
+			// transition rewards are only there for MDPRewards
+			return d;
+		}
+		double reward = ((MDPRewards) rewards).getTransitionReward(state, choice);
+		if (reward == 0 && !showZero) {
+			return d;
+		}
+
+		d.labelAddBelow("+" + reward);
+		return d;
+	}
+
+}

prism/src/explicit/graphviz/ShowStateRewardsDecorator.java

@@ -0,0 +1,98 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit.graphviz;
+
+import java.util.Collections;
+import java.util.List;
+
+import explicit.rewards.MCRewards;
+import explicit.rewards.MDPRewards;
+import explicit.rewards.StateRewards;
+
+/**
+ * A decorator that attaches state rewards
+ * to the labels of nodes, according to the
+ * given reward structure(s).
+ */
+public class ShowStateRewardsDecorator implements Decorator
+{
+	/** List of state reward structures */
+	private List<StateRewards> rewards;
+	/** Output state rewards even if they are all zero for a state? */
+	private boolean showAllZero;
+
+	/** Constructor, single reward structure */
+	public ShowStateRewardsDecorator(explicit.rewards.StateRewards rewards, boolean showZero)
+	{
+		this(Collections.singletonList(rewards), showZero);
+	}
+
+	/** Constructor, multiple reward structures */
+	public ShowStateRewardsDecorator(List<explicit.rewards.StateRewards> rewards, boolean showAllZero)
+	{
+		this.rewards = rewards;
+		this.showAllZero = showAllZero;
+	}
+
+	/** Attach state rewards for the given state */
+	@Override
+	public Decoration decorateState(int state, Decoration d)
+	{
+		boolean allZero = true;
+
+		for (StateRewards rew : rewards) {
+			double reward = 0;
+			if (rew instanceof MCRewards) {
+				reward = ((MCRewards) rewards).getStateReward(state);
+			} else if (rew instanceof MDPRewards) {
+				reward = ((MDPRewards) rewards).getStateReward(state);
+			}
+			if (reward != 0) {
+				allZero = false;
+				break;
+			}
+		}
+		if (allZero && !showAllZero)
+			return d;
+
+		String values = "";
+		for (StateRewards rew : rewards) {
+			double reward = 0;
+			if (rew instanceof MCRewards) {
+				reward = ((MCRewards) rewards).getStateReward(state);
+			} else if (rew instanceof MDPRewards) {
+				reward = ((MDPRewards) rewards).getStateReward(state);
+			}
+			if (!values.isEmpty())
+				values += ",";
+			values += reward;
+		}
+
+		d.labelAddBelow(values);
+		return d;
+	}
+}

prism/src/explicit/graphviz/ShowStatesDecorator.java

@@ -0,0 +1,56 @@
+//==============================================================================
+//	
+//	Copyright (c) 2016-
+//	Authors:
+//	* Joachim Klein <klein@tcs.inf.tu-dresden.de> (TU Dresden)
+//	
+//------------------------------------------------------------------------------
+//	
+//	This file is part of PRISM.
+//	
+//	PRISM is free software; you can redistribute it and/or modify
+//	it under the terms of the GNU General Public License as published by
+//	the Free Software Foundation; either version 2 of the License, or
+//	(at your option) any later version.
+//	
+//	PRISM is distributed in the hope that it will be useful,
+//	but WITHOUT ANY WARRANTY; without even the implied warranty of
+//	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+//	GNU General Public License for more details.
+//	
+//	You should have received a copy of the GNU General Public License
+//	along with PRISM; if not, write to the Free Software Foundation,
+//	Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+//	
+//==============================================================================
+
+package explicit.graphviz;
+
+import java.util.List;
+
+import parser.State;
+
+/**
+ * Decorator which show the state variable valuation for a given state.
+ */
+public class ShowStatesDecorator implements Decorator
+{
+	/** The state list, i.e., the variable valuation information for each state index */
+	private List<State> stateList;
+
+	/**
+	 * Constructor.
+	 * @param stateList the variable valuation information for each state index
+	 */
+	public ShowStatesDecorator(List<State> stateList)
+	{
+		this.stateList = stateList;
+	}
+
+	/** Decorate state label by appending the variable information */
+	public Decoration decorateState(int state, Decoration d)
+	{
+		d.labelAddBelow(stateList.get(state).toString());
+		return d;
+	}
+}