Skip to content

Commit

Permalink
Added CexMonitor update
Browse files Browse the repository at this point in the history
  • Loading branch information
leventeBajczi committed Nov 9, 2023
1 parent 8aa168f commit 274b07d
Show file tree
Hide file tree
Showing 2 changed files with 7 additions and 5 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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()) {
Expand Down Expand Up @@ -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);
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,17 +17,18 @@ 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?> :
RuntimeDataCollection<ArgTrace<S, A>?> {

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))
}
}

0 comments on commit 274b07d

Please sign in to comment.