ProjektGraph/OurApplication/OurDrawArea.java

62 lines
1.6 KiB
Java
Raw Normal View History

2024-07-02 19:13:30 +00:00
package OurApplication;
2024-07-08 19:15:24 +00:00
import graph.*;
2024-07-02 19:13:30 +00:00
import logging.LogElementList;
import visualisation.DrawArea;
import visualizationElements.Edge;
2024-07-08 19:15:24 +00:00
import java.awt.*;
2024-07-02 19:13:30 +00:00
/**
2024-07-08 22:17:31 +00:00
* This class provides an example for using visualization.DrawArea.
* It extends DrawArea to visualize a graph based on logging elements.
*
* @see DrawArea
2024-07-02 19:13:30 +00:00
*/
2024-07-08 22:17:31 +00:00
public class OurDrawArea extends DrawArea {
2024-07-02 19:13:30 +00:00
private static final long serialVersionUID = 1L;
2024-07-08 19:15:24 +00:00
private graph.Graph<VertexMarking, EdgeMarking> currentGraph;
2024-07-03 17:41:46 +00:00
2024-07-02 19:13:30 +00:00
/**
* Standard constructor.
2024-07-08 22:17:31 +00:00
* Initializes an empty draw area.
2024-07-02 19:13:30 +00:00
*/
public OurDrawArea() {
super();
}
2024-07-08 19:15:24 +00:00
2024-07-02 19:13:30 +00:00
/**
2024-07-08 22:17:31 +00:00
* Extended constructor.
* Creates a draw area with a specified log list and display name.
*
* @param logList the draw area's log element list
* @param drawAreaName the display name over the draw area
2024-07-02 19:13:30 +00:00
*/
2024-07-08 22:17:31 +00:00
public OurDrawArea(LogElementList<OurLogElement> logList, String drawAreaName) {
2024-07-02 19:13:30 +00:00
super(logList, drawAreaName);
2024-07-08 19:15:24 +00:00
}
2024-07-02 19:13:30 +00:00
/**
2024-07-08 22:17:31 +00:00
* Draws visualization elements on the draw area.
* @param g the graphics context used for drawing
2024-07-02 19:13:30 +00:00
*/
2024-07-02 22:46:21 +00:00
public void draw(Graphics g) {
2024-07-08 22:17:31 +00:00
// Get the current log element from the log list
2024-07-03 17:41:46 +00:00
OurLogElement logElement = (OurLogElement) logList.get();
2024-07-08 22:17:31 +00:00
// Draw the graph associated with the log element
logElement.getGraph().draw(g);
2024-07-02 19:13:30 +00:00
2024-07-08 22:17:31 +00:00
// Draw markings on edges
for (Edge screenEdge : logElement.getGraph().getEdges()) {
g.drawString(screenEdge.getMarking(),
(screenEdge.getSource().getXpos() + screenEdge.getDestination().getXpos()) / 2,
(screenEdge.getSource().getYpos() + screenEdge.getDestination().getYpos()) / 2);
}
2024-07-02 19:13:30 +00:00
}
2024-07-03 17:41:46 +00:00
2024-07-02 19:13:30 +00:00
}