31586418187

Committed 12 Aug 2026 09:53AM UTC coverage: 92.921% (+0.9%) from 92.059%

Build # 31586418187

Build Type

push

github

Committed by

mtf90

Commit Message

use new version scheme

Coverage Stats

17615 of 18957 relevant lines covered (92.92%)

1.72 hits per line

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

85.42

/visualization/dot-visualizer/src/main/java/net/automatalib/visualization/dot/DOTImageComponent.java

/* Copyright (C) 2013-2026 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.visualization.dot;

import java.awt.Color;
import java.awt.Cursor;
import java.awt.Dimension;
import java.awt.Graphics;
import java.awt.Point;
import java.awt.event.ActionEvent;
import java.awt.event.MouseEvent;
import java.awt.image.BufferedImage;
import java.io.IOException;
import java.io.Writer;

import javax.imageio.ImageIO;
import javax.swing.AbstractAction;
import javax.swing.Action;
import javax.swing.JComponent;
import javax.swing.JFileChooser;
import javax.swing.JOptionPane;
import javax.swing.JViewport;
import javax.swing.event.MouseInputAdapter;

import net.automatalib.common.util.IOUtil;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.slf4j.Logger;
import org.slf4j.LoggerFactory;

/**
 * Component that displays a {@link BufferedImage}.
 */
final class DOTImageComponent extends JComponent {

    private static final Logger LOGGER = LoggerFactory.getLogger(DOTImageComponent.class);

    private @Nullable String dot;
    private @Nullable BufferedImage img;

    private final Action saveDotAction = new AbstractAction("Save DOT") {

        @Override
        public void actionPerformed(ActionEvent e) {
            final JFileChooser saveDlg = new JFileChooser();
            saveDlg.setFileFilter(DOTUtil.DOT_FILTER);
            final int result = saveDlg.showSaveDialog(DOTImageComponent.this);
            if (result != JFileChooser.APPROVE_OPTION) {
                return;
            }
            final String dot = DOTImageComponent.this.dot;
            if (dot == null) {
                throw new IllegalStateException("No DOT text has been set");
            }
            try (Writer w = IOUtil.asBufferedUTF8Writer(saveDlg.getSelectedFile())) {
                w.write(dot);
            } catch (IOException ex) {
                LOGGER.error("Cannot save DOT", ex);
                JOptionPane.showMessageDialog(DOTImageComponent.this,
                                              "Could not save DOT file: " + ex.getMessage(),
                                              "Cannot save DOT",
                                              JOptionPane.ERROR_MESSAGE);
            }
        }
    };

    private final Action savePngAction = new AbstractAction("Save PNG") {

        @Override
        public void actionPerformed(ActionEvent e) {
            JFileChooser chooser = new JFileChooser();
            chooser.setFileFilter(DOTUtil.PNG_FILTER);
            int result = chooser.showSaveDialog(DOTImageComponent.this);
            if (result != JFileChooser.APPROVE_OPTION) {
                return;
            }
            final BufferedImage img = DOTImageComponent.this.img;
            if (img == null) {
                throw new IllegalStateException("No image has been set");
            }
            try {
                ImageIO.write(img, "png", chooser.getSelectedFile());
            } catch (IOException ex) {
                LOGGER.error("Cannot save PNG", ex);
                JOptionPane.showMessageDialog(DOTImageComponent.this,
                                              "Could not save PNG file: " + ex.getMessage(),
                                              "Could not save PNG",
                                              JOptionPane.ERROR_MESSAGE);
            }
        }
    };

    /**
     * Default constructor.
     */
    DOTImageComponent() {
        final DnDMover dnDMover = new DnDMover();

        setPreferredSize(new Dimension(DOTUtil.DEFAULT_WIDTH, DOTUtil.DEFAULT_HEIGHT));
        addMouseListener(dnDMover);
        addMouseMotionListener(dnDMover);
    }

    /**
     * Sets the image to be displayed.
     *
     * @param img
     *         the image to be displayed
     */
    void setImage(@Nullable BufferedImage img) {
        this.img = img;
        Dimension dim;
        if (img != null) {
            dim = new Dimension(img.getWidth(), img.getHeight());
        } else {
            dim = new Dimension(DOTUtil.DEFAULT_WIDTH, DOTUtil.DEFAULT_HEIGHT);
        }

        setSize(dim);
        setPreferredSize(dim);
        repaint();
    }

    void setDotText(@Nullable String dot) {
        this.dot = dot;
    }

    void setData(@Nullable PlottedGraph pg) {
        if (pg == null) {
            this.setDotText(null);
            this.setImage(null);
        } else {
            this.setDotText(pg.getDotText());
            this.setImage(pg.getImage());
        }
    }

    /**
     * Retrieves an {@link Action} to save the image in a PNG file.
     *
     * @return the action
     */
    Action getSavePngAction() {
        return savePngAction;
    }

    Action getSaveDotAction() {
        return saveDotAction;
    }

    @Override
    protected void paintComponent(Graphics g) {
        g.setColor(Color.WHITE);
        g.fillRect(0, 0, getWidth(), getHeight());
        if (img != null) {
            g.drawImage(img, 0, 0, null);
        }
    }

    /*
     * Based on https://stackoverflow.com/questions/31171502/scroll-jscrollpane-by-dragging-mouse-java-swing/58815302#58815302
     */
    private class DnDMover extends MouseInputAdapter {

        private final DOTImageComponent cmp;
        private Point holdPointOnView;

        DnDMover() {
            this.cmp = DOTImageComponent.this;
        }

        @Override
        public void mousePressed(MouseEvent e) {
            cmp.setCursor(Cursor.getPredefinedCursor(Cursor.MOVE_CURSOR));
            holdPointOnView = e.getPoint();
        }

        @Override
        public void mouseReleased(MouseEvent e) {
            cmp.setCursor(null);
        }

        @Override
        public void mouseDragged(MouseEvent e) {
            final Point dragEventPoint = e.getPoint();
            @SuppressWarnings("nullness") // the DOTImageComponent is always embedded in a parent frame
            final @NonNull JViewport viewport = (JViewport) cmp.getParent();

            final Point viewPos = viewport.getViewPosition();

            final int maxViewPosX = cmp.getWidth() - viewport.getWidth();
            final int maxViewPosY = cmp.getHeight() - viewport.getHeight();

            assert holdPointOnView != null;

            if (cmp.getWidth() > viewport.getWidth()) {
                viewPos.x -= dragEventPoint.x - holdPointOnView.x;

                if (viewPos.x < 0) {
                    viewPos.x = 0;
                    holdPointOnView.x = dragEventPoint.x;
                }

                if (viewPos.x > maxViewPosX) {
                    viewPos.x = maxViewPosX;
                    holdPointOnView.x = dragEventPoint.x;
                }
            }

            if (cmp.getHeight() > viewport.getHeight()) {
                viewPos.y -= dragEventPoint.y - holdPointOnView.y;

                if (viewPos.y < 0) {
                    viewPos.y = 0;
                    holdPointOnView.y = dragEventPoint.y;
                }

                if (viewPos.y > maxViewPosY) {
                    viewPos.y = maxViewPosY;
                    holdPointOnView.y = dragEventPoint.y;
                }
            }

            viewport.setViewPosition(viewPos);
        }
    }
}

1	/* Copyright (C) 2013-2026 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.visualization.dot;
17
18	import java.awt.Color;
19	import java.awt.Cursor;
20	import java.awt.Dimension;
21	import java.awt.Graphics;
22	import java.awt.Point;
23	import java.awt.event.ActionEvent;
24	import java.awt.event.MouseEvent;
25	import java.awt.image.BufferedImage;
26	import java.io.IOException;
27	import java.io.Writer;
28
29	import javax.imageio.ImageIO;
30	import javax.swing.AbstractAction;
31	import javax.swing.Action;
32	import javax.swing.JComponent;
33	import javax.swing.JFileChooser;
34	import javax.swing.JOptionPane;
35	import javax.swing.JViewport;
36	import javax.swing.event.MouseInputAdapter;
37
38	import net.automatalib.common.util.IOUtil;
39	import org.checkerframework.checker.nullness.qual.NonNull;
40	import org.checkerframework.checker.nullness.qual.Nullable;
41	import org.slf4j.Logger;
42	import org.slf4j.LoggerFactory;
43
44	/**
45	* Component that displays a {@link BufferedImage}.
46	*/
47	final class DOTImageComponent extends JComponent {
48
49	private static final Logger LOGGER = LoggerFactory.getLogger(DOTImageComponent.class);	2✔
50
51	private @Nullable String dot;
52	private @Nullable BufferedImage img;
53
54	private final Action saveDotAction = new AbstractAction("Save DOT") {	2✔
55
56	@Override
57	public void actionPerformed(ActionEvent e) {
58	final JFileChooser saveDlg = new JFileChooser();	2✔
59	saveDlg.setFileFilter(DOTUtil.DOT_FILTER);	2✔
60	final int result = saveDlg.showSaveDialog(DOTImageComponent.this);	2✔
61	if (result != JFileChooser.APPROVE_OPTION) {	2✔
62	return;	2✔
63	}
64	final String dot = DOTImageComponent.this.dot;	2✔
65	if (dot == null) {	2✔
66	throw new IllegalStateException("No DOT text has been set");	×
67	}
68	try (Writer w = IOUtil.asBufferedUTF8Writer(saveDlg.getSelectedFile())) {	2✔
69	w.write(dot);	2✔
70	} catch (IOException ex) {	×
71	LOGGER.error("Cannot save DOT", ex);	×
72	JOptionPane.showMessageDialog(DOTImageComponent.this,	×
73	"Could not save DOT file: " + ex.getMessage(),	×
74	"Cannot save DOT",
75	JOptionPane.ERROR_MESSAGE);
76	}	2✔
77	}	2✔
78	};
79
80	private final Action savePngAction = new AbstractAction("Save PNG") {	2✔
81
82	@Override
83	public void actionPerformed(ActionEvent e) {
84	JFileChooser chooser = new JFileChooser();	2✔
85	chooser.setFileFilter(DOTUtil.PNG_FILTER);	2✔
86	int result = chooser.showSaveDialog(DOTImageComponent.this);	2✔
87	if (result != JFileChooser.APPROVE_OPTION) {	2✔
88	return;	2✔
89	}
90	final BufferedImage img = DOTImageComponent.this.img;	2✔
91	if (img == null) {	2✔
92	throw new IllegalStateException("No image has been set");	×
93	}
94	try {
95	ImageIO.write(img, "png", chooser.getSelectedFile());	2✔
96	} catch (IOException ex) {	×
97	LOGGER.error("Cannot save PNG", ex);	×
98	JOptionPane.showMessageDialog(DOTImageComponent.this,	×
99	"Could not save PNG file: " + ex.getMessage(),	×
100	"Could not save PNG",
101	JOptionPane.ERROR_MESSAGE);
102	}	2✔
103	}	2✔
104	};
105
106	/**
107	* Default constructor.
108	*/
109	DOTImageComponent() {	2✔
110	final DnDMover dnDMover = new DnDMover();	2✔
111
112	setPreferredSize(new Dimension(DOTUtil.DEFAULT_WIDTH, DOTUtil.DEFAULT_HEIGHT));	2✔
113	addMouseListener(dnDMover);	2✔
114	addMouseMotionListener(dnDMover);	2✔
115	}	2✔
116
117	/**
118	* Sets the image to be displayed.
119	*
120	* @param img
121	* the image to be displayed
122	*/
123	void setImage(@Nullable BufferedImage img) {
124	this.img = img;	2✔
125	Dimension dim;
126	if (img != null) {	2✔
127	dim = new Dimension(img.getWidth(), img.getHeight());	2✔
128	} else {
129	dim = new Dimension(DOTUtil.DEFAULT_WIDTH, DOTUtil.DEFAULT_HEIGHT);	2✔
130	}
131
132	setSize(dim);	2✔
133	setPreferredSize(dim);	2✔
134	repaint();	2✔
135	}	2✔
136
137	void setDotText(@Nullable String dot) {
138	this.dot = dot;	2✔
139	}	2✔
140
141	void setData(@Nullable PlottedGraph pg) {
142	if (pg == null) {	2✔
143	this.setDotText(null);	2✔
144	this.setImage(null);	2✔
145	} else {
146	this.setDotText(pg.getDotText());	2✔
147	this.setImage(pg.getImage());	2✔
148	}
149	}	2✔
150
151	/**
152	* Retrieves an {@link Action} to save the image in a PNG file.
153	*
154	* @return the action
155	*/
156	Action getSavePngAction() {
157	return savePngAction;	2✔
158	}
159
160	Action getSaveDotAction() {
161	return saveDotAction;	2✔
162	}
163
164	@Override
165	protected void paintComponent(Graphics g) {
166	g.setColor(Color.WHITE);	2✔
167	g.fillRect(0, 0, getWidth(), getHeight());	2✔
168	if (img != null) {	2✔
169	g.drawImage(img, 0, 0, null);	2✔
170	}
171	}	2✔
172
173	/*
174	* Based on https://stackoverflow.com/questions/31171502/scroll-jscrollpane-by-dragging-mouse-java-swing/58815302#58815302
175	*/
176	private class DnDMover extends MouseInputAdapter {	2✔
177
178	private final DOTImageComponent cmp;
179	private Point holdPointOnView;
180
181	DnDMover() {	2✔
182	this.cmp = DOTImageComponent.this;	2✔
183	}	2✔
184
185	@Override
186	public void mousePressed(MouseEvent e) {
187	cmp.setCursor(Cursor.getPredefinedCursor(Cursor.MOVE_CURSOR));	2✔
188	holdPointOnView = e.getPoint();	2✔
189	}	2✔
190
191	@Override
192	public void mouseReleased(MouseEvent e) {
193	cmp.setCursor(null);	2✔
194	}	2✔
195
196	@Override
197	public void mouseDragged(MouseEvent e) {
198	final Point dragEventPoint = e.getPoint();	2✔
199	@SuppressWarnings("nullness") // the DOTImageComponent is always embedded in a parent frame
200	final @NonNull JViewport viewport = (JViewport) cmp.getParent();	2✔
201
202	final Point viewPos = viewport.getViewPosition();	2✔
203
204	final int maxViewPosX = cmp.getWidth() - viewport.getWidth();	2✔
205	final int maxViewPosY = cmp.getHeight() - viewport.getHeight();	2✔
206
207	assert holdPointOnView != null;	2✔
208
209	if (cmp.getWidth() > viewport.getWidth()) {	2✔
210	viewPos.x -= dragEventPoint.x - holdPointOnView.x;	2✔
211
212	if (viewPos.x < 0) {	2✔
213	viewPos.x = 0;	2✔
214	holdPointOnView.x = dragEventPoint.x;	2✔
215	}
216
217	if (viewPos.x > maxViewPosX) {	2✔
218	viewPos.x = maxViewPosX;	×
219	holdPointOnView.x = dragEventPoint.x;	×
220	}
221	}
222
223	if (cmp.getHeight() > viewport.getHeight()) {	2✔
224	viewPos.y -= dragEventPoint.y - holdPointOnView.y;	2✔
225
226	if (viewPos.y < 0) {	2✔
227	viewPos.y = 0;	2✔
228	holdPointOnView.y = dragEventPoint.y;	2✔
229	}
230
231	if (viewPos.y > maxViewPosY) {	2✔
232	viewPos.y = maxViewPosY;	×
233	holdPointOnView.y = dragEventPoint.y;	×
234	}
235	}
236
237	viewport.setViewPosition(viewPos);	2✔
238	}	2✔
239	}
240	}

LearnLib / automatalib / 31586418187

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