19864403395

/* Copyright (C) 2013-2025 TU Dortmund University
 * This file is part of AutomataLib <https://automatalib.net>.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package net.automatalib.automaton.visualization;

import java.util.Collections;
import java.util.List;
import java.util.Map;
import java.util.Objects;
import java.util.StringJoiner;
import java.util.function.Function;

import net.automatalib.automaton.mmlt.MMLT;
import net.automatalib.automaton.mmlt.TimerInfo;
import net.automatalib.common.util.Triple;
import net.automatalib.symbol.time.InputSymbol;
import net.automatalib.symbol.time.SymbolicInput;
import net.automatalib.symbol.time.TimerTimeoutSymbol;
import net.automatalib.visualization.DefaultVisualizationHelper;

/**
 * A visualization helper for MMLTs which Allows edge coloring and explicit resets in transition labels for easier
 * inspection.
 * <p>
 * If you want to serialize MMLTs using this visualization helper, you should consider disabling explicit resets as the
 * additional markup may cause problems during parsing.
 *
 * @param <S>
 *         location type
 * @param <I>
 *         input symbol type (of non-delaying inputs)
 * @param <O>
 *         output symbol type
 */
public class MMLTVisualizationHelper<S, I, O> extends DefaultVisualizationHelper<S, Triple<SymbolicInput<I>, O, S>> {

    private final MMLT<S, I, ?, O> mmlt;
    private final boolean colorEdges;
    private final boolean includeResets;

    /**
     * Default constructor.
     *
     * @param mmlt
     *         the MMLT
     * @param colorEdges
     *         a flag indicating whether the transitions for local resets, periodic timers, and one-shot timers should
     *         be colored differently
     * @param includeResets
     *         a flag indicating whether each transition label should include a list of timers that it resets
     */
    public MMLTVisualizationHelper(MMLT<S, I, ?, O> mmlt, boolean colorEdges, boolean includeResets) {
        this.mmlt = mmlt;
        this.colorEdges = colorEdges;
        this.includeResets = includeResets;
    }

    @Override
    public boolean getNodeProperties(S node, Map<String, String> properties) {
        super.getNodeProperties(node, properties);

        if (Objects.equals(node, mmlt.getInitialState())) {
            properties.put(NodeAttrs.INITIAL, String.valueOf(true));
        }

        // Include timer assignments:
        final List<TimerInfo<S, O>> timers = mmlt.getSortedTimers(node);

        if (!timers.isEmpty()) {
            // Add local timer info:
            properties.put(MMLTNodeAttrs.TIMERS,
                           renderTimers(timers, t -> String.format("%s=%d", t.name(), t.initial())));
        }

        return true;
    }

    @Override
    public boolean getEdgeProperties(S src,
                                     Triple<SymbolicInput<I>, O, S> edge,
                                     S tgt,
                                     Map<String, String> properties) {
        super.getEdgeProperties(src, edge, tgt, properties);

        final SymbolicInput<I> input = edge.getFirst();
        final List<TimerInfo<S, O>> timers = mmlt.getSortedTimers(tgt);

        final String label = String.format("%s / %s", input, edge.getSecond());
        final StringBuilder labelBuilder = new StringBuilder(label);

        if (input instanceof TimerTimeoutSymbol<I> ts) {
            // Get info for corresponding timer:
            TimerInfo<S, O> timer = null;
            for (TimerInfo<S, O> t : mmlt.getSortedTimers(src)) {
                if (t.name().equals(ts.timer())) {
                    timer = t;
                    break;
                }
            }

            if (timer == null) {
                throw new IllegalArgumentException("timeout symbol references unknown timer");
            }

            if (timer.periodic()) {
                // Periodic -> resets itself:
                appendResetInfo(labelBuilder, timer);
                colorEdges(properties, "blue");
            } else {
                // One-shot -> resets all in target:
                appendResetInfo(labelBuilder, timers);
                if (Objects.equals(tgt, src)) {
                    // If the target is another location, reset info can always be inferred from context.
                    // --> Only include if self-loop:
                    properties.put(MMLTEdgeAttrs.RESETS, renderTimers(timers, TimerInfo::name));
                }
                colorEdges(properties, "green");
            }
        } else if (input instanceof InputSymbol<I> ndi && Objects.equals(src, tgt) &&
                   mmlt.isLocalReset(src, ndi.symbol())) {
            // Self-loop + local reset -> resets all in target:
            appendResetInfo(labelBuilder, timers);
            colorEdges(properties, "orange");
            properties.put(MMLTEdgeAttrs.RESETS, renderTimers(timers, TimerInfo::name));
        }

        properties.put(EdgeAttrs.LABEL, labelBuilder.toString());

        return true;
    }

