Resolved gh #806 and #809

.classpath

@@ -37,5 +37,16 @@
 			<attribute name="optional" value="true"/>
 		</attributes>
 	</classpathentry>
+	<classpathentry kind="lib" path="C:/Users/Rensink/.m2/repository/org/eclipse/jdt/org.eclipse.jdt.annotation/2.2.700/org.eclipse.jdt.annotation-2.2.700.jar" sourcepath="C:/Users/Rensink/.m2/repository/org/eclipse/jdt/org.eclipse.jdt.annotation/2.2.700/org.eclipse.jdt.annotation-2.2.700-sources.jar">
+		<attributes>
+			<attribute name="maven.pomderived" value="true"/>
+			<attribute name="module" value="true"/>
+			<attribute name="javadoc_location" value="jar:file:/C:/Users/Rensink/.m2/repository/org/eclipse/jdt/org.eclipse.jdt.annotation/2.2.700/org.eclipse.jdt.annotation-2.2.700-javadoc.jar!/"/>
+			<attribute name="maven.groupId" value="org.eclipse.jdt"/>
+			<attribute name="maven.artifactId" value="org.eclipse.jdt.annotation"/>
+			<attribute name="maven.version" value="2.2.700"/>
+			<attribute name="maven.scope" value="compile"/>
+		</attributes>
+	</classpathentry>
 	<classpathentry kind="output" path="target/classes"/>
 </classpath>

src/main/java/nl/utwente/groove/grammar/aspect/AspectEdge.java

@@ -39,8 +39,6 @@
 import static nl.utwente.groove.graph.GraphRole.TYPE;
 import static nl.utwente.groove.util.Factory.lazy;
 
-import java.util.Objects;
-
 import org.eclipse.jdt.annotation.NonNull;
 import org.eclipse.jdt.annotation.Nullable;
 
