From 59745d025c6b06f6b57e2cab1ad81d35c1a70d83 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 21 Jul 2017 14:00:11 +0000 Subject: [PATCH] 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 | 198 ++++++++++++++++++ prism/src/explicit/graphviz/Decorator.java | 109 ++++++++++ .../graphviz/MarkStateSetDecorator.java | 76 +++++++ .../graphviz/ShowRewardDecorator.java | 105 ++++++++++ .../graphviz/ShowStateRewardsDecorator.java | 98 +++++++++ .../graphviz/ShowStatesDecorator.java | 56 +++++ 6 files changed, 642 insertions(+) create mode 100644 prism/src/explicit/graphviz/Decoration.java create mode 100644 prism/src/explicit/graphviz/Decorator.java create mode 100644 prism/src/explicit/graphviz/MarkStateSetDecorator.java create mode 100644 prism/src/explicit/graphviz/ShowRewardDecorator.java create mode 100644 prism/src/explicit/graphviz/ShowStateRewardsDecorator.java create mode 100644 prism/src/explicit/graphviz/ShowStatesDecorator.java diff --git a/prism/src/explicit/graphviz/Decoration.java b/prism/src/explicit/graphviz/Decoration.java new file mode 100644 index 00000000..11d45a99 --- /dev/null +++ b/prism/src/explicit/graphviz/Decoration.java @@ -0,0 +1,198 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (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 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 attributes() + { + if (attributes == null) { + // If there have been no attributes before, initialise empty map + attributes = new TreeMap(); + } + return attributes; + } + + /** + * Returns a read-only map for accessing attributes (apart from the label attribute). + *
+ * Note: If you only need read access, it might be more efficient to use this + * method instead of {@code attributes()}. + */ + public Map 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. + *
+ * 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 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()); + } + +} diff --git a/prism/src/explicit/graphviz/Decorator.java b/prism/src/explicit/graphviz/Decorator.java new file mode 100644 index 00000000..d7e38dc4 --- /dev/null +++ b/prism/src/explicit/graphviz/Decorator.java @@ -0,0 +1,109 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (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. + *
+ * 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; + } + +} diff --git a/prism/src/explicit/graphviz/MarkStateSetDecorator.java b/prism/src/explicit/graphviz/MarkStateSetDecorator.java new file mode 100644 index 00000000..764a6bd4 --- /dev/null +++ b/prism/src/explicit/graphviz/MarkStateSetDecorator.java @@ -0,0 +1,76 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (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; + } + +} diff --git a/prism/src/explicit/graphviz/ShowRewardDecorator.java b/prism/src/explicit/graphviz/ShowRewardDecorator.java new file mode 100644 index 00000000..374b107c --- /dev/null +++ b/prism/src/explicit/graphviz/ShowRewardDecorator.java @@ -0,0 +1,105 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (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; + } + +} diff --git a/prism/src/explicit/graphviz/ShowStateRewardsDecorator.java b/prism/src/explicit/graphviz/ShowStateRewardsDecorator.java new file mode 100644 index 00000000..f4bf7cb6 --- /dev/null +++ b/prism/src/explicit/graphviz/ShowStateRewardsDecorator.java @@ -0,0 +1,98 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (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 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 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; + } +} diff --git a/prism/src/explicit/graphviz/ShowStatesDecorator.java b/prism/src/explicit/graphviz/ShowStatesDecorator.java new file mode 100644 index 00000000..c24d25a6 --- /dev/null +++ b/prism/src/explicit/graphviz/ShowStatesDecorator.java @@ -0,0 +1,56 @@ +//============================================================================== +// +// Copyright (c) 2016- +// Authors: +// * Joachim Klein (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 stateList; + + /** + * Constructor. + * @param stateList the variable valuation information for each state index + */ + public ShowStatesDecorator(List 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; + } +}