    private void colorEdges(Map<String, String> properties, String color) {
        if (this.colorEdges) {
            properties.put(EdgeAttrs.COLOR, color);
            properties.put(EdgeAttrs.FONTCOLOR, color);
        }
    }

    private void appendResetInfo(StringBuilder labelBuilder, TimerInfo<S, O> timer) {
        appendResetInfo(labelBuilder, Collections.singletonList(timer));
    }

    private void appendResetInfo(StringBuilder labelBuilder, List<TimerInfo<S, O>> timers) {
        if (includeResets && !timers.isEmpty()) {
            labelBuilder.append(" {")
                        .append(renderTimersInternal(timers, t -> String.format("%s↦%d", t.name(), t.initial())))
                        .append('}');
        }
    }

    private String renderTimers(List<TimerInfo<S, O>> timers, Function<TimerInfo<S, O>, String> extractor) {
        return renderTimersInternal(timers, extractor).toString();
    }

    private StringJoiner renderTimersInternal(List<TimerInfo<S, O>> timers,
                                              Function<TimerInfo<S, O>, String> extractor) {
        final StringJoiner sj = new StringJoiner(",");
        for (TimerInfo<S, O> t : timers) {
            sj.add(extractor.apply(t));
        }
        return sj;
    }

}

1	/* Copyright (C) 2013-2025 TU Dortmund University
2	* This file is part of AutomataLib <https://automatalib.net>.
3	*
4	* Licensed under the Apache License, Version 2.0 (the "License");
5	* you may not use this file except in compliance with the License.
6	* You may obtain a copy of the License at
7	*
8	* http://www.apache.org/licenses/LICENSE-2.0
9	*
10	* Unless required by applicable law or agreed to in writing, software
11	* distributed under the License is distributed on an "AS IS" BASIS,
12	* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13	* See the License for the specific language governing permissions and
14	* limitations under the License.
15	*/
16	package net.automatalib.automaton.visualization;
17
18	import java.util.Collections;
19	import java.util.List;
20	import java.util.Map;
21	import java.util.Objects;
22	import java.util.StringJoiner;
23	import java.util.function.Function;
24
25	import net.automatalib.automaton.mmlt.MMLT;
26	import net.automatalib.automaton.mmlt.TimerInfo;
27	import net.automatalib.common.util.Triple;
28	import net.automatalib.symbol.time.InputSymbol;
29	import net.automatalib.symbol.time.SymbolicInput;
30	import net.automatalib.symbol.time.TimerTimeoutSymbol;
31	import net.automatalib.visualization.DefaultVisualizationHelper;
32
33	/**
34	* A visualization helper for MMLTs which Allows edge coloring and explicit resets in transition labels for easier
35	* inspection.
36	* <p>
37	* If you want to serialize MMLTs using this visualization helper, you should consider disabling explicit resets as the
38	* additional markup may cause problems during parsing.
39	*
40	* @param <S>
41	* location type
42	* @param <I>
43	* input symbol type (of non-delaying inputs)
44	* @param <O>
45	* output symbol type
46	*/
47	public class MMLTVisualizationHelper<S, I, O> extends DefaultVisualizationHelper<S, Triple<SymbolicInput<I>, O, S>> {
48
49	private final MMLT<S, I, ?, O> mmlt;
50	private final boolean colorEdges;
51	private final boolean includeResets;
52
53	/**
54	* Default constructor.
55	*
56	* @param mmlt
57	* the MMLT
58	* @param colorEdges
59	* a flag indicating whether the transitions for local resets, periodic timers, and one-shot timers should
60	* be colored differently
61	* @param includeResets
62	* a flag indicating whether each transition label should include a list of timers that it resets
63	*/
64	public MMLTVisualizationHelper(MMLT<S, I, ?, O> mmlt, boolean colorEdges, boolean includeResets) {	1✔
65	this.mmlt = mmlt;	1✔
66	this.colorEdges = colorEdges;	1✔
67	this.includeResets = includeResets;	1✔
68	}	1✔
69
70	@Override
71	public boolean getNodeProperties(S node, Map<String, String> properties) {
72	super.getNodeProperties(node, properties);	1✔
73
74	if (Objects.equals(node, mmlt.getInitialState())) {	1✔
75	properties.put(NodeAttrs.INITIAL, String.valueOf(true));	1✔
76	}
77
78	// Include timer assignments:
79	final List<TimerInfo<S, O>> timers = mmlt.getSortedTimers(node);	1✔
80
81	if (!timers.isEmpty()) {	1✔
82	// Add local timer info:
83	properties.put(MMLTNodeAttrs.TIMERS,	1✔
84	renderTimers(timers, t -> String.format("%s=%d", t.name(), t.initial())));	1✔
85	}
86
87	return true;	1✔
88	}
89
90	@Override
91	public boolean getEdgeProperties(S src,
92	Triple<SymbolicInput<I>, O, S> edge,
93	S tgt,
94	Map<String, String> properties) {
95	super.getEdgeProperties(src, edge, tgt, properties);	1✔
96
97	final SymbolicInput<I> input = edge.getFirst();	1✔
98	final List<TimerInfo<S, O>> timers = mmlt.getSortedTimers(tgt);	1✔
99
100	final String label = String.format("%s / %s", input, edge.getSecond());	1✔
101	final StringBuilder labelBuilder = new StringBuilder(label);	1✔
102
103	if (input instanceof TimerTimeoutSymbol<I> ts) {	1✔
104	// Get info for corresponding timer:
105	TimerInfo<S, O> timer = null;	1✔
106	for (TimerInfo<S, O> t : mmlt.getSortedTimers(src)) {	1✔
107	if (t.name().equals(ts.timer())) {	1✔
108	timer = t;	1✔
109	break;	1✔
110	}
111	}	1✔
112
113	if (timer == null) {	1✔
NEW 114	throw new IllegalArgumentException("timeout symbol references unknown timer");	×
115	}
116
117	if (timer.periodic()) {	1✔
118	// Periodic -> resets itself:
119	appendResetInfo(labelBuilder, timer);	1✔
120	colorEdges(properties, "blue");	1✔
121	} else {
122	// One-shot -> resets all in target:
123	appendResetInfo(labelBuilder, timers);	1✔
124	if (Objects.equals(tgt, src)) {	1✔
125	// If the target is another location, reset info can always be inferred from context.
126	// --> Only include if self-loop:
127	properties.put(MMLTEdgeAttrs.RESETS, renderTimers(timers, TimerInfo::name));	1✔
128	}
129	colorEdges(properties, "green");	1✔
130	}
131	} else if (input instanceof InputSymbol<I> ndi && Objects.equals(src, tgt) &&	1✔
132	mmlt.isLocalReset(src, ndi.symbol())) {	1✔
133	// Self-loop + local reset -> resets all in target:
134	appendResetInfo(labelBuilder, timers);	1✔
135	colorEdges(properties, "orange");	1✔
136	properties.put(MMLTEdgeAttrs.RESETS, renderTimers(timers, TimerInfo::name));	1✔
137	}
138
139	properties.put(EdgeAttrs.LABEL, labelBuilder.toString());	1✔
140
141	return true;	1✔
142	}
143
144	private void colorEdges(Map<String, String> properties, String color) {
145	if (this.colorEdges) {	1✔
146	properties.put(EdgeAttrs.COLOR, color);	1✔
147	properties.put(EdgeAttrs.FONTCOLOR, color);	1✔
148	}
149	}	1✔
150
151	private void appendResetInfo(StringBuilder labelBuilder, TimerInfo<S, O> timer) {
152	appendResetInfo(labelBuilder, Collections.singletonList(timer));	1✔
153	}	1✔
154
155	private void appendResetInfo(StringBuilder labelBuilder, List<TimerInfo<S, O>> timers) {
156	if (includeResets && !timers.isEmpty()) {	1✔
157	labelBuilder.append(" {")	1✔
158	.append(renderTimersInternal(timers, t -> String.format("%s↦%d", t.name(), t.initial())))	1✔
159	.append('}');	1✔
160	}
161	}	1✔
162
163	private String renderTimers(List<TimerInfo<S, O>> timers, Function<TimerInfo<S, O>, String> extractor) {
164	return renderTimersInternal(timers, extractor).toString();	1✔
165	}
166
167	private StringJoiner renderTimersInternal(List<TimerInfo<S, O>> timers,
168	Function<TimerInfo<S, O>, String> extractor) {
169	final StringJoiner sj = new StringJoiner(",");	1✔
170	for (TimerInfo<S, O> t : timers) {	1✔
171	sj.add(extractor.apply(t));	1✔
172	}	1✔
173	return sj;	1✔
174	}
175
176	}

LearnLib / automatalib / 19864403395

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous