From 274b07dab03b183ebf682bf1ae71e64decdf5f3f Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Thu, 9 Nov 2023 16:49:22 +0100
Subject: [PATCH] Added CexMonitor update

---
 .../theta/analysis/algorithm/ArgStructuralEquality.java    | 7 ++++---
 .../analysis/runtimemonitor/container/CexHashStorage.kt    | 5 +++--
 2 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgStructuralEquality.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgStructuralEquality.java
index 2631cb362e..4f7585db03 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgStructuralEquality.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/ArgStructuralEquality.java
@@ -21,6 +21,7 @@
 
 import java.util.LinkedHashMap;
 import java.util.Map;
+import java.util.Set;
 import java.util.stream.Collectors;
 
 import static com.google.common.base.Objects.equal;
@@ -82,8 +83,8 @@ public static boolean equals(final ArgEdge<? extends State, ? extends Action> e1
     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());
+        Set<ArgNode<? extends State, ? extends Action>> leaves1 = a1.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet());
+        Set<ArgNode<? extends State, ? extends Action>> 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()) {
@@ -141,7 +142,7 @@ public static int hashCode(final ArgEdge<? extends State, ? extends Action> e) {
     public static int hashCode(final ARG<? extends State, ? extends Action> a) {
         int hashcode = 0;
 
-        var leaves = a.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet());
+        Set<ArgNode<? extends State, ? extends Action>> leaves = a.getNodes().filter(ArgNode::isLeaf).collect(Collectors.toUnmodifiableSet());
         for (ArgNode<? extends State, ? extends Action> leaf : leaves) {
             hashcode += hashCode(leaf);
         }
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/container/CexHashStorage.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/container/CexHashStorage.kt
index ba42658891..d1dc1d49a1 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/container/CexHashStorage.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/runtimemonitor/container/CexHashStorage.kt
@@ -17,6 +17,7 @@ package hu.bme.mit.theta.analysis.runtimemonitor.container
 
 import hu.bme.mit.theta.analysis.Action
 import hu.bme.mit.theta.analysis.State
+import hu.bme.mit.theta.analysis.algorithm.ArgStructuralEquality
 import hu.bme.mit.theta.analysis.algorithm.ArgTrace
 
 class CexHashStorage<S : State?, A : Action?> :
@@ -24,10 +25,10 @@ class CexHashStorage<S : State?, A : Action?> :
 
     private val counterexamples: MutableSet<Int> = LinkedHashSet()
     override fun addData(newData: ArgTrace<S, A>?) {
-        counterexamples.add(newData.hashCode())
+        counterexamples.add(ArgStructuralEquality.hashCode(newData))
     }
 
     override operator fun contains(data: ArgTrace<S, A>?): Boolean {
-        return counterexamples.contains(data.hashCode())
+        return counterexamples.contains(ArgStructuralEquality.hashCode(data))
     }
 }
\ No newline at end of file