diff --git a/graphminimize/src/main/java/GraphMinimize.java b/graphminimize/src/main/java/GraphMinimize.java
index 2801450d4cf9a8b534d9ace13757d87a49495fb9..57141ce403f773a0a7830fe769c07a67d5598d8f 100755
--- a/graphminimize/src/main/java/GraphMinimize.java
+++ b/graphminimize/src/main/java/GraphMinimize.java
@@ -156,7 +156,7 @@ public class GraphMinimize {
graph.minimizeTau(hasTauOnly(args));
- graph.display(true);
+ graph.display(true, false);
}
} // Class GraphShow
diff --git a/graphshow/src/main/java/GraphShow.java b/graphshow/src/main/java/GraphShow.java
index a8333f593b9a5268c6f7f99a978ab0adfb279632..3170ff4ff08f71aacbb4e041780982a34e0c819e 100755
--- a/graphshow/src/main/java/GraphShow.java
+++ b/graphshow/src/main/java/GraphShow.java
@@ -137,7 +137,7 @@ public class GraphShow {
System.out.println("Graph has " + graph.getNbOfStates() + " states and " + graph.getNbOfTransitions() + " transitions.");
- graph.display(true);
+ graph.display(true, false);
}
diff --git a/modeling/AVATAR/testDependencyGraphs.xml b/modeling/AVATAR/testDependencyGraphs.xml
index 704ff892a79fdc871c2a61b33188e7019d78d8bc..272ef9c51575ce8c0f7ab7da9314d6302817edc5 100644
--- a/modeling/AVATAR/testDependencyGraphs.xml
+++ b/modeling/AVATAR/testDependencyGraphs.xml
@@ -1858,11 +1858,11 @@ Double-click to edit
</COMPONENT>
<SUBCOMPONENT type="5000" id="957" index="3" uid="08f5deac-ff7e-424d-9124-5dd57f0a2ebe" >
<father id="1039" num="0" />
-<cdparam x="279" y="67" />
-<sizeparam width="83" height="71" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="366" y="66" />
+<sizeparam width="79" height="71" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="93" minY="0" maxY="45" />
-<infoparam name="Block0" value="Instance1" />
+<cdrectangleparam minX="0" maxX="97" minY="0" maxY="45" />
+<infoparam name="Block0" value="Instance2" />
<TGConnectingPoint num="0" id="917" />
<TGConnectingPoint num="1" id="918" />
<TGConnectingPoint num="2" id="919" />
@@ -1910,11 +1910,11 @@ Double-click to edit
</SUBCOMPONENT>
<SUBCOMPONENT type="5000" id="998" index="4" uid="08f5deac-ff7e-424d-9124-5dd57f0a2ebe" >
<father id="1039" num="1" />
-<cdparam x="366" y="66" />
-<sizeparam width="79" height="71" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="279" y="67" />
+<sizeparam width="83" height="71" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="97" minY="0" maxY="45" />
-<infoparam name="Block0" value="Instance2" />
+<cdrectangleparam minX="0" maxX="93" minY="0" maxY="45" />
+<infoparam name="Block0" value="Instance1" />
<TGConnectingPoint num="0" id="958" />
<TGConnectingPoint num="1" id="959" />
<TGConnectingPoint num="2" id="960" />
@@ -2929,13 +2929,13 @@ Double-click to edit
<Signal value="in answer()" attached="true" />
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="5000" id="1508" index="4" uid="1f2ca3b6-69b5-4809-9120-4e63b74dd9d9" >
+<SUBCOMPONENT type="5000" id="1508" index="4" uid="38090441-87bf-4259-b51d-053be523a93e" >
<father id="1590" num="0" />
-<cdparam x="412" y="230" />
-<sizeparam width="141" height="88" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="571" y="228" />
+<sizeparam width="150" height="92" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="215" minY="0" maxY="158" />
-<infoparam name="Block0" value="Client1" />
+<cdrectangleparam minX="0" maxX="206" minY="0" maxY="154" />
+<infoparam name="Block0" value="Client2" />
<TGConnectingPoint num="0" id="1468" />
<TGConnectingPoint num="1" id="1469" />
<TGConnectingPoint num="2" id="1470" />
@@ -2981,13 +2981,13 @@ Double-click to edit
<CryptoBlock value="false" />
</extraparam>
</SUBCOMPONENT>
-<SUBCOMPONENT type="5000" id="1549" index="5" uid="38090441-87bf-4259-b51d-053be523a93e" >
+<SUBCOMPONENT type="5000" id="1549" index="5" uid="1f2ca3b6-69b5-4809-9120-4e63b74dd9d9" >
<father id="1590" num="1" />
-<cdparam x="571" y="228" />
-<sizeparam width="150" height="92" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="412" y="230" />
+<sizeparam width="141" height="88" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="206" minY="0" maxY="154" />
-<infoparam name="Block0" value="Client2" />
+<cdrectangleparam minX="0" maxX="215" minY="0" maxY="158" />
+<infoparam name="Block0" value="Client1" />
<TGConnectingPoint num="0" id="1509" />
<TGConnectingPoint num="1" id="1510" />
<TGConnectingPoint num="2" id="1511" />
@@ -3909,8 +3909,8 @@ Double-click to edit
<infoparam name="connector" value="" />
<TGConnectingPoint num="0" id="1977" />
<TGConnectingPoint num="1" id="1978" />
-<P1 x="921" y="357" id="2029" />
-<P2 x="1023" y="392" id="1987" />
+<P1 x="921" y="357" id="1988" />
+<P2 x="1023" y="392" id="2028" />
<Point x="921" y="391" />
<AutomaticDrawing data="true" />
<extraparam>
@@ -3993,13 +3993,13 @@ Double-click to edit
<Signal value="in value()" attached="true" />
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="5000" id="2022" index="5" uid="1c21ee3a-d0b2-4f9a-92bf-e9341f5daaa1" >
+<SUBCOMPONENT type="5000" id="2022" index="5" uid="b9daba4a-7b74-4e52-8bd9-b5bc9df56d86" >
<father id="2104" num="0" />
-<cdparam x="1023" y="234" />
-<sizeparam width="143" height="158" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="830" y="238" />
+<sizeparam width="183" height="119" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="221" minY="0" maxY="95" />
-<infoparam name="Block" value="center1" />
+<cdrectangleparam minX="0" maxX="181" minY="0" maxY="134" />
+<infoparam name="Block" value="Filter" />
<TGConnectingPoint num="0" id="1982" />
<TGConnectingPoint num="1" id="1983" />
<TGConnectingPoint num="2" id="1984" />
@@ -4043,16 +4043,16 @@ Double-click to edit
<extraparam>
<blockType data="block" color="-4072719" />
<CryptoBlock value="false" />
-<Signal value="in query()" attached="true" />
+<Signal value="out query()" attached="true" />
</extraparam>
</SUBCOMPONENT>
-<SUBCOMPONENT type="5000" id="2063" index="6" uid="b9daba4a-7b74-4e52-8bd9-b5bc9df56d86" >
+<SUBCOMPONENT type="5000" id="2063" index="6" uid="1c21ee3a-d0b2-4f9a-92bf-e9341f5daaa1" >
<father id="2104" num="1" />
-<cdparam x="830" y="238" />
-<sizeparam width="183" height="119" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="1023" y="234" />
+<sizeparam width="143" height="158" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="181" minY="0" maxY="134" />
-<infoparam name="Block" value="Filter" />
+<cdrectangleparam minX="0" maxX="221" minY="0" maxY="95" />
+<infoparam name="Block" value="center1" />
<TGConnectingPoint num="0" id="2023" />
<TGConnectingPoint num="1" id="2024" />
<TGConnectingPoint num="2" id="2025" />
@@ -4096,7 +4096,7 @@ Double-click to edit
<extraparam>
<blockType data="block" color="-4072719" />
<CryptoBlock value="false" />
-<Signal value="out query()" attached="true" />
+<Signal value="in query()" attached="true" />
</extraparam>
</SUBCOMPONENT>
@@ -4152,13 +4152,13 @@ Double-click to edit
<Signal value="out value()" attached="true" />
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="5000" id="2145" index="7" uid="b0f72ee8-81dc-4a55-b945-936ed82b727e" >
+<SUBCOMPONENT type="5000" id="2145" index="7" uid="d32fb600-eac8-4ee5-aa40-e223c4804bf6" >
<father id="2227" num="0" />
-<cdparam x="252" y="231" />
-<sizeparam width="157" height="119" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="424" y="232" />
+<sizeparam width="168" height="117" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="225" minY="0" maxY="157" />
-<infoparam name="Block" value="Sensor1" />
+<cdrectangleparam minX="0" maxX="214" minY="0" maxY="159" />
+<infoparam name="Block" value="Sensor2" />
<TGConnectingPoint num="0" id="2105" />
<TGConnectingPoint num="1" id="2106" />
<TGConnectingPoint num="2" id="2107" />
@@ -4204,13 +4204,13 @@ Double-click to edit
<CryptoBlock value="false" />
</extraparam>
</SUBCOMPONENT>
-<SUBCOMPONENT type="5000" id="2186" index="8" uid="d32fb600-eac8-4ee5-aa40-e223c4804bf6" >
+<SUBCOMPONENT type="5000" id="2186" index="8" uid="b0f72ee8-81dc-4a55-b945-936ed82b727e" >
<father id="2227" num="1" />
-<cdparam x="424" y="232" />
-<sizeparam width="168" height="117" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="252" y="231" />
+<sizeparam width="157" height="119" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="214" minY="0" maxY="159" />
-<infoparam name="Block" value="Sensor2" />
+<cdrectangleparam minX="0" maxX="225" minY="0" maxY="157" />
+<infoparam name="Block" value="Sensor1" />
<TGConnectingPoint num="0" id="2146" />
<TGConnectingPoint num="1" id="2147" />
<TGConnectingPoint num="2" id="2148" />
diff --git a/src/main/java/graph/AUTGraph.java b/src/main/java/graph/AUTGraph.java
index d33f5e7905d2b243041e5a05bf74b3b705a63a77..5b1bfedc359d6fd08d8e273b5ef435c548581972 100755
--- a/src/main/java/graph/AUTGraph.java
+++ b/src/main/java/graph/AUTGraph.java
@@ -510,12 +510,17 @@ public class AUTGraph implements myutil.Graph {
}
}
+
+ public void display(boolean forceAutoLayout) {
+ display(false, forceAutoLayout);
+ }
+
public void display() {
- display(false);
+ display(false, true);
}
- public void display(boolean exitOnClose) {
- AUTGraphDisplay display = new AUTGraphDisplay(this, exitOnClose);
+ public void display(boolean exitOnClose, boolean forceAutoLayout) {
+ AUTGraphDisplay display = new AUTGraphDisplay(this, exitOnClose, forceAutoLayout);
display.display();
}
diff --git a/src/main/java/graph/AUTGraphDisplay.java b/src/main/java/graph/AUTGraphDisplay.java
index 9c8374213120f8511b86594a9215d485731e4c59..f01d4c92efd7c73f1292e1e5fac37ca1485dd87e 100755
--- a/src/main/java/graph/AUTGraphDisplay.java
+++ b/src/main/java/graph/AUTGraphDisplay.java
@@ -42,30 +42,21 @@ package graph;
import common.ConfigurationTTool;
import common.SpecConfigTTool;
import myutil.TraceManager;
-import org.apache.batik.anim.timing.Trace;
import org.graphstream.algorithm.Toolkit;
import org.graphstream.graph.Edge;
import org.graphstream.graph.Node;
-import org.graphstream.graph.implementations.AbstractEdge;
import org.graphstream.graph.implementations.MultiGraph;
-import org.graphstream.graph.implementations.MultiNode;
import org.graphstream.stream.ProxyPipe;
-import org.graphstream.ui.geom.Point2;
import org.graphstream.ui.geom.Point3;
+import org.graphstream.ui.graphicGraph.GraphicGraph;
import org.graphstream.ui.swing.SwingGraphRenderer;
import org.graphstream.ui.swing_viewer.DefaultView;
import org.graphstream.ui.swing_viewer.SwingViewer;
-import org.graphstream.ui.graphicGraph.GraphicElement;
import org.graphstream.ui.view.View;
-import org.graphstream.ui.swing_viewer.ViewPanel;
-import org.graphstream.ui.view.View;
-import org.graphstream.algorithm.Toolkit.*;
import org.graphstream.ui.view.Viewer;
import org.graphstream.ui.view.ViewerListener;
-import org.graphstream.ui.view.ViewerPipe;
import org.graphstream.ui.view.camera.Camera;
-import org.graphstream.ui.view.util.InteractiveElement;
-import ui.MainGUI;
+import org.graphstream.ui.view.util.ShortcutManager;
import ui.file.PNGFilter;
import ui.util.IconManager;
@@ -77,7 +68,6 @@ import java.awt.geom.AffineTransform;
import java.awt.image.BufferedImage;
import java.io.File;
import java.util.ArrayList;
-import java.util.EnumSet;
import java.util.HashSet;
import java.util.logging.Logger;
@@ -91,27 +81,12 @@ import java.util.logging.Logger;
*/
public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable {
- protected AUTGraph graph;
- protected SwingViewer viewer;
- protected MultiGraph vGraph;
- protected boolean loop;
- protected Node firstNode;
- protected ArrayList<Edge> edges;
- protected boolean exitOnClose = false;
- protected BasicFrame bf;
-
- protected String USED_STYLE_SHEET = "";
-
- // see http://graphstream-project.org/doc/Advanced-Concepts/GraphStream-CSS-Reference/
-
-
protected static String STYLE_SHEET = "node {fill-color: #B1CAF1; text-color: black; size: 20px, 20px; text-size:14;} " +
"edge {text-color: black; shape: cubic-curve; text-size:10;} " +
"edge.defaultedge {text-size:10; text-color:black;} " +
"edge.external {text-color:blue; text-size:14;} " +
"node.deadlock {fill-color: orange; text-color: red; size: 20px, 20px; text-size:15;} " +
"node.init { fill-color: green; text-color: black; size: 20px, 20px; text-size:15;}";
-
protected static String STYLE_SHEET2 = "graph { canvas-color: white; fill-mode: gradient-vertical; fill-color: white, #004; padding: 20px; } " +
"node { shape: circle; size-mode: dyn-size; size: 10px; fill-mode: gradient-radial; fill-color: #FFFC, #FFF0; stroke-mode: none; " +
"shadow-mode: gradient-radial; shadow-color: #FFF5, #FFF0; shadow-width: 5px; shadow-offset: 0px, 0px; } " +
@@ -120,11 +95,24 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
"edge.defaultedge { shape: curve-cubic; size: 1px; fill-color: #FFF3; fill-mode: plain; arrow-shape: none; } " +
"edge.external { shape: L-square-line; size: 3px; fill-color: #AAA3; fill-mode: plain; arrow-shape: circle; } " +
"sprite { shape: circle; fill-mode: gradient-radial; fill-color: #FFF8, #FFF0; }";
+ protected AUTGraph graph;
+ protected SwingViewer viewer;
+ protected MultiGraph vGraph;
+ protected boolean loop;
+ protected Node firstNode;
+ protected ArrayList<Edge> edges;
+ protected boolean exitOnClose = false;
+ protected BasicFrame bf;
+
+ // see http://graphstream-project.org/doc/Advanced-Concepts/GraphStream-CSS-Reference/
+ protected boolean forceAutoLayout;
+ protected String USED_STYLE_SHEET = "";
- public AUTGraphDisplay(AUTGraph _graph, boolean _exitOnClose) {
+ public AUTGraphDisplay(AUTGraph _graph, boolean _exitOnClose, boolean _forceAutoLayout) {
graph = _graph;
exitOnClose = _exitOnClose;
+ forceAutoLayout = _forceAutoLayout;
System.setProperty("org.graphstream.ui", "swing");
}
@@ -215,7 +203,7 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
//viewer.setCloseFramePolicy(Viewer.CloseFramePolicy.CLOSE_VIEWER);
- bf = new BasicFrame(this, viewer, vGraph, graph, edges, exitOnClose);
+ bf = new BasicFrame(this, viewer, vGraph, graph, edges, exitOnClose, forceAutoLayout);
loop = true;
@@ -335,55 +323,55 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
}
-class BasicFrame extends JFrame implements ActionListener {
- protected MultiGraph vGraph;
- protected SwingViewer viewer;
- protected JPanel viewerPanel;
- protected AUTGraph graph;
- protected ArrayList<Edge> edges;
+ class BasicFrame extends JFrame implements ActionListener {
+ public AffineTransform transform;
+ protected MultiGraph vGraph;
+ protected SwingViewer viewer;
+ protected JPanel viewerPanel;
+ protected AUTGraph graph;
+ protected ArrayList<Edge> edges;
+ protected JButton close;
+ protected JButton screenshot;
+ protected JButton fontPlus, fontMinus;
+ protected JButton resetView;
+ protected JCheckBox autoLayout;
+ protected JCheckBox internalActions;
+ protected JCheckBox readActions;
+ protected JCheckBox higherQuality, antialiasing;
+ protected JLabel help, info;
+ protected MouseEvent last;
- protected JButton close;
- protected JButton screenshot;
- protected JButton fontPlus, fontMinus;
- protected JButton resetView;
- protected JCheckBox autoLayout;
- protected JCheckBox internalActions;
- protected JCheckBox readActions;
- protected JCheckBox higherQuality, antialiasing;
- protected JLabel help, info;
+ protected boolean exitOnClose;
- public AffineTransform transform;
+ private AUTGraphDisplay autD;
- protected MouseEvent last;
+ private DefaultView dv;
+ private Node selectedNode;
- protected boolean exitOnClose;
+ private boolean forceAutoLayout;
- private AUTGraphDisplay autD;
- private DefaultView dv;
- private Node selectedNode;
+ public BasicFrame(AUTGraphDisplay autD, SwingViewer viewer, MultiGraph vGraph, AUTGraph autgraph, ArrayList<Edge> _edges,
+ boolean _exitOnClose, boolean _forceAutoLayout) {
+ this.autD = autD;
+ this.viewer = viewer;
+ this.vGraph = vGraph;
+ this.graph = autgraph;
+ forceAutoLayout = _forceAutoLayout;
- public BasicFrame(AUTGraphDisplay autD, SwingViewer viewer, MultiGraph vGraph, AUTGraph autgraph, ArrayList<Edge> _edges,
- boolean _exitOnClose) {
- this.autD = autD;
- this.viewer = viewer;
- this.vGraph = vGraph;
- this.graph = autgraph;
+ edges = _edges;
+ exitOnClose = _exitOnClose;
+ makeComponents();
+ if (exitOnClose) {
+ setDefaultCloseOperation(WindowConstants.EXIT_ON_CLOSE);
+ }
- edges = _edges;
- exitOnClose = _exitOnClose;
- makeComponents();
-
- if (exitOnClose) {
- setDefaultCloseOperation(WindowConstants.EXIT_ON_CLOSE);
}
- }
-
- public void processDrag(MouseEvent event) {
+ public void processDrag(MouseEvent event) {
/*if (last != null) {
Camera camera = dv.getCamera();
Point3 p1 = camera.getViewCenter();
@@ -397,448 +385,508 @@ class BasicFrame extends JFrame implements ActionListener {
camera.setViewCenter(p3.x,p3.y, 0);
}
last=event;*/
- }
+ }
- public void resetDrag() {
- //this.last=null;
- }
+ public void resetDrag() {
+ //this.last=null;
+ }
- public void makeComponents() {
+ public void makeComponents() {
+ dv = new DefaultView(viewer, "Graph", new SwingGraphRenderer());
- dv = new DefaultView(viewer, "Graph", new SwingGraphRenderer());
+ MouseListener[] listeners = dv.getMouseListeners();
+ for (MouseListener l : listeners) {
+ dv.removeMouseListener(l);
+ }
- MouseListener[] listeners = dv.getMouseListeners();
- for(MouseListener l: listeners) {
- dv.removeMouseListener(l);
- }
+ MouseMotionListener[] mL = dv.getMouseMotionListeners();
+ for (MouseMotionListener l : mL) {
+ dv.removeMouseMotionListener(l);
+ }
- MouseMotionListener[] mL = dv.getMouseMotionListeners();
- for(MouseMotionListener l: mL) {
- //dv.removeMouseMotionListener(l);
- }
+ KeyListener[] keyListeners = dv.getKeyListeners();
+ for (KeyListener k : keyListeners) {
+ dv.removeKeyListener(k);
+ }
+ dv.setShortcutManager(new ShortcutManager() {
- dv.addKeyListener(new KeyListener() {
- @Override
- public void keyTyped(KeyEvent e) {
+ private View view;
- }
+ @Override
+ public void init(GraphicGraph graph, View view) {
+ this.view = view;
+ ((Component)view).addKeyListener(this);
+ }
- @Override
- public void keyPressed(KeyEvent e) {
+ @Override
+ public void release() {
+ view.removeKeyListener(this);
+ }
- }
+ @Override
+ public void keyPressed(KeyEvent e) {
+ System.out.println("keyPressed!");
+ }
- @Override
- public void keyReleased(KeyEvent e) {
+ @Override
+ public void keyReleased(KeyEvent e) {
+ System.out.println("keyReleased!");
+ }
- TraceManager.addDev("Key event:" + e.getKeyCode());
- updateMe();
- }
- });
-
- dv.addMouseMotionListener(new MouseMotionListener() {
-
- @Override
- public void mouseDragged(MouseEvent e) {
- //TraceManager.addDev("Dragged!");
- if (selectedNode != null) {
- double diffX = 1;
- double diffY = 1;
- if (transform != null) {
- diffX = transform.getScaleX();
- diffY = transform.getScaleY();
+ @Override
+ public void keyTyped(KeyEvent e) {
+ System.out.println("keyTyped!");
+ }
+ });
+
+ /*((Component) dv).addKeyListener(new KeyListener() {
+ @Override
+ public void keyTyped(KeyEvent e) {
+ TraceManager.addDev("Key pressed event:" + e.getKeyCode());
+ updateMe();
+ }
+
+ @Override
+ public void keyPressed(KeyEvent e) {
+ TraceManager.addDev("Key pressed event:" + e.getKeyCode());
+ updateMe();
+ }
+
+ @Override
+ public void keyReleased(KeyEvent e) {
+
+ TraceManager.addDev("Key event:" + e.getKeyCode());
+ updateMe();
+ }
+ });*/
+
+
+ dv.addMouseMotionListener(new MouseMotionListener() {
+
+ @Override
+ public void mouseDragged(MouseEvent e) {
+ //TraceManager.addDev("Dragged!");
+ if (selectedNode != null) {
+ double diffX = 1;
+ double diffY = 1;
+ if (transform != null) {
+ diffX = transform.getScaleX();
+ diffY = transform.getScaleY();
+ }
+ Point3 p = dv.getCamera().transformPxToGu(e.getX() * diffX, e.getY() * diffY);
+ selectedNode.setAttribute("x", p.x);
+ selectedNode.setAttribute("y", p.y);
}
- Point3 p = dv.getCamera().transformPxToGu(e.getX()*diffX, e.getY()*diffY);
- selectedNode.setAttribute("x", p.x);
- selectedNode.setAttribute("y", p.y);
+ processDrag(e);
}
- processDrag(e);
- }
- @Override
- public void mouseMoved(MouseEvent e) {
+ @Override
+ public void mouseMoved(MouseEvent e) {
- }
- });
+ }
+ });
- dv.addMouseListener(new MouseListener() {
- @Override
- public void mouseClicked(MouseEvent e) {
- //TraceManager.addDev("Mouse clicked!");
- }
+ dv.addMouseListener(new MouseListener() {
+ @Override
+ public void mouseClicked(MouseEvent e) {
+ //TraceManager.addDev("Mouse clicked!");
+ }
- @Override
- public void mousePressed(MouseEvent e) {
+ @Override
+ public void mousePressed(MouseEvent e) {
- Graphics2D g = (Graphics2D) dv.getGraphics ();
- transform = g.getFontRenderContext ().getTransform ();
- TraceManager.addDev("Affine transform = " + transform);
+ Graphics2D g = (Graphics2D) dv.getGraphics();
+ transform = g.getFontRenderContext().getTransform();
+ //TraceManager.addDev("Affine transform = " + transform);
- //setAutoLayout(false);
- //viewer.disableAutoLayout();
- TraceManager.addDev("Mouse pressed!");
+ //setAutoLayout(false);
+ //viewer.disableAutoLayout();
+ //TraceManager.addDev("Mouse pressed!");
- Node node = findNodeAt(e.getX(), e.getY());
- if (node != null) {
- TraceManager.addDev("Mouse pressed at node: " + node.getId());
- selectedNode = node;
- } else {
- TraceManager.addDev("Mouse pressed not on a node");
- }
+ Node node = findNodeAt(e.getX(), e.getY());
+ if (node != null) {
+ //TraceManager.addDev("Mouse pressed at node: " + node.getId());
+ selectedNode = node;
+ } else {
+ //TraceManager.addDev("Mouse pressed not on a node");
+ }
- resetDrag();
+ resetDrag();
- }
+ }
- @Override
- public void mouseReleased(MouseEvent e) {
- TraceManager.addDev("Mouse released!");
- selectedNode = null;
- //viewer.enableAutoLayout();
- }
+ @Override
+ public void mouseReleased(MouseEvent e) {
+ //TraceManager.addDev("Mouse released!");
+ selectedNode = null;
+ //viewer.enableAutoLayout();
+ }
- @Override
- public void mouseEntered(MouseEvent e) {
+ @Override
+ public void mouseEntered(MouseEvent e) {
- }
+ }
- @Override
- public void mouseExited(MouseEvent e) {
+ @Override
+ public void mouseExited(MouseEvent e) {
+ }
+ });
+
+
+ ((Component) dv).addMouseWheelListener(new MouseWheelListener() {
+ @Override
+ public void mouseWheelMoved(MouseWheelEvent e) {
+ e.consume();
+ int i = e.getWheelRotation();
+ TraceManager.addDev("Wheel rotation:" + i);
+ double factor = Math.pow(1.01, i);
+ Camera cam = dv.getCamera();
+ double zoom = cam.getViewPercent() * factor;
+ /*Point2 pxCenter = cam.transformGuToPx(cam.getViewCenter().x, cam.getViewCenter().y, 0);
+ double diffX = 1;
+ double diffY = 1;
+ if (transform != null) {
+ diffX = transform.getScaleX();
+ diffY = transform.getScaleY();
+ }
+ Point3 guClicked = cam.transformPxToGu(e.getX()*diffX, e.getY()*diffY);
+
+ double newRatioPx2Gu = cam.getMetrics().ratioPx2Gu/factor;
+ double x = guClicked.x + (pxCenter.x - e.getX())/newRatioPx2Gu;
+ double y = guClicked.y - (pxCenter.y - e.getY())/newRatioPx2Gu;
+ cam.setViewCenter(x, y, 0);*/
+ cam.setViewPercent(zoom);
+ }
+ });
+
+
+ //Graphics g = dv.getGraphics();
+ //TraceManager.addDev("Transform:" + ((Graphics2D)g).getTransform());
+ //TraceManager.addDev("scale:" + System.getProperty("sun.java2d.uiScale"));
+
+
+ add(dv, BorderLayout.CENTER);
+
+ //add(viewer, BorderLayout.CENTER );
+ close = new JButton("Close", IconManager.imgic27);
+ close.addActionListener(this);
+ screenshot = new JButton("Save in png", IconManager.imgic28);
+ screenshot.addActionListener(this);
+ fontPlus = new JButton(IconManager.imgic144);
+ fontPlus.addActionListener(this);
+ fontMinus = new JButton(IconManager.imgic146);
+ fontMinus.addActionListener(this);
+ resetView = new JButton("Reset view");
+ resetView.addActionListener(this);
+ autoLayout = new JCheckBox("Auto layout", true);
+ autoLayout.addActionListener(this);
+ close.addActionListener(this);
+ help = new JLabel("Zoom with mouse wheel or PageUp/PageDown, move with cursor keys");
+ help = new JLabel("click on a node and drag it to move it");
+ info = new JLabel("Graph: " + graph.getNbOfStates() + " states, " + graph.getNbOfTransitions() + " transitions");
+ internalActions = new JCheckBox("Display internal actions", true);
+ internalActions.addActionListener(this);
+ readActions = new JCheckBox("Display read/write actions", true);
+ readActions.addActionListener(this);
+ higherQuality = new JCheckBox("Higher drawing quality", false);
+ higherQuality.addActionListener(this);
+ antialiasing = new JCheckBox("Anti aliasing", false);
+ antialiasing.addActionListener(this);
+
+
+ JPanel jp01 = new JPanel();
+ GridBagLayout gridbag01 = new GridBagLayout();
+ GridBagConstraints c01 = new GridBagConstraints();
+ jp01.setLayout(gridbag01);
+ jp01.setBorder(new javax.swing.border.TitledBorder("Options"));
+ //c01.gridwidth = 1;
+ c01.gridheight = 1;
+ c01.weighty = 1.0;
+ c01.weightx = 1.0;
+ c01.fill = GridBagConstraints.HORIZONTAL;
+ c01.gridwidth = GridBagConstraints.REMAINDER; //end row
+ jp01.add(screenshot);
+ jp01.add(internalActions);
+ jp01.add(readActions);
+ jp01.add(higherQuality);
+ jp01.add(antialiasing);
+ if (!forceAutoLayout) {
+ jp01.add(autoLayout);
}
- });
-
-
- //Graphics g = dv.getGraphics();
- //TraceManager.addDev("Transform:" + ((Graphics2D)g).getTransform());
- //TraceManager.addDev("scale:" + System.getProperty("sun.java2d.uiScale"));
-
-
-
- add(dv, BorderLayout.CENTER);
-
- //add(viewer, BorderLayout.CENTER );
- close = new JButton("Close", IconManager.imgic27);
- close.addActionListener(this);
- screenshot = new JButton("Save in png", IconManager.imgic28);
- screenshot.addActionListener(this);
- fontPlus = new JButton(IconManager.imgic144);
- fontPlus.addActionListener(this);
- fontMinus = new JButton(IconManager.imgic146);
- fontMinus.addActionListener(this);
- resetView = new JButton("Reset view");
- resetView.addActionListener(this);
- autoLayout = new JCheckBox("Auto layout", true);
- autoLayout.addActionListener(this);
- close.addActionListener(this);
- help = new JLabel("Zoom with mouse wheel or PageUp/PageDown, move with cursor keys");
- help = new JLabel("click on a node and drag it to move it");
- info = new JLabel("Graph: " + graph.getNbOfStates() + " states, " + graph.getNbOfTransitions() + " transitions");
- internalActions = new JCheckBox("Display internal actions", true);
- internalActions.addActionListener(this);
- readActions = new JCheckBox("Display read/write actions", true);
- readActions.addActionListener(this);
- higherQuality = new JCheckBox("Higher drawing quality", false);
- higherQuality.addActionListener(this);
- antialiasing = new JCheckBox("Anti aliasing", false);
- antialiasing.addActionListener(this);
-
-
- JPanel jp01 = new JPanel();
- GridBagLayout gridbag01 = new GridBagLayout();
- GridBagConstraints c01 = new GridBagConstraints();
- jp01.setLayout(gridbag01);
- jp01.setBorder(new javax.swing.border.TitledBorder("Options"));
- //c01.gridwidth = 1;
- c01.gridheight = 1;
- c01.weighty = 1.0;
- c01.weightx = 1.0;
- c01.fill = GridBagConstraints.HORIZONTAL;
- c01.gridwidth = GridBagConstraints.REMAINDER; //end row
- jp01.add(screenshot);
- jp01.add(internalActions);
- jp01.add(readActions);
- jp01.add(higherQuality);
- jp01.add(antialiasing);
- if (MainGUI.experimentalOn) {
- jp01.add(autoLayout);
+ jp01.add(fontMinus);
+ jp01.add(fontPlus);
+ jp01.add(resetView);
+
+ JPanel infoPanel = new JPanel(new BorderLayout());
+ JPanel labelPanel = new JPanel(new BorderLayout());
+ labelPanel.add(help, BorderLayout.EAST);
+ labelPanel.add(info, BorderLayout.WEST);
+ infoPanel.add(labelPanel, BorderLayout.NORTH);
+ infoPanel.add(close, BorderLayout.SOUTH);
+ infoPanel.add(jp01, BorderLayout.CENTER);
+
+
+ add(infoPanel, BorderLayout.SOUTH);
+ //setDefaultCloseOperation(EXIT_ON_CLOSE);
+ setSize(1000, 700);
+ setVisible(true);
}
- jp01.add(fontMinus);
- jp01.add(fontPlus);
- jp01.add(resetView);
-
- JPanel infoPanel = new JPanel(new BorderLayout());
- JPanel labelPanel = new JPanel(new BorderLayout());
- labelPanel.add(help, BorderLayout.EAST);
- labelPanel.add(info, BorderLayout.WEST);
- infoPanel.add(labelPanel, BorderLayout.NORTH);
- infoPanel.add(close, BorderLayout.SOUTH);
- infoPanel.add(jp01, BorderLayout.CENTER);
-
-
- add(infoPanel, BorderLayout.SOUTH);
- //setDefaultCloseOperation(EXIT_ON_CLOSE);
- setSize(1000, 700);
- setVisible(true);
- }
- public void actionPerformed(ActionEvent evt) {
- if (evt.getSource() == close) {
- closeFrame();
- } else if (evt.getSource() == screenshot) {
- screenshot();
- } else if (evt.getSource() == internalActions) {
- manageInternalActions();
- } else if (evt.getSource() == readActions) {
- manageReadActions();
- } else if (evt.getSource() == higherQuality) {
- manageHigherQuality();
- } else if (evt.getSource() == antialiasing) {
- manageAntialiasing();
- } else if (evt.getSource() == fontPlus) {
- fontPlus();
- } else if (evt.getSource() == fontMinus) {
- fontMinus();
- } else if (evt.getSource() == resetView) {
- dv.getCamera().resetView();
- updateMe();
- } else if (evt.getSource() == autoLayout) {
- if (autoLayout.isSelected()) {
- viewer.enableAutoLayout();
- } else {
- viewer.disableAutoLayout();
+ public void actionPerformed(ActionEvent evt) {
+ if (evt.getSource() == close) {
+ closeFrame();
+ } else if (evt.getSource() == screenshot) {
+ screenshot();
+ } else if (evt.getSource() == internalActions) {
+ manageInternalActions();
+ } else if (evt.getSource() == readActions) {
+ manageReadActions();
+ } else if (evt.getSource() == higherQuality) {
+ manageHigherQuality();
+ } else if (evt.getSource() == antialiasing) {
+ manageAntialiasing();
+ } else if (evt.getSource() == fontPlus) {
+ fontPlus();
+ } else if (evt.getSource() == fontMinus) {
+ fontMinus();
+ } else if (evt.getSource() == resetView) {
+ dv.getCamera().resetView();
+ updateMe();
+ } else if (evt.getSource() == autoLayout) {
+ if (autoLayout.isSelected()) {
+ viewer.enableAutoLayout();
+ } else {
+ viewer.disableAutoLayout();
+ }
}
}
- }
- public void closeFrame() {
- if (autD != null) {
- autD.viewClosed("closed pushed");
- }
- if (exitOnClose) {
- System.exit(1);
+ public void closeFrame() {
+ if (autD != null) {
+ autD.viewClosed("closed pushed");
+ }
+ if (exitOnClose) {
+ System.exit(1);
+ }
+ dispose();
}
- dispose();
- }
-
- public void takeScreenshot(Component component, File file) {
- BufferedImage image = new BufferedImage(
- component.getWidth(),
- component.getHeight(),
- BufferedImage.TYPE_INT_RGB
- );
- // call the Component's paint method, using
- // the Graphics object of the image.
- component.paint(image.getGraphics()); // alternately use .printAll(..)
- try {
- // save captured image to PNG file
- ImageIO.write(image, "png", file);
- } catch (Exception e) {
- }
+ public void takeScreenshot(Component component, File file) {
+ BufferedImage image = new BufferedImage(
+ component.getWidth(),
+ component.getHeight(),
+ BufferedImage.TYPE_INT_RGB
+ );
+ // call the Component's paint method, using
+ // the Graphics object of the image.
+ component.paint(image.getGraphics()); // alternately use .printAll(..)
- }
+ try {
+ // save captured image to PNG file
+ ImageIO.write(image, "png", file);
+ } catch (Exception e) {
+ }
- public void fontPlus() {
- setTextSize(1);
+ }
- }
+ public void fontPlus() {
+ setTextSize(1);
- public void fontMinus() {
- setTextSize(-1);
- }
+ }
- private void setTextSize(int modifier) {
- String style = USED_STYLE_SHEET;
- if ((style == null) || (style.length() == 0)) {
- return;
+ public void fontMinus() {
+ setTextSize(-1);
}
- // default.edge
- //TraceManager.addDev("Old style: " + style);
- style = modifyTextSize(modifier, style, "node ");
- style = modifyTextSize(modifier, style, "node.deadlock");
- style = modifyTextSize(modifier, style, "node.init");
- style = modifyTextSize(modifier, style, "edge ");
- style = modifyTextSize(modifier, style, "edge.defaultedge");
- //TraceManager.addDev("New style default: " + style);
- // external
- style = modifyTextSize(modifier, style, "edge.external");
- //TraceManager.addDev("New style external: " + style);
- vGraph.setAttribute("ui.stylesheet", style);
- USED_STYLE_SHEET = style;
+ private void setTextSize(int modifier) {
+ String style = USED_STYLE_SHEET;
+ if ((style == null) || (style.length() == 0)) {
+ return;
+ }
+ // default.edge
+ //TraceManager.addDev("Old style: " + style);
+ style = modifyTextSize(modifier, style, "node ");
+ style = modifyTextSize(modifier, style, "node.deadlock");
+ style = modifyTextSize(modifier, style, "node.init");
+ style = modifyTextSize(modifier, style, "edge ");
+ style = modifyTextSize(modifier, style, "edge.defaultedge");
+ //TraceManager.addDev("New style default: " + style);
+ // external
+ style = modifyTextSize(modifier, style, "edge.external");
+ //TraceManager.addDev("New style external: " + style);
+ vGraph.setAttribute("ui.stylesheet", style);
+ USED_STYLE_SHEET = style;
- }
- public String modifyTextSize(int modifier, String input, String key) {
- String ret = input;
- int indexD = input.indexOf(key);
- if (indexD != -1) {
- String before = input.substring(0, indexD);
-
- String tmp = input.substring(indexD);
- int indexBB = tmp.indexOf("{");
- int indexBE = tmp.indexOf("}");
- int indexT = tmp.indexOf("text-size:");
- if ((indexT > -1) && (indexBB >-1) && (indexBE > -1) && (indexT>indexBB) && (indexT < indexBE)) {
- String bef = tmp.substring(0, indexT+10);
- String textSize = tmp.substring(indexT+10);
- int indexVirg = textSize.indexOf(";");
- if (indexVirg > -1) {
- String textValue = textSize.substring(0, indexVirg);
- String endf = textSize.substring(indexVirg);
- int val = Integer.decode(textValue);
- val += modifier;
- if (val < 1) {
- val = 1;
+ }
+
+ public String modifyTextSize(int modifier, String input, String key) {
+ String ret = input;
+ int indexD = input.indexOf(key);
+ if (indexD != -1) {
+ String before = input.substring(0, indexD);
+
+ String tmp = input.substring(indexD);
+ int indexBB = tmp.indexOf("{");
+ int indexBE = tmp.indexOf("}");
+ int indexT = tmp.indexOf("text-size:");
+ if ((indexT > -1) && (indexBB > -1) && (indexBE > -1) && (indexT > indexBB) && (indexT < indexBE)) {
+ String bef = tmp.substring(0, indexT + 10);
+ String textSize = tmp.substring(indexT + 10);
+ int indexVirg = textSize.indexOf(";");
+ if (indexVirg > -1) {
+ String textValue = textSize.substring(0, indexVirg);
+ String endf = textSize.substring(indexVirg);
+ int val = Integer.decode(textValue);
+ val += modifier;
+ if (val < 1) {
+ val = 1;
+ }
+ //TraceManager.addDev("Value=" + val);
+ // Rebuild the string
+ ret = before + bef + val + endf;
}
- //TraceManager.addDev("Value=" + val);
- // Rebuild the string
- ret = before + bef + val + endf;
}
- }
+ }
+ return ret;
}
- return ret;
- }
- public void screenshot() {
- TraceManager.addDev("Screenshot");
- JFileChooser jfcggraph;
- if (SpecConfigTTool.GGraphPath.length() > 0) {
- jfcggraph = new JFileChooser(SpecConfigTTool.GGraphPath);
- } else {
- jfcggraph = new JFileChooser();
- }
- PNGFilter filter = new PNGFilter();
- jfcggraph.setFileFilter(filter);
- int returnVal = jfcggraph.showDialog(this, "Graph capture (in png)");
- if (returnVal != JFileChooser.APPROVE_OPTION) {
- return;
- }
- File pngFile = jfcggraph.getSelectedFile();
- TraceManager.addDev("Making the screenshot in " + pngFile.getAbsolutePath());
+ public void screenshot() {
+ TraceManager.addDev("Screenshot");
+ JFileChooser jfcggraph;
+ if (SpecConfigTTool.GGraphPath.length() > 0) {
+ jfcggraph = new JFileChooser(SpecConfigTTool.GGraphPath);
+ } else {
+ jfcggraph = new JFileChooser();
+ }
+ PNGFilter filter = new PNGFilter();
+ jfcggraph.setFileFilter(filter);
+ int returnVal = jfcggraph.showDialog(this, "Graph capture (in png)");
+ if (returnVal != JFileChooser.APPROVE_OPTION) {
+ return;
+ }
+ File pngFile = jfcggraph.getSelectedFile();
+ TraceManager.addDev("Making the screenshot in " + pngFile.getAbsolutePath());
- takeScreenshot(dv, pngFile);
+ takeScreenshot(dv, pngFile);
- TraceManager.addDev("Screenshot performed");
- }
+ TraceManager.addDev("Screenshot performed");
+ }
- public synchronized void manageInternalActions() {
- if (edges == null) {
- return;
- }
- int cpt = 0;
- for (AUTTransition transition : graph.getTransitions()) {
- if (transition.transition.startsWith("i(")) {
- if (internalActions.isSelected()) {
- edges.get(cpt).setAttribute("ui.label", transition.transition);
- } else {
- edges.get(cpt).setAttribute("ui.label", "");
+ public synchronized void manageInternalActions() {
+ if (edges == null) {
+ return;
+ }
+ int cpt = 0;
+ for (AUTTransition transition : graph.getTransitions()) {
+ if (transition.transition.startsWith("i(")) {
+ if (internalActions.isSelected()) {
+ edges.get(cpt).setAttribute("ui.label", transition.transition);
+ } else {
+ edges.get(cpt).setAttribute("ui.label", "");
+ }
}
+ cpt++;
}
- cpt++;
+ //dv.repaint();
}
- //dv.repaint();
- }
- public synchronized void manageReadActions() {
- if (edges == null) {
- return;
- }
- int cpt = 0;
- for (AUTTransition transition : graph.getTransitions()) {
- if (transition.transition.contains("?")) {
- if (readActions.isSelected()) {
- edges.get(cpt).setAttribute("ui.label", transition.transition);
- } else {
- edges.get(cpt).setAttribute("ui.label", "");
+ public synchronized void manageReadActions() {
+ if (edges == null) {
+ return;
+ }
+ int cpt = 0;
+ for (AUTTransition transition : graph.getTransitions()) {
+ if (transition.transition.contains("?")) {
+ if (readActions.isSelected()) {
+ edges.get(cpt).setAttribute("ui.label", transition.transition);
+ } else {
+ edges.get(cpt).setAttribute("ui.label", "");
+ }
}
+ cpt++;
}
- cpt++;
- }
- //dv.repaint();
- }
-
- public synchronized void manageHigherQuality() {
- //viewer.disableAutoLayout();
- if (higherQuality.isSelected()) {
- vGraph.setAttribute("ui.quality");
- } else {
- vGraph.removeAttribute("ui.quality");
- }
- try {
- //viewer.enableAutoLayout();
//dv.repaint();
- } catch (Exception e) {
}
- }
+ public synchronized void manageHigherQuality() {
+ //viewer.disableAutoLayout();
+ if (higherQuality.isSelected()) {
+ vGraph.setAttribute("ui.quality");
+ } else {
+ vGraph.removeAttribute("ui.quality");
+ }
+ try {
+ //viewer.enableAutoLayout();
+ //dv.repaint();
+ } catch (Exception e) {
+ }
+ }
- public synchronized void manageAntialiasing() {
- //viewer.disableAutoLayout();
- if (antialiasing.isSelected()) {
- vGraph.setAttribute("ui.antialias");
- } else {
- vGraph.removeAttribute("ui.antialias");
- }
- try {
- //viewer.enableAutoLayout();
- //dv.repaint();
- } catch (Exception e) {
+ public synchronized void manageAntialiasing() {
+ //viewer.disableAutoLayout();
+ if (antialiasing.isSelected()) {
+ vGraph.setAttribute("ui.antialias");
+ } else {
+ vGraph.removeAttribute("ui.antialias");
+ }
+ try {
+ //viewer.enableAutoLayout();
+ //dv.repaint();
+ } catch (Exception e) {
+ }
}
- }
- public synchronized void updateMe() {
- //TraceManager.addDev("updateMe");
- dv.repaint();
- }
+ public synchronized void updateMe() {
+ //TraceManager.addDev("updateMe");
+ dv.repaint();
+ }
- public Node findNodeAt(int x, int y) {
- for( int i=0; i<vGraph.getNodeCount(); i++) {
- TraceManager.addDev("index:" + i);
- Node node = vGraph.getNode(i);
- if (node != null) {
- double pos[] = Toolkit.nodePosition(node);
- if (pos != null) {
- //TraceManager.addDev("pos of Node " + node.getId() + " is " + pos[0] + "," + pos[1]);
- Point3 position = dv.getCamera().transformGuToPx(pos[0], pos[1], 0);
- TraceManager.addDev("Coordinate = " + position + " vs mouse : " + x + "," + y);
- double diffX = 1;
- double diffY = 1;
- if (transform != null) {
- diffX = transform.getScaleX();
- diffY = transform.getScaleY();
- }
- if ((Math.abs(position.x - diffX*x) < 10) && (Math.abs(position.y - diffY*y) < 10)) {
- return node;
+ public Node findNodeAt(int x, int y) {
+ for (int i = 0; i < vGraph.getNodeCount(); i++) {
+ //TraceManager.addDev("index:" + i);
+ Node node = vGraph.getNode(i);
+ if (node != null) {
+ double pos[] = Toolkit.nodePosition(node);
+ if (pos != null) {
+ //TraceManager.addDev("pos of Node " + node.getId() + " is " + pos[0] + "," + pos[1]);
+ Point3 position = dv.getCamera().transformGuToPx(pos[0], pos[1], 0);
+ //TraceManager.addDev("Coordinate = " + position + " vs mouse : " + x + "," + y);
+ double diffX = 1;
+ double diffY = 1;
+ if (transform != null) {
+ diffX = transform.getScaleX();
+ diffY = transform.getScaleY();
+ }
+ if ((Math.abs(position.x - diffX * x) < 10) && (Math.abs(position.y - diffY * y) < 10)) {
+ return node;
+ }
+ } else {
+ TraceManager.addDev("Null pos");
}
- } else {
- TraceManager.addDev("Null pos");
}
}
- }
- return null;
- }
+ return null;
+ }
/*public void setAutoLayout(boolean auto) {
autoLayout.setSelected(auto);
}*/
-
-
-} // Basic Frame
+ } // Basic Frame
} // Main class
diff --git a/src/main/java/ui/tree/JDiagramTree.java b/src/main/java/ui/tree/JDiagramTree.java
index a883fb59c6ef48cdd6d5da3a0135a6c56e552c62..9a61df4165c6b899ea55c2fb6e65ac083b442eec 100755
--- a/src/main/java/ui/tree/JDiagramTree.java
+++ b/src/main/java/ui/tree/JDiagramTree.java
@@ -519,7 +519,7 @@ public class JDiagramTree extends javax.swing.JTree implements ActionListener, M
} else if (ae.getSource() == jmiShow) {
if (selectedRG.graph != null) {
- selectedRG.graph.display();
+ selectedRG.graph.display(!MainGUI.experimentalOn);
} else {
mgui.displayAUTFromRG(selectedRG.name, selectedRG);
}
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 26ef37d52c4153fc44bcd6d978765815e6fdb897..d1d0b289843c9da2ab45acb4d5bef5561bb98106 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -770,7 +770,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
if (graphAUT != null) {
AUTGraph rg = new AUTGraph();
rg.buildGraph(graphAUT);
- rg.display();
+ rg.display(!MainGUI.experimentalOn);
}
}
diff --git a/src/main/java/ui/window/JFrameStatistics.java b/src/main/java/ui/window/JFrameStatistics.java
index 9d6724be8f51b1f03e6d655563f0ba2d578f0312..95e7027ae029a673a98436129836480185207da9 100644
--- a/src/main/java/ui/window/JFrameStatistics.java
+++ b/src/main/java/ui/window/JFrameStatistics.java
@@ -45,6 +45,7 @@ import automata.Transition;
import common.SpecConfigTTool;
import graph.AUTGraph;
import myutil.*;
+import ui.MainGUI;
import ui.StoppableGUIElement;
import ui.ThreadGUIElement;
import ui.file.AUTFileFilter;
@@ -569,12 +570,12 @@ public class JFrameStatistics extends JFrame implements ActionListener, Stoppabl
} else if (evt.getSource() == savePathL) {
saveAutomata(lastLongestAutomata);
} else if (evt.getSource() == showGraph) {
- graph.display();
+ graph.display(!MainGUI.experimentalOn);
}
}
public void displayGraph() {
- graph.display();
+ graph.display(!MainGUI.experimentalOn);
}
private void saveAutomata(Automata aut) {