Removed hashCode and equals from ARG-related classes, added ArgStruct…

…uralEquality

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ARG.java

@@ -21,7 +21,6 @@
 import hu.bme.mit.theta.common.container.Containers;
 
 import java.util.Collection;
-import java.util.Objects;
 import java.util.Optional;
 import java.util.OptionalInt;
 import java.util.stream.Stream;
@@ -221,18 +220,4 @@ public double getMeanBranchingFactor() {
         final double mean = nodesToCalculate.mapToDouble(n -> n.getOutEdges().count()).average().orElse(0);
         return mean;
     }
-
-    @Override
-    public boolean equals(Object o) {
-        if (this == o) return true;
-        if (o == null || getClass() != o.getClass()) return false;
-        ARG<?, ?> arg = (ARG<?, ?>) o;
-        return initialized == arg.initialized &&
-                initNodes.equals(arg.initNodes);
-    }
-
-    @Override
-    public int hashCode() {
-        return Objects.hash(initNodes, initialized, partialOrd);
-    }
 }

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgEdge.java

@@ -18,36 +18,10 @@
 import hu.bme.mit.theta.analysis.Action;
 import hu.bme.mit.theta.analysis.State;
 
-import java.util.Objects;
-
 public final class ArgEdge<S extends State, A extends Action> {
     private static final int HASH_SEED = 3653;
     private volatile int hashCode = 0;
 
-    @Override
-    public boolean equals(Object o) {
-        if (this == o) return true;
-        if (o == null || getClass() != o.getClass()) return false;
-        ArgEdge<?, ?> argEdge = (ArgEdge<?, ?>) o;
-        return Objects.equals(source.getState(), argEdge.source.getState())
-                && Objects.equals(target, argEdge.target)
-                && Objects.equals(action.toString(), argEdge.action.toString());
-    }
-
-    @Override
-    public int hashCode() {
-        int result = hashCode;
-        if (result == 0) {
-            result = HASH_SEED;
-            result = 31 * result + source.getState().hashCode();
-            result = 31 * result + target.getState().hashCode();
-            result = 31 * result + action.toString().hashCode();
-            hashCode = result;
-        }
-        return result;
-        // return Objects.hash(source.getState(), target.getState(), action.toString());
-    }
-
     private final ArgNode<S, A> source;
     private final ArgNode<S, A> target;
     private final A action;

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgNode.java

@@ -20,7 +20,9 @@
 import hu.bme.mit.theta.common.Utils;
 import hu.bme.mit.theta.common.container.Containers;
 
-import java.util.*;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Optional;
 import java.util.stream.Stream;
 
 import static com.google.common.base.Preconditions.checkArgument;
@@ -270,29 +272,6 @@ private Stream<ArgNode<S, A>> unexcludedDescendantsOfNode() {
 
     ////
 
-    @Override
-    public int hashCode() {
-        int result = hashCode;
-        if (result == 0) {
-            result = HASH_SEED;
-            result = 31 * result + id;
-            hashCode = result;
-        }
-        return result;
-    }
-
-    @Override
-    public boolean equals(Object o) {
-        if (this == o) return true;
-        if (o == null || getClass() != o.getClass()) return false;
-        ArgNode<?, ?> argNode = (ArgNode<?, ?>) o;
-        return depth == argNode.depth &&
-                state.equals(argNode.state) &&
-                coveringNode.equals(argNode.coveringNode) &&
-                Set.copyOf(outEdges).equals(Set.copyOf(argNode.outEdges)) &&
-                target == argNode.target;
-    }
-
     @Override
     public String toString() {
         return Utils.lispStringBuilder("ArgNode").add(id).body().add(state).toString();

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgStructuralEquality.java

@@ -0,0 +1,160 @@
+/*
+ *  Copyright 2023 Budapest University of Technology and Economics
+ *
+ *  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.
+ */
+
+package hu.bme.mit.theta.analysis.algorithm;
+
+import hu.bme.mit.theta.analysis.Action;
+import hu.bme.mit.theta.analysis.State;
+
+import java.util.LinkedHashMap;
+import java.util.Map;
+import java.util.stream.Collectors;
+
+import static com.google.common.base.Objects.equal;
+
+/**
+ * Structural comparisons using equal() and hashCode() for ARG-related classes.
+ * Each node is uniquely identifiable using its incoming edge (or its absence), and wrapped state.
+ * Each edge is uniquely identifiable using its source node, and wrapped action.
+ * An ARG is uniquely identifiable using its leaf nodes.
+ * An ArgTrace is uniquely identifiable using its last node.
+ * <p>
+ * We perform caching for the hash codes, but equals() checks will always traverse the ancestors of
+ * a node (and edge). However, this traversal only goes towards the root, rather than in all
+ * directions.
+ */
+public final class ArgStructuralEquality {
+    private static final Map<Object, Integer> hashCodeCache = new LinkedHashMap<>();
+
+    private ArgStructuralEquality(){
+    }
+
+    public static boolean equals(final ArgNode<? extends State, ? extends Action> n1,
+                                 final ArgNode<? extends State, ? extends Action> n2) {
+
+        // if one node has a parent but the other one does not, nodes are not equal
+        if(n1.inEdge.isPresent() != n2.inEdge.isPresent()) {
+            return false;
+        }
+
+        // if in edge is not same, nodes are not equal
+        if(n1.inEdge.isPresent() && !equals(n1.inEdge.get(), n2.inEdge.get())) {
+            return false;
+        }
+
+        // if wrapped state is not same, nodes are not equal
+        if(!n1.getState().equals(n2.getState())) {
+            return false;
+        }
+
+        return true;
+    }
+
+    public static boolean equals(final ArgEdge<? extends State, ? extends Action> e1,
+                                 final ArgEdge<? extends State, ? extends Action> e2) {
+
+        // if source node is not same, edges are not equal
+        if(!equals(e1.getSource(), e2.getSource())) {
+            return false;
+        }
+
+        // if wrapped action is not same, edges are not equal
+        if(!e1.getAction().equals(e2.getAction())) {
+            return false;
+        }
+
+        return true;
+    }
+
+    public static boolean equals(final ARG<? extends State, ? extends Action> a1,
+                                 final ARG<? extends State, ? extends Action> a2) {
+
+        var leaves1 = a1.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet());
+        var leaves2 = a2.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet());
+
+        // if the two ARGs contain a different number of leaf nodes, they are not equal
+        if(leaves1.size() != leaves2.size()) {
+            return false;
+        }
+
+        leaves1loop:
+        for (ArgNode<? extends State, ? extends Action> n1 : leaves1) {
+            for (ArgNode<? extends State, ? extends Action> n2 : leaves2) {
+                if(equals(n1, n2)) {
+                    continue leaves1loop;
+                }
+            }
+            // a leaf node did not have a corresponding leaf node in the other arg
+            return false;
+        }
+        return true;
+    }
+
+    public static boolean equals(final ArgTrace<? extends State, ? extends Action> t1,
+                                 final ArgTrace<? extends State, ? extends Action> t2) {
+
+        return equal(t1.node(t1.length()), t2.node(t2.length()));
+    }
+
+
+    public static int hashCode(final ArgNode<? extends State, ? extends Action> n) {
+        if(!hashCodeCache.containsKey(n)) {
+            int hashcode = 0;
+
+            if(n.inEdge.isPresent()) {
+                hashcode += hashCode(n.inEdge.get());
+            }
+
+            hashcode += n.getState().hashCode();
+            hashCodeCache.put(n, hashcode);
+        }
+        return hashCodeCache.get(n);
+    }
+
+    public static int hashCode(final ArgEdge<? extends State, ? extends Action> e) {
+        if(!hashCodeCache.containsKey(e)) {
+            int hashcode = 0;
+
+            hashcode += hashCode(e.getSource());
+
+            hashcode += e.getAction().hashCode();
+
+            hashCodeCache.put(e, hashcode);
+        }
+        return hashCodeCache.get(e);
+    }
+
+    // ARG is not immutable, so we don't cache
+    public static int hashCode(final ARG<? extends State, ? extends Action> a) {
+        int hashcode = 0;
+
+        var leaves = a.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet());
+        for (ArgNode<? extends State, ? extends Action> leaf : leaves) {
+            hashcode += hashCode(leaf);
+        }
+
+        return hashcode;
+    }
+
+    public static int hashCode(final ArgTrace<? extends State, ? extends Action> t) {
+        if(!hashCodeCache.containsKey(t)) {
+            int hashcode = hashCode(t.node(t.length()));
+            hashCodeCache.put(t, hashcode);
+        }
+        return hashCodeCache.get(t);
+    }
+
+}

subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgTrace.java

@@ -116,30 +116,4 @@ public Iterator<ArgNode<S, A>> iterator() {
         return nodes.iterator();
     }
 
-    @Override
-    public boolean equals(Object o) {
-        if (this == o) {
-            return true;
-        }
-        if (o == null || getClass() != o.getClass()) {
-            return false;
-        }
-        ArgTrace<?, ?> argTrace = (ArgTrace<?, ?>) o;
-        return states.equals(argTrace.states); // && edges.equals(argTrace.edges);
-    }
-
-    @Override
-    public int hashCode() {
-        int result = hashCode;
-        if (result == 0) {
-            result = HASH_SEED;
-            result = 31 * result + states.hashCode();
-            result = 31 * result + edges.hashCode();
-            hashCode = result;
-        }
-        return result;
-        // return Objects.hash(states, edges);
-    }
-    ////
-
 }

subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaState.kt

@@ -300,7 +300,7 @@ data class XcfaProcessState(val locs: LinkedList<XcfaLocation>, val varLookup: L
 
     override fun hashCode(): Int {
         var result = locs.hashCode()
-        result = 31 * result + paramsInitialized.hashCode() // TODO FRICKIN INNER STATE HASH
+        result = 31 * result + paramsInitialized.hashCode()
         return result
     }