@@ -1035,18 +1033,16 @@ public Multiplicity getOutMult() {
 
     @Override
     protected int computeHashCode() {
-        return super.computeHashCode() + Objects.hashCode(getGraph());
+        return super.computeHashCode() + 31 * getGraph().externalHashCode();
     }
 
     @Override
     public boolean equals(@Nullable Object obj) {
-        boolean result = super.equals(obj);
-        if (!result) {
+        if (!super.equals(obj)) {
             return false;
         }
-        var other = (AspectEdge) obj;
-        assert other != null;
-        return getGraph() == other.getGraph();
+        assert obj != null;
+        return getGraph().externalEquals(((AspectEdge) obj).getGraph());
     }
 
     /** Separator between level name and edge label. */

src/main/java/nl/utwente/groove/grammar/aspect/AspectGraph.java

@@ -28,6 +28,7 @@
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
+import java.util.Objects;
 import java.util.SortedSet;
 import java.util.TreeSet;
 
@@ -639,6 +640,17 @@ int getEdgeNumber() {
 
     private final Dispenser edgeNumber;
 
+    /** Returns a hash code for this graph based on normal status, name and role. */
+    int externalHashCode() {
+        return Objects.hash(isNormal(), getRole(), getName());
+    }
+
+    /** Compares this graph to another one on the basis of normal status, name and role. */
+    boolean externalEquals(AspectGraph other) {
+        return isNormal() == other.isNormal() && getRole() == other.getRole()
+            && Objects.equals(getName(), other.getName());
+    }
+
     /**
      * Creates an aspect graph from a given (plain) graph.
      * @param graph the plain graph to convert
@@ -836,7 +848,8 @@ public AspectEdge createEdge(AspectNode source, Label label, AspectNode target)
             if (aLabel.has(AspectKind.REMARK)) {
                 nr = this.remarkCount.getNext();
             } else {
-                nr = this.graph.getEdgeNumber();
+                // non-remark edges are all numbered 0
+                // nr = this.graph.getEdgeNumber();
             }
             return new AspectEdge(source, (AspectLabel) label, target, nr);
         }

src/main/java/nl/utwente/groove/grammar/aspect/AspectNode.java

@@ -93,7 +93,7 @@ public AspectGraph getGraph() {
      */
     @Override
     protected int computeHashCode() {
-        return Objects.hash(getNumber(), getGraph().getClass(), getGraph().getName());
+        return super.computeHashCode() + 31 * getGraph().externalHashCode();
     }
 
     /**
@@ -111,8 +111,7 @@ public boolean equals(Object obj) {
         if (other.getNumber() != getNumber()) {
             return false;
         }
-        return Objects.equals(getGraph().getClass(), other.getGraph().getClass())
-            && Objects.equals(getGraph().getName(), other.getGraph().getName());
+        return getGraph().externalEquals(((AspectNode) obj).getGraph());
     }
 
     /**

src/main/java/nl/utwente/groove/grammar/model/GrammarModel.java

@@ -636,7 +636,16 @@ private void invalidate() {
     @Override
     public void propertyChange(PropertyChangeEvent evt) {
         SystemStore.Edit edit = (SystemStore.Edit) evt.getNewValue();
-        if (edit.getType() != EditType.LAYOUT) {
+        if (edit.getType() == EditType.LAYOUT) {
+            // replace the sources of the resource models
+            for (var kind : edit.getChange()) {
+                for (var name : getNames(kind)) {
+                    var graph = getStore().getGraphs(kind).get(name);
+                    assert graph != null;
+                    getGraphResource(kind, name).setSource(graph);
+                }
+            }
+        } else {
             syncResources(edit.getChange());
         }
     }

src/main/java/nl/utwente/groove/grammar/model/GraphBasedModel.java

@@ -66,7 +66,15 @@ public AspectGraph getSource() {
         return this.source;
     }
 
-    private final AspectGraph source;
+    /**
+     * Replaces the source with a new one, without rebuilding the model.
+     * This is <em>only</em> allowed if the layout changed, and nothing else!
+     */
+    void setSource(AspectGraph newSource) {
+        this.source = newSource;
+    }
+
+    private AspectGraph source;
 
     @Override
     public String getName() {

src/main/java/nl/utwente/groove/grammar/type/TypeEdge.java

@@ -47,8 +47,16 @@ public class TypeEdge extends AEdge<TypeNode,TypeLabel> implements TypeElement {
             .format("Can't create %s label %s between distinct nodes %s and %s",
                     label.getRole().getDescription(false), label, source, target);
         this.graph = graph;
+        this.key = new TypeEdgeKey(this);
     }
 
+    @Override
+    public TypeEdgeKey key() {
+        return this.key;
+    }
+
+    private final TypeEdgeKey key;
+
     @Override
     public boolean isSimple() {
         return true;

src/main/java/nl/utwente/groove/grammar/type/TypeEdgeKey.java

@@ -0,0 +1,36 @@
+/* GROOVE: GRaphs for Object Oriented VErification
+ * Copyright 2003--2023 University of Twente
+ *
+ * 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.
+ *
+ * $Id$
+ */
+package nl.utwente.groove.grammar.type;
+
+/**
+ * Distinguishing elements of a type edge, namely source node label, consisting of
+ * source node label, target node label and edge label
+ * @author Arend Rensink
+ * @version $Revision$
+ */
+public record TypeEdgeKey(TypeLabel sourceLabel, TypeLabel edgeLabel, TypeLabel targetLabel)
+    implements TypeKey {
+    /** Constructs a key from a given type edge by using its source, edge and target label. */
+    public TypeEdgeKey(TypeEdge edge) {
+        this(edge.source().label(), edge.label(), edge.target().label());
+    }
+
+    @Override
+    public TypeLabel label() {
+        return edgeLabel();
+    }
+}

src/main/java/nl/utwente/groove/grammar/type/TypeElement.java

@@ -36,7 +36,14 @@ public interface TypeElement extends Element, AnchorValue, Label {
      * Note that for type edges, the label does not completely determine
      * the edge, whereas for type nodes it does.
      */
-    public TypeLabel label();
+    default public TypeLabel label() {
+        return key().label();
+    }
+
+    /** Returns the type key for this type element, consisting of
+     * just the label information and not the type graph or sub- or supertypes.
+     */
+    public TypeKey key();
 
     /**
      * Returns the type graph to which this type element belongs.

src/main/java/nl/utwente/groove/grammar/type/TypeKey.java

@@ -0,0 +1,29 @@
+/* GROOVE: GRaphs for Object Oriented VErification
+ * Copyright 2003--2023 University of Twente
+ *
+ * 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.
+ *
+ * $Id$
+ */
+package nl.utwente.groove.grammar.type;
+
+/**
+ * Distinguishing elements from a {@link TypeElement}, consisting
+ * of (only) node and edge type labels, without taking type graph identity
+ * into account.
+ * @author Arend Rensink
+ * @version $Revision$
+ */
+public sealed interface TypeKey permits TypeEdgeKey, TypeNodeKey {
+    /** Returns the main label of this type key. */
+    TypeLabel label();
+}

src/main/java/nl/utwente/groove/grammar/type/TypeNode.java

@@ -21,6 +21,7 @@
 import java.awt.Color;
 import java.util.Set;
 
+import org.eclipse.jdt.annotation.NonNull;
 import org.eclipse.jdt.annotation.NonNullByDefault;
 import org.eclipse.jdt.annotation.Nullable;
 
@@ -52,8 +53,8 @@ public TypeNode(int nr, TypeLabel type, TypeGraph graph) {
         assert graph != null;
         assert type.getRole() == NODE_TYPE : String
             .format("Can't create type node for non-type label '%s'", type);
+        this.key = new TypeNodeKey(type);
         this.nr = nr;
-        this.type = type;
         this.graph = graph;
     }
 
@@ -133,12 +134,13 @@ public EdgeRole getRole() {
         return EdgeRole.NODE_TYPE;
     }
 
-    /** Returns the type of this node. */
     @Override
-    public TypeLabel label() {
-        return this.type;
+    public @NonNull TypeKey key() {
+        return this.key;
     }
 
+    private final TypeKey key;
+
     /** Indicates if this node type is abstract. */
     public final boolean isAbstract() {
         return this.abstracted;
@@ -151,7 +153,7 @@ public final void setAbstract() {
 
     /** Returns true if this node if of top type. */
     public final boolean isTopType() {
-        return this.type == TypeLabel.NODE;
+        return label() == TypeLabel.NODE;
     }
 
     /** Changes the importedness status of this node.
@@ -173,12 +175,12 @@ public final boolean isImported() {
 
     /** Indicates if this node type stands for a data type. */
     public final boolean isSort() {
-        return this.type.isSort();
+        return label().isSort();
     }
 
     /** Returns the data type of this node type, if any. */
     public final @Nullable Sort getSort() {
-        return this.type.getSort();
+        return label().getSort();
     }
 
     /** Returns the (possibly {@code null}) label pattern associated with this type node. */
@@ -248,6 +250,4 @@ public AnchorKind getAnchorKind() {
 
     /** Flag indicating if this node type is abstract. */
     private boolean abstracted;
-    /** The type of this node. */
-    private final TypeLabel type;
 }

src/main/java/nl/utwente/groove/grammar/type/TypeNodeKey.java

@@ -0,0 +1,30 @@
+/* GROOVE: GRaphs for Object Oriented VErification
+ * Copyright 2003--2023 University of Twente
+ *
+ * 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.
+ *
+ * $Id$
+ */
+package nl.utwente.groove.grammar.type;
+
+/**
+ * Distinguishing elements of a type edge, namely source node label, consisting of
+ * source node label, target node label and edge label
+ * @author Arend Rensink
+ * @version $Revision$
+ */
+public record TypeNodeKey(TypeLabel label) implements TypeKey {
+    /** Constructs the key for a given type node from its node label. */
+    public TypeNodeKey(TypeNode node) {
+        this(node.label());
+    }
+}

src/main/java/nl/utwente/groove/gui/display/GraphTab.java

@@ -334,9 +334,9 @@ public void undoableEditHappened(UndoableEditEvent e) {
                 // we need to clone the graph to properly freeze the next layout change
                 var graph = jModel.getGraph();
                 assert graph != null;
-                AspectGraph graphClone = graph.clone();
-                graphClone.setFixed();
-                getSimulatorModel().doAddGraph(getResourceKind(), graphClone, true);
+                //AspectGraph graphClone = graph.clone();
+                //graphClone.setFixed();
+                getSimulatorModel().doAddGraph(getResourceKind(), graph, true);
                 loadProperties(jModel);
             } catch (IOException e1) {
                 // do nothing

src/main/java/nl/utwente/groove/gui/tree/LabelFilter.java

@@ -289,7 +289,7 @@ private void notifyIfNonempty(Set<JCell<G>> changedCells) {
      * This is the case if no node type entry is actively filtered, and either unfiltered
      * edges need not be shown or all or all edge entries are also unselected.
      * @param jCell the jCell for which the test is performed
-     * @return {@code true} if {@code jCell} is filtered
+     * @return {@code true} if {@code jCell} is visible
      */
     public boolean isIncluded(JCell<G> jCell) {
         boolean activeShow = false;

src/main/java/nl/utwente/groove/gui/tree/LabelTree.java

@@ -469,13 +469,17 @@ protected StringBuilder getText(Entry entry) {
         return result;
     }
 
-    /** Indicates if a given jCell is entirely filtered. */
+    /** Indicates if a given jCell is entirely filtered.
+     * @return {@code true} if the jCell is currently visible
+     */
     public boolean isIncluded(JCell<G> jCell) {
         synchroniseModel();
         return getFilter().isIncluded(jCell);
     }
 
-    /** Indicates if a given key is actively filtered. */
+    /** Indicates if a given key is actively filtered.
+     * @return {@code true} if the key is currently visible
+     */
     public boolean isIncluded(Label key) {
         synchroniseModel();
         return getFilter().getEntry(key).isSelected();