taco_threshold_automaton/
dot.rs

1//! Visualization of threshold automata in DOT format
2//!
3//! This module provides the trait `ToDOT` for converting threshold automata into
4//! the [DOT format](https://graphviz.org/doc/info/lang.html), which can be
5//! visualized using tools like [Graphviz](https://graphviz.org/).
6//!
7//! The trait `ToDOT` is implemented for both `ThresholdAutomaton` and
8//! `LIAThresholdAutomaton`. The `ThresholdAutomaton` can be converted into a
9//! graph in DOT format, while the `LIAThresholdAutomaton` can be converted into
10//! a graph in DOT format with the additional information of the transformed
11//! guards.
12//!
13//! The trait `DOTDiff` is meant for debugging purposes and implemented for
14//! both `ThresholdAutomaton` and `LIAThresholdAutomaton`. It allows to
15//! visualize the difference between two automata in DOT format, i.e., it marks
16//! added locations and edges in green, removed locations and edges in red, and
17//! unchanged locations and edges in black.
18
19use std::fmt::{self};
20
21use taco_display_utils::{indent_all, join_iterator};
22
23use crate::{RuleDefinition, ThresholdAutomaton};
24
25/// Define the font type for labels and nodes in the graph
26const GRAPH_OPTIONS: &str = "\
27rankdir=LR \
28fontname=\"Helvetica,Arial,sans-serif\" \
29node [fontname=\"Helvetica,Arial,sans-serif\"] \
30edge [fontname=\"Helvetica,Arial,sans-serif\"];";
31
32/// Options to mark initial locations
33const INITIAL_LOC_OPTIONS: &str = "shape = circle";
34/// Options for locations
35const LOC_OPTIONS: &str = "shape = circle";
36
37// Diff coloring
38/// Options for removed locations
39const REMOVED: &str = "color = red, fontcolor = red";
40/// Options for added locations
41const ADDED: &str = "color = green, fontcolor = green";
42
43/// Objects implementing this train can be converted visualized as a graph with
44/// graphviz
45///
46/// This trait is only available if the `dot` feature is enabled. It allows to
47/// export an object into the
48/// [DOT format](https://graphviz.org/doc/info/lang.html),
49/// which can be visualized using tools like [Graphviz](https://graphviz.org/).
50pub trait ToDOT {
51    /// Get the underlying graph in DOT format
52    ///
53    /// Returns the visualization in DOT format. The output can be visualized
54    /// using tools [Graphviz](https://graphviz.org/) or tools compatible with
55    /// the [DOT Language](https://graphviz.org/doc/info/lang.html).
56    fn get_dot_graph(&self) -> String;
57}
58
59/// Trait for encoding an automaton (e.g.
60/// [`crate::general_threshold_automaton::GeneralThresholdAutomaton`] or other
61/// types implementing the [`ThresholdAutomaton`] trait into a graph in DOT
62/// format
63trait AutomatonEncoding {
64    /// Type for the edge labels
65    type EdgeLabel: fmt::Display + PartialEq;
66
67    /// Name of the automaton
68    fn get_name(&self) -> String;
69
70    /// Initial locations of the automaton
71    ///
72    /// Locations are the states of the automaton and must implement
73    /// `fmt::Display`. The name will be used as the label in the DOT file.
74    fn get_initial_locations(&self) -> impl Iterator<Item = String>;
75
76    /// Locations of the automaton
77    ///
78    /// Get the locations of the automaton that are neither initial nor final
79    /// Locations must implement
80    /// `fmt::Display`. The name will be used as the label in the DOT file.
81    fn get_locations(&self) -> impl Iterator<Item = String>;
82
83    /// Get the transitions of the automaton
84    fn get_transitions(&self) -> impl Iterator<Item = (String, Self::EdgeLabel, String)>;
85
86    /// Get the encoding of the nodes into the DOT format
87    fn get_node_encoding(nodes: impl Iterator<Item = String>, node_options: &String) -> String {
88        let mut nodes = join_iterator(nodes, "\n");
89        if !nodes.is_empty() {
90            nodes = format!("node [{}];\n{}\n;", node_options, indent_all(nodes));
91            nodes = indent_all(nodes);
92            nodes += "\n";
93        }
94
95        nodes
96    }
97
98    /// General function to enable the encoding of the edges into the DOT format
99    /// with the given edge options
100    fn get_edge_encoding(
101        edges: impl Iterator<Item = (String, Self::EdgeLabel, String)>,
102        edge_options: &String,
103    ) -> String {
104        let edge_options = if edge_options.is_empty() {
105            String::new()
106        } else {
107            format!(", {edge_options}")
108        };
109
110        let edges = edges
111            .map(|(src, label, tgt)| format!("{src} -> {tgt} [label = \"{label}\"{edge_options}]"));
112        let mut edges = join_iterator(edges, ";\n");
113
114        if !edges.is_empty() {
115            edges += ";";
116            edges = indent_all(edges);
117            edges += "\n";
118        }
119
120        edges
121    }
122}
123
124// implement `ToDOT` for all types implementing the [`AutomatonEncoding`] trait
125impl<T: AutomatonEncoding> ToDOT for T {
126    fn get_dot_graph(&self) -> String {
127        let graph_title = format!(
128            "graph [label =<<B>{}</B>>, labelloc = t, fontsize = 35];\n",
129            self.get_name()
130        );
131
132        let init_states = Self::get_node_encoding(
133            self.get_initial_locations(),
134            &INITIAL_LOC_OPTIONS.to_string(),
135        );
136
137        let loc = Self::get_node_encoding(self.get_locations(), &LOC_OPTIONS.to_string());
138
139        let transitions = Self::get_edge_encoding(self.get_transitions(), &String::new());
140
141        format!(
142            "digraph {} {{\n{}\n{}{}{}{}}}",
143            self.get_name(),
144            indent_all(GRAPH_OPTIONS),
145            indent_all(graph_title),
146            init_states,
147            loc,
148            transitions,
149        )
150    }
151}
152
153// implement [`AutomatonEncoding`] for all types implementing the
154// [`ThresholdAutomaton`] type
155impl<T> AutomatonEncoding for T
156where
157    T: ThresholdAutomaton,
158{
159    type EdgeLabel = String;
160
161    fn get_name(&self) -> String {
162        self.name().to_string()
163    }
164
165    fn get_initial_locations(&self) -> impl Iterator<Item = String> {
166        self.locations()
167            .filter(|l| self.can_be_initial_location(l))
168            .map(|l| l.to_string())
169    }
170
171    fn get_locations(&self) -> impl Iterator<Item = String> {
172        self.locations().map(|l| l.to_string())
173    }
174
175    fn get_transitions(&self) -> impl Iterator<Item = (String, Self::EdgeLabel, String)> {
176        self.rules().map(|r| {
177            (
178                r.source().to_string(),
179                r.guard().to_string(),
180                r.target().to_string(),
181            )
182        })
183    }
184}
185
186/// Visualize the difference between two objects in DOT format
187///
188/// This trait is only available if the `dot` feature is enabled. It allows to
189/// visualize the difference between two objects in DOT format, i.e., it marks
190/// added objects in green, removed objects in red, and unchanged locations and
191/// edges in black.
192pub trait DOTDiff {
193    /// Get the difference between two objects in DOT format
194    ///
195    /// Returns the difference between two objects in DOT format, i.e., it marks
196    /// added objects in green, removed objects in red, and unchanged locations and
197    /// edges in black.
198    fn get_dot_diff(&self, other: &Self) -> String;
199}
200
201impl<T: AutomatonEncoding> DOTDiff for T {
202    fn get_dot_diff(&self, other: &Self) -> String {
203        let graph_title = format!(
204            "graph [label =<<B>Diff: {} - {} </B>>, labelloc = t, fontsize = 35];\n",
205            self.get_name(),
206            other.get_name()
207        );
208
209        let removed_init_states = self
210            .get_initial_locations()
211            .filter(|l| !other.get_initial_locations().any(|ol| *l == ol));
212        let removed_init_states = Self::get_node_encoding(
213            removed_init_states,
214            &format!("{INITIAL_LOC_OPTIONS}, {REMOVED}"),
215        );
216
217        let added_init_states = other
218            .get_initial_locations()
219            .filter(|l| !self.get_initial_locations().any(|ol| *l == ol));
220        let added_init_states = Self::get_node_encoding(
221            added_init_states,
222            &format!("{INITIAL_LOC_OPTIONS}, {ADDED}"),
223        );
224
225        let regular_init_states = self
226            .get_initial_locations()
227            .filter(|l| other.get_initial_locations().any(|ol| *l == ol));
228        let regular_init_states =
229            Self::get_node_encoding(regular_init_states, &INITIAL_LOC_OPTIONS.to_string());
230        let init_states = format!("{removed_init_states}{added_init_states}{regular_init_states}");
231
232        let removed_loc = self
233            .get_locations()
234            .filter(|l| !other.get_locations().any(|ol| *l == ol));
235        let removed_loc =
236            Self::get_node_encoding(removed_loc, &format!("{LOC_OPTIONS}, {REMOVED}"));
237
238        let added_loc = other
239            .get_locations()
240            .filter(|l| !self.get_locations().any(|ol| *l == ol));
241        let added_loc = Self::get_node_encoding(added_loc, &format!("{LOC_OPTIONS}, {ADDED}"));
242
243        let regular_loc = self
244            .get_locations()
245            .filter(|l| other.get_locations().any(|ol| *l == ol));
246        let regular_loc = Self::get_node_encoding(regular_loc, &LOC_OPTIONS.to_string());
247        let loc = format!("{removed_loc}{added_loc}{regular_loc}");
248
249        let removed_transitions = self.get_transitions().filter(|(src, lbl, tgt)| {
250            !other
251                .get_transitions()
252                .any(|(osrc, olbl, otgt)| *src == osrc && *tgt == otgt && *lbl == olbl)
253        });
254        let removed_transitions =
255            Self::get_edge_encoding(removed_transitions, &format!("{REMOVED}, {REMOVED}"));
256
257        let added_transitions = other.get_transitions().filter(|(src, lbl, tgt)| {
258            !self
259                .get_transitions()
260                .any(|(osrc, olbl, otgt)| *src == osrc && *tgt == otgt && *lbl == olbl)
261        });
262        let added_transitions =
263            Self::get_edge_encoding(added_transitions, &format!("{ADDED}, {ADDED}"));
264
265        let regular_transitions = self.get_transitions().filter(|(src, lbl, tgt)| {
266            other
267                .get_transitions()
268                .any(|(osrc, olbl, otgt)| *src == osrc && *tgt == otgt && *lbl == olbl)
269        });
270        let regular_transitions = Self::get_edge_encoding(regular_transitions, &String::new());
271        let transitions = format!("{removed_transitions}{added_transitions}{regular_transitions}");
272
273        format!(
274            "digraph {} {{\n{}\n{}{}{}{}}}",
275            self.get_name(),
276            indent_all(GRAPH_OPTIONS),
277            indent_all(graph_title),
278            init_states,
279            loc,
280            transitions,
281        )
282    }
283}
taco_threshold_automaton/dot.rs

taco_threshold_automaton/
dot.rs
