Repository: workcraft/workcraft
Issue: Concurrent modification exception on import from Verilog

To reproduce synthesise a relatively complex STG (e.g. VME bus controller). When the resultant Verilog is imported sometimes (not always) the drawing thread tries to access those components that are still being imported. This results in concurrent modification of some collections of nodes.


Changed files:
SonPlugin/src/org/workcraft/plugins/son/exception/TimeEstimationValueException.java
SonPlugin/src/org/workcraft/plugins/son/util/EstimatedInterval.java
WorkcraftCore/src/org/workcraft/dom/visual/DrawMan.java
SonPlugin/src/org/workcraft/plugins/son/tools/SONSimulationTool.java
SonPlugin/src/org/workcraft/plugins/son/test/Dijkstra.java

diff --git a/SonPlugin/src/org/workcraft/plugins/son/exception/TimeEstimationValueException.java b/SonPlugin/src/org/workcraft/plugins/son/exception/TimeEstimationValueException.java
deleted file mode 100644
index ccc130f94..000000000
--- a/SonPlugin/src/org/workcraft/plugins/son/exception/TimeEstimationValueException.java
+++ /dev/null
@@ -1,11 +0,0 @@
-package org.workcraft.plugins.son.exception;
-
-public class TimeEstimationValueException extends Exception {
-
-    private static final long serialVersionUID = 1L;
-
-    public TimeEstimationValueException(String msg) {
-        super(msg);
-    }
-
-}
diff --git a/SonPlugin/src/org/workcraft/plugins/son/test/Dijkstra.java b/SonPlugin/src/org/workcraft/plugins/son/test/Dijkstra.java
deleted file mode 100644
index fb0a0d252..000000000
--- a/SonPlugin/src/org/workcraft/plugins/son/test/Dijkstra.java
+++ /dev/null
@@ -1,146 +0,0 @@
-package org.workcraft.plugins.son.test;
-
-import java.io.*;
-import java.util.*;
-
-public class Dijkstra {
-    private static final Graph.Edge[] GRAPH = {
-        new Graph.Edge("a", "b", 7),
-        new Graph.Edge("a", "c", 9),
-        new Graph.Edge("a", "f", 14),
-        new Graph.Edge("b", "c", 10),
-        new Graph.Edge("b", "d", 15),
-        new Graph.Edge("c", "d", 11),
-        new Graph.Edge("c", "f", 2),
-        new Graph.Edge("d", "e", 1),
-        new Graph.Edge("f", "e", 1),
-    };
-    private static final String START = "a";
-    private static final String END = "e";
-
-    public static void main(String[] args) {
-        Graph g = new Graph(GRAPH);
-        g.dijkstra(START);
-        g.printPath(END);
-        g.printAllPaths();
-    }
-
-    private static class Graph {
-        private final Map<String, Vertex> graph; // mapping of vertex names to Vertex objects, built from a set of Edges
-
-        /** One edge of the graph (only used by Graph constructor) */
-        public static class Edge {
-            public final String v1, v2;
-            public final int dist;
-            Edge(String v1, String v2, int dist) {
-                this.v1 = v1;
-                this.v2 = v2;
-                this.dist = dist;
-            }
-        }
-
-        /** One vertex of the graph, complete with mappings to neighbouring vertices */
-        public static class Vertex implements Comparable<Vertex> {
-            public final String name;
-            public int dist = Integer.MAX_VALUE; // MAX_VALUE assumed to be infinity
-            public Vertex previous = null;
-            public final Map<Vertex, Integer> neighbours = new HashMap<>();
-
-            Vertex(String name) {
-                this.name = name;
-            }
-
-            private void printPath() {
-                if (this == this.previous) {
-                    System.out.printf("%s", this.name);
-                } else if (this.previous == null) {
-                    System.out.printf("%s(unreached)", this.name);
-                } else {
-                    this.previous.printPath();
-                    System.out.printf(" -> %s(%d)", this.name, this.dist);
-                }
-            }
-
-            public int compareTo(Vertex other) {
-                return Integer.compare(dist, other.dist);
-            }
-        }
-
-        /** Builds a graph from a set of edges */
-        Graph(Edge[] edges) {
-            graph = new HashMap<>(edges.length);
-
-            //one pass to find all vertices
-            for (Edge e : edges) {
-                if (!graph.containsKey(e.v1)) graph.put(e.v1, new Vertex(e.v1));
-                if (!graph.containsKey(e.v2)) graph.put(e.v2, new Vertex(e.v2));
-            }
-
-            //another pass to set neighbouring vertices
-            for (Edge e : edges) {
-                graph.get(e.v1).neighbours.put(graph.get(e.v2), e.dist);
-                graph.get(e.v2).neighbours.put(graph.get(e.v1), e.dist); // also do this for an undirected graph
-            }
-        }
-
-        /** Runs dijkstra using a specified source vertex */
-        public void dijkstra(String startName) {
-            if (!graph.containsKey(startName)) {
-                System.err.printf("Graph doesn't contain start vertex \\"%s\\"\\n", startName);
-                return;
-            }
-            final Vertex source = graph.get(startName);
-            NavigableSet<Vertex> q = new TreeSet<>();
-
-            // set-up vertices
-            for (Vertex v : graph.values()) {
-                v.previous = v == source ? source : null;
-                v.dist = v == source ? 0 : Integer.MAX_VALUE;
-                q.add(v);
-            }
-            dijkstra(q);
-        }
-
-        /** Implementation of dijkstra's algorithm using a binary heap. */
-        private void dijkstra(final NavigableSet<Vertex> q) {
-            Vertex u, v;
-
-            while (!q.isEmpty()) {
-
-                u = q.pollFirst(); // vertex with shortest distance (first iteration will return source)
-                if (u.dist == Integer.MAX_VALUE) break; // we can ignore u (and any other remaining vertices) since they are unreachable
-
-                //look at distances to each neighbour
-                for (Map.Entry<Vertex, Integer> a : u.neighbours.entrySet()) {
-                    v = a.getKey(); //the neighbour in this iteration
-
-                    final int alternateDist = u.dist + a.getValue();
-                    if (alternateDist < v.dist) { // shorter path to neighbour found
-                        q.remove(v);
-                        v.dist = alternateDist;
-                        v.previous = u;
-                        q.add(v);
-                    }
-                }
-            }
-        }
-
-        /** Prints a path from the source to the specified vertex */
-        public void printPath(String endName) {
-            if (!graph.containsKey(endName)) {
-                System.err.printf("Graph doesn't contain end vertex \\"%s\\"\\n", endName);
-                return;
-            }
-
-            graph.get(endName).printPath();
-            System.out.println();
-        }
-        /** Prints the path from the source to every vertex (output order is not guaranteed) */
-        public void printAllPaths() {
-            for (Vertex v : graph.values()) {
-                v.printPath();
-                System.out.println();
-            }
-        }
-    }
-}
diff --git a/SonPlugin/src/org/workcraft/plugins/son/tools/SONSimulationTool.java b/SonPlugin/src/org/workcraft/plugins/son/tools/SONSimulationTool.java
index c811513a8..f7e5ce41d 100644
--- a/SonPlugin/src/org/workcraft/plugins/son/tools/SONSimulationTool.java
+++ b/SonPlugin/src/org/workcraft/plugins/son/tools/SONSimulationTool.java
@@ -398,8 +398,7 @@ public class SONSimulationTool extends AbstractTool implements ClipboardOwner {
         }
         updateState(editor);
         editor.requestFocus();
