diff --git a/build.txt b/build.txt
index e1101ae6ec8ccf1349020b21ab0b1ad6dca67315..4b0ce1b9bca6ea3f75b3586be44aa7cdef648f42 100644
--- a/build.txt
+++ b/build.txt
@@ -1 +1 @@
-13563
\ No newline at end of file
+13571
\ No newline at end of file
diff --git a/src/main/java/graph/AUTGraphDisplay.java b/src/main/java/graph/AUTGraphDisplay.java
index b3fb3a293bdb9ee381ad9144154e88cc2dcab3c1..3fabea16d6ccbd80b4e125b99cf380bccd1cb9c1 100755
--- a/src/main/java/graph/AUTGraphDisplay.java
+++ b/src/main/java/graph/AUTGraphDisplay.java
@@ -54,6 +54,7 @@ import org.graphstream.ui.swing_viewer.ViewPanel;
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 ui.file.PNGFilter;
import ui.util.IconManager;
@@ -87,14 +88,17 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
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 static String STYLE_SHEET = "node {fill-color: #B1CAF1; text-color: black; size: 11px, 11px;} node.init " +
- "{fill-color:green; text-color: black; size: 15px, 15px;} node.deadlock {fill-color: red; text-color: white; size: 15px," +
- "15px;} edge {text-color: blue; shape: cubic-curve;} edge.defaultedge {text-color: blue; shape: cubic-curve;} edge.external " +
- "{text-color: red; text-style: bold} ";
+ 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: red; text-color: white; size: 20px, 20px; text-size:16;} " +
+ "node.init { fill-color: green; text-color: black; size: 20px, 20px; text-size:16;}";
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; " +
@@ -143,13 +147,13 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
System.setProperty("org.graphstream.ui.renderer", "org.graphstream.ui.j2dviewer.J2DGraphRenderer");
vGraph = new MultiGraph("TTool graph");
- /*if ((ConfigurationTTool.RGStyleSheet != null) && (ConfigurationTTool.RGStyleSheet.trim().length() > 0)) {
+ if ((ConfigurationTTool.RGStyleSheet != null) && (ConfigurationTTool.RGStyleSheet.trim().length() > 0)) {
TraceManager.addDev("Adding stylesheet:" + ConfigurationTTool.RGStyleSheet + "\n\nvs default:" + STYLE_SHEET);
- vGraph.addAttribute("ui.stylesheet", ConfigurationTTool.RGStyleSheet);
+ vGraph.setAttribute("ui.stylesheet", ConfigurationTTool.RGStyleSheet);
} else {
- vGraph.addAttribute("ui.stylesheet", STYLE_SHEET);
- }*/
- vGraph.setAttribute("ui.stylesheet", STYLE_SHEET);
+ vGraph.setAttribute("ui.stylesheet", STYLE_SHEET);
+ }
+ //vGraph.setAttribute("ui.stylesheet", STYLE_SHEET);
//vGraph.addAttribute("layout.weight", 0.5);
@@ -181,12 +185,12 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
//edge.addAttribute("ui.class", "edge");
//edge.addAttribute("shape", "cubic-curve");
//edge.addAttribute("arrow-shape", "circle");
- //edge.addAttribute("layout.weight", 0.4);
- /*if (!(transition.transition.startsWith("i("))) {
- edge.addAttribute("ui.class", "external");
+ edge.setAttribute("layout.weight", 0.4);
+ if (!(transition.transition.startsWith("i("))) {
+ edge.setAttribute("ui.class", "external");
} else {
- edge.addAttribute("ui.class", "defaultedge");
- }*/
+ edge.setAttribute("ui.class", "defaultedge");
+ }
edges.add(edge);
cpt++;
}
@@ -199,8 +203,7 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
//View vi = viewer.addDefaultView(true);
viewer.setCloseFramePolicy(Viewer.CloseFramePolicy.CLOSE_VIEWER);
- BasicFrame bf = new BasicFrame(this, viewer, vGraph, graph, edges, exitOnClose);
-
+ bf = new BasicFrame(this, viewer, vGraph, graph, edges, exitOnClose);
//vi.addMouseListener(this);
@@ -211,11 +214,20 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
}
+ public void sleep(int time) {
+ try {
+ Thread.sleep(time);
+ } catch (InterruptedException e) {
+ e.printStackTrace();
+ }
+ }
+
public void run() {
- ViewerPipe fromViewer = viewer.newViewerPipe();
+ /*ViewerPipe fromViewer = viewer.newViewerPipe();
fromViewer.addViewerListener(this);
- fromViewer.addSink(vGraph);
+ fromViewer.addSink(vGraph);*/
+
// Then we need a loop to do our work and to wait for events.
// In this loop we will need to call the
@@ -224,8 +236,34 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
// our thread
int cpt = 0;
- //TraceManager.addDev("Starting loop:" + cpt);
+ ViewerPipe pipeIn = viewer.newViewerPipe();
+ pipeIn.addSink(vGraph);
+ pipeIn.addViewerListener(this);
+
+
+
while (loop) {
+ try {
+ pipeIn.blockingPump(50);
+ } catch (Exception e) {
+
+ }
+
+
+ if (vGraph.hasAttribute("ui.viewClosed")) {
+ //TraceManager.addDev("View was closed");
+ loop = false;
+ if (exitOnClose) {
+ System.exit(1);
+ }
+ }
+
+ bf.updateMe();
+ }
+
+
+ //TraceManager.addDev("Starting loop:" + cpt);
+ /*while (loop) {
try {
//TraceManager.addDev("beg of loop:" + cpt);
fromViewer.blockingPump(); // or fromViewer.blockingPump(); in the nightly builds
@@ -233,27 +271,22 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
}
if (vGraph.hasAttribute("ui.viewClosed")) {
- TraceManager.addDev("View was closed");
+ //TraceManager.addDev("View was closed");
loop = false;
if (exitOnClose) {
System.exit(1);
}
- } /*else if (firstNode.hasAttribute("ui.clicked")) {
- TraceManager.addDev("Init node was clicked");
- firstNode.removeAttribute("ui.clicked");
- }*/
-
- // here your simulation code.
- //TraceManager.addDev("End of loop" + cpt);
- //cpt ++;
-
- // You do not necessarily need to use a loop, this is only an example.
- // as long as you call pump() before using the graph. pump() is non
- // blocking. If you only use the loop to look at event, use blockingPump()
- // to avoid 100% CPU usage. The blockingPump() method is only available from
- // the nightly builds.
- }
- //viewPipe = null;
+ } */
+
+ // here your simulation code.
+ //TraceManager.addDev("End of loop" + cpt);
+ //cpt ++;
+
+ // You do not necessarily need to use a loop, this is only an example.
+ // as long as you call pump() before using the graph. pump() is non
+ // blocking. If you only use the loop to look at event, use blockingPump()
+ // to avoid 100% CPU usage. The blockingPump() method is only available from
+ // the nightly builds.
}
@@ -266,7 +299,7 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
}
public void viewClosed(String id) {
- TraceManager.addDev("View closed and closed !");
+ //TraceManager.addDev("View closed and closed !");
loop = false;
if (viewer != null) {
viewer.close();
@@ -311,232 +344,234 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
}
- public void mouseOver(java.lang.String id){}
-
-
-
- public void mouseLeft(java.lang.String id){}
+ public void mouseOver(java.lang.String id) {
+ TraceManager.addDev("Mouse over: " + id);
+ }
+ public void mouseLeft(java.lang.String id) {
+ TraceManager.addDev("Mouse over: " + id);
+ }
+class InitializeApplication extends JFrame implements Runnable {
+ private static final long serialVersionUID = -804177406404724792L;
+ protected MultiGraph vGraph;
+ protected SwingViewer viewer;
+ protected AUTGraph graph;
+ protected Node firstNode;
- class InitializeApplication extends JFrame implements Runnable {
- private static final long serialVersionUID = -804177406404724792L;
- protected MultiGraph vGraph;
- protected SwingViewer viewer;
- protected AUTGraph graph;
- protected Node firstNode;
+ public InitializeApplication(SwingViewer viewer, MultiGraph vGraph, AUTGraph autgraph) {
+ this.viewer = viewer;
+ this.vGraph = vGraph;
+ this.graph = autgraph;
+ }
- public InitializeApplication(SwingViewer viewer, MultiGraph vGraph, AUTGraph autgraph) {
- this.viewer = viewer;
- this.vGraph = vGraph;
- this.graph = autgraph;
+ public void run() {
+ int cpt = 0;
+ Node node;
+ Edge edge;
+ for (AUTState state : graph.getStates()) {
+ node = vGraph.addNode("" + state.id);
+ node.setAttribute("ui.label", "" + state.id);
+ if (state.getNbOutTransitions() == 0) {
+ node.setAttribute("ui.class", "deadlock");
+ }
+ if (cpt == 0) {
+ node.setAttribute("ui.class", "init");
+ firstNode = node;
+ }
+ cpt++;
}
+ cpt = 0;
+ // We must merge the transitions with the same starting and ending state
+ HashSet<AUTTransition> transitionsMet = new HashSet<>();
+ for (AUTTransition transition : graph.getTransitions()) {
+ edge = vGraph.addEdge("" + cpt, "" + transition.origin, "" + transition.destination, true);
- public void run() {
- int cpt = 0;
- Node node;
- Edge edge;
- for (AUTState state : graph.getStates()) {
- node = vGraph.addNode("" + state.id);
- node.setAttribute("ui.label", "" + state.id);
- if (state.getNbOutTransitions() == 0) {
- node.setAttribute("ui.class", "deadlock");
- }
- if (cpt == 0) {
- node.setAttribute("ui.class", "init");
- firstNode = node;
- }
- cpt++;
- }
- cpt = 0;
- // We must merge the transitions with the same starting and ending state
- HashSet<AUTTransition> transitionsMet = new HashSet<>();
- for (AUTTransition transition : graph.getTransitions()) {
- edge = vGraph.addEdge("" + cpt, "" + transition.origin, "" + transition.destination, true);
-
- transitionsMet.add(transition);
- edge = vGraph.addEdge("" + cpt, "" + transition.origin, "" + transition.destination, true);
+ transitionsMet.add(transition);
+ edge = vGraph.addEdge("" + cpt, "" + transition.origin, "" + transition.destination, true);
/*TraceManager.addDev("Transition=" + transition.transition);
String tmp = Conversion.replaceAllChar(transition.transition, '(', "$");
tmp = Conversion.replaceAllChar(tmp, ')', "$");
TraceManager.addDev("Transition=" + tmp);*/
- edge.setAttribute("ui.label", transition.transition);
- edge.setAttribute("ui.class", "classic");
- if (!(transition.transition.startsWith("i("))) {
- edge.setAttribute("ui.class", "external");
- }
- cpt++;
-
+ edge.setAttribute("ui.label", transition.transition);
+ edge.setAttribute("ui.class", "classic");
+ if (!(transition.transition.startsWith("i("))) {
+ edge.setAttribute("ui.class", "external");
}
+ cpt++;
- viewer.enableAutoLayout();
- DefaultView dv = new DefaultView(viewer, "Graph", new SwingGraphRenderer());
- //ViewPanel vp = viewer.addDefaultView(true, new SwingGraphRenderer());
- add(dv, BorderLayout.CENTER);
- setDefaultCloseOperation(EXIT_ON_CLOSE);
- setSize(800, 600);
- setVisible(true);
}
+ viewer.enableAutoLayout();
+ DefaultView dv = new DefaultView(viewer, "Graph", new SwingGraphRenderer());
+ //ViewPanel vp = viewer.addDefaultView(true, new SwingGraphRenderer());
+ add(dv, BorderLayout.CENTER);
+ setDefaultCloseOperation(EXIT_ON_CLOSE);
+ setSize(800, 600);
+ setVisible(true);
}
- class BasicFrame extends JFrame implements ActionListener {
- protected MultiGraph vGraph;
- protected SwingViewer viewer;
- protected JPanel viewerPanel;
- protected AUTGraph graph;
- protected ArrayList<Edge> edges;
-
- protected JButton close;
- protected JButton screenshot;
- protected JCheckBox internalActions;
- protected JCheckBox readActions;
- protected JCheckBox higherQuality, antialiasing;
- protected JLabel help, info;
-
- protected boolean exitOnClose;
-
- private AUTGraphDisplay autD;
-
-
- 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);
- }
+}
- }
+class BasicFrame extends JFrame implements ActionListener {
+ protected MultiGraph vGraph;
+ protected SwingViewer viewer;
+ protected JPanel viewerPanel;
+ protected AUTGraph graph;
+ protected ArrayList<Edge> edges;
- public void makeComponents() {
- DefaultView dv = new DefaultView(viewer, "Graph", new SwingGraphRenderer());
- //viewerPanel = viewer.addDefaultView(false);
- 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);
- close.addActionListener(this);
- help = new JLabel("Zoom with PageUp/PageDown, move with cursor keys");
- 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);
-
- 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);
- }
+ protected JButton close;
+ protected JButton screenshot;
+ protected JCheckBox internalActions;
+ protected JCheckBox readActions;
+ protected JCheckBox higherQuality, antialiasing;
+ protected JLabel help, info;
- 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();
- }
+ protected boolean exitOnClose;
+
+ private AUTGraphDisplay autD;
+
+ private DefaultView dv;
+
+
+ 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);
}
- public void closeFrame() {
- if (autD != null) {
- autD.viewClosed("closed pushed");
- }
- if (exitOnClose) {
- System.exit(1);
- }
- dispose();
+ }
+
+ public void makeComponents() {
+ dv = new DefaultView(viewer, "Graph", new SwingGraphRenderer());
+ //viewerPanel = viewer.addDefaultView(false);
+ 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);
+ close.addActionListener(this);
+ help = new JLabel("Zoom with PageUp/PageDown, move with cursor keys");
+ 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);
+
+ 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();
}
+ }
- 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(..)
+ public void closeFrame() {
+ if (autD != null) {
+ autD.viewClosed("closed pushed");
+ }
+ if (exitOnClose) {
+ System.exit(1);
+ }
+ dispose();
+ }
- 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 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());
- //vGraph.addAttribute("ui.screenshot", pngFile.getAbsolutePath());
- //vGraph.addAttribute("ui.screenshot", "/homes/apvrille/tmp/toto.png");
- takeScreenshot(viewerPanel, pngFile);
+ //vGraph.addAttribute("ui.screenshot", pngFile.getAbsolutePath());
+ //vGraph.addAttribute("ui.screenshot", "/homes/apvrille/tmp/toto.png");
+
+ takeScreenshot(dv, pngFile);
/*FileSinkImages pic = new FileSinkImages(OutputType.PNG, Resolutions.UXGA);
//pic.setQuality();
@@ -548,73 +583,90 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable
TraceManager.addDev("Capture could not be performed: " + e.getMessage());
}*/
- //vGraph.addAttribute("ui.screenshot", "/tmp/toto.png");
- TraceManager.addDev("Screenshot performed");
- }
+ //vGraph.addAttribute("ui.screenshot", "/tmp/toto.png");
+ TraceManager.addDev("Screenshot performed");
+ }
- public 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();
+ }
- public 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 void manageHigherQuality() {
- viewer.disableAutoLayout();
- if (higherQuality.isSelected()) {
- vGraph.setAttribute("ui.quality");
- } else {
- vGraph.removeAttribute("ui.quality");
- }
- try {
- viewer.enableAutoLayout();
- } 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 void manageAntialiasing() {
- viewer.disableAutoLayout();
- if (antialiasing.isSelected()) {
- vGraph.setAttribute("ui.antialias");
- } else {
- vGraph.removeAttribute("ui.antialias");
- }
- try {
- viewer.enableAutoLayout();
- } catch (Exception e) {
- }
+
+ /*public void updateCameraView() {
+ Camera camera = controller.getPanel().getCamera();
+ cameraAutoFitView.setSelected(autoFit);
+ viewCenterX.setText(camera.getViewCenter().x+"");
+ viewCenterY.setText(camera.getViewCenter().y+"");
+ scale.setText(camera.getViewPercent()+"");
+ }*/
+
+ 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() {
+ dv.repaint();
+ }
- } // Basic Frame
+} // Basic Frame
} // Main class
diff --git a/src/main/java/ui/avatarsmd/AvatarSMDTransitionInfo.java b/src/main/java/ui/avatarsmd/AvatarSMDTransitionInfo.java
index a05ec28bdb1335602028fbc1241e3ea8d348816b..104c04233841f29126eb774dd8ce18a96671d7fa 100755
--- a/src/main/java/ui/avatarsmd/AvatarSMDTransitionInfo.java
+++ b/src/main/java/ui/avatarsmd/AvatarSMDTransitionInfo.java
@@ -530,6 +530,11 @@ public class AvatarSMDTransitionInfo extends TGCWithoutInternalComponent impleme
//TraceManager.addDev("Max delay:" + jdat.getAfterMax().trim());
afterDelay.getMinExpression().setText( jdat.getAfterMin().trim() );
afterDelay.getMaxExpression().setText( jdat.getAfterMax().trim() );
+
+ computeDelay.getMinExpression().setText( "");
+ computeDelay.getMaxExpression().setText( "" );
+
+
String retExtra = jdat.getExtraDelay1().trim();
try {
double extra1 = Double.parseDouble(retExtra);
diff --git a/src/main/java/ui/util/DefaultText.java b/src/main/java/ui/util/DefaultText.java
index 93d350cab7df6a8e1ffe9b8e4e833b3ddc47937b..3e1030403ef472b75f5e0d65a2bfa406245fe976 100755
--- a/src/main/java/ui/util/DefaultText.java
+++ b/src/main/java/ui/util/DefaultText.java
@@ -50,8 +50,8 @@ package ui.util;
*/
public class DefaultText {
- public static String BUILD = "13562";
- public static String DATE = "2020/09/30 03:13:38 CET";
+ public static String BUILD = "13570";
+ public static String DATE = "2020/10/06 03:13:34 CET";
public static StringBuffer sbAbout = makeAbout();
diff --git a/src/main/resources/help/avatarsafetypragmas.html b/src/main/resources/help/avatarsafetypragmas.html
index d1a2d50ad64f23131d3b384e9634bb10afc579db..d768df8039ab5298886d4d3c056d072fa8f45023 100644
--- a/src/main/resources/help/avatarsafetypragmas.html
+++ b/src/main/resources/help/avatarsafetypragmas.html
@@ -41,7 +41,7 @@
</center>
<h2 id="e-properties-1">E<> properties</h2>
<center>
-<img src="file:../help/ctleall_small.png" />
+<img src="file:../help/ctleone_small.png" />
</center>
<h2 id="leads-to-properties">“Leads to†properties</h2>
<p>“p –> q†means that whenever p is encoutred in a state s, all paths starting from state s must have a state in which q is satisfied.</p>
diff --git a/src/main/resources/help/avatarsafetypragmas.md b/src/main/resources/help/avatarsafetypragmas.md
index 92819d24398b70f0276b0c26613c7c1e109c36ea..eb29a0360520e1c3f63a89575192bd585933c5a1 100644
--- a/src/main/resources/help/avatarsafetypragmas.md
+++ b/src/main/resources/help/avatarsafetypragmas.md
@@ -43,7 +43,7 @@ means that the attribute "x" of block "Block1" is always strictly positive.
## E<> properties
<center>
-
+
</center>