-        editor.forceRedraw();
-        editor.getModel().setTemplateNode(null);
+        super.activated(editor);
     }
 
     protected void initialise() {
@@ -421,8 +420,13 @@ public class SONSimulationTool extends AbstractTool implements ClipboardOwner {
     }
 
     @Override
-    public void deactivated(GraphEditor editor) {
+    public void deactivated(final GraphEditor editor) {
         super.deactivated(editor);
+        if (timer != null) {
+            timer.stop();
+            timer = null;
+        }
+        editor.getWorkspaceEntry().cancelMemento();
         mainTrace.clear();
         branchTrace.clear();
         isRev = false;
diff --git a/SonPlugin/src/org/workcraft/plugins/son/util/EstimatedInterval.java b/SonPlugin/src/org/workcraft/plugins/son/util/EstimatedInterval.java
deleted file mode 100644
index 82bd5e45c..000000000
--- a/SonPlugin/src/org/workcraft/plugins/son/util/EstimatedInterval.java
+++ /dev/null
@@ -1,15 +0,0 @@
-package org.workcraft.plugins.son.util;
-
-public class EstimatedInterval extends Interval {
-
-    public EstimatedInterval() {
-        super();
-        // TODO Auto-generated constructor stub
-    }
-
-    public EstimatedInterval(Integer start, Integer end) {
-        super(start, end);
-        // TODO Auto-generated constructor stub
-    }
-
-}
diff --git a/WorkcraftCore/src/org/workcraft/dom/visual/DrawMan.java b/WorkcraftCore/src/org/workcraft/dom/visual/DrawMan.java
index 02707544a..19d4fd178 100644
--- a/WorkcraftCore/src/org/workcraft/dom/visual/DrawMan.java
+++ b/WorkcraftCore/src/org/workcraft/dom/visual/DrawMan.java
@@ -23,6 +23,7 @@ package org.workcraft.dom.visual;
 
 import java.awt.Graphics2D;
 import java.awt.geom.AffineTransform;
+import java.util.ArrayList;
 
 import org.workcraft.dom.Node;
 import org.workcraft.dom.visual.connections.VisualConnection;
@@ -105,14 +106,16 @@ final class DrawMan {
         boolean isCollapsed = (node instanceof Collapsible) && ((Collapsible) node).getIsCollapsed();
         boolean isInsideCollapsed = isCollapsed && ((Collapsible) node).isCurrentLevelInside();
         if (isInsideCollapsed || !isCollapsed) {
+            // Copy the collection of children nodes before drawing in order to avoid concurrent modification exception
+            ArrayList<Node> children = new ArrayList<>(node.getChildren());
             // First draw nodes
-            for (Node childNode : node.getChildren()) {
+            for (Node childNode : children) {
                 if (!(childNode instanceof VisualConnection)) {
                     draw(decoration, childNode);
                 }
             }
             // Then draw connections
-            for (Node childNode : node.getChildren()) {
+            for (Node childNode : children) {
                 if (childNode instanceof VisualConnection) {
                     draw(decoration, childNode);
                 }