fix hb function bug

Author: Ramanathan0908

.gitignore

@@ -1,5 +1,6 @@
 obj/
 traces/
+witness/
 predictor
 run_tests
 .vscode/

scripts/runner.sh

@@ -0,0 +1,60 @@
+#!/bin/bash
+
+SCRIPT_DIR="$(dirname "$(realpath "$0")")"
+PROJECT_DIR="$(dirname "$SCRIPT_DIR")"
+TRACES_DIR="$PROJECT_DIR/traces"
+PROGRAM="$PROJECT_DIR/predictor"
+
+TIMEOUT=600
+
+if [ ! -f "$PROGRAM" ]; then
+    echo "Error: $PROGRAM not found"
+    exit 1
+fi
+
+BENCHMARK_TRACES=(
+    # "cryptorsa" 
+    # "linkedlist" 
+    # "lusearch" 
+    # "xalan" 
+    # "bufwriter" 
+    # "moldyn" 
+    # "readerswriters" 
+    # "ftpserver" 
+    # "derby" 
+    "jigsaw"
+    "account" 
+    "airlinetickets" 
+    "array" 
+    "boundedbuffer" 
+    "bubblesort" 
+    "clean" 
+    "critical" 
+    "lang" 
+    "mergesort" 
+    "pingpong" 
+    "producerconsumer" 
+    "raytracer" 
+    "twostage" 
+    "wronglock"
+)
+
+for trace in "${BENCHMARK_TRACES[@]}"; do
+
+    if [ ! -f "$TRACES_DIR/$trace" ]; then
+        echo "Error: $trace not found"
+        continue
+    fi
+
+    echo "Running $trace"
+    gtimeout $TIMEOUT "$PROGRAM" -f "$TRACES_DIR/$trace" 2>&1
+    EXIT_CODE=$?
+
+    if [ $EXIT_CODE -eq 124 ]; then
+        echo "Error: $trace timed out"
+        continue
+    elif [ $EXIT_CODE -ne 0 ]; then
+        echo "Error: $trace failed with exit code $EXIT_CODE"
+        continue
+    fi
+done

src/casual_model.cpp

@@ -253,14 +253,15 @@ uint32_t CasualModel::solve() {
         z3::expr_vector race_sat(c_);
         race_sat.push_back(race_con);
 
+        auto [e1, e2] = filtered_cop_events_[i];
+
         if (s_.check(race_sat) == z3::sat) {
             race_count++;
-
             if (log_witness_) {
-                auto [e1, e2] = filtered_cop_events_[i];
                 logger_.logWitnessPrefix(s_.get_model(), e1, e2);
             }
         }
+
         i++;
     }
 

src/casual_model.h

@@ -4,6 +4,7 @@
 #include <utility>
 #include <vector>
 
+#include "BSlogger.hpp"
 #include "event.h"
 #include "lockset_engine.h"
 #include "trace.h"
@@ -54,7 +55,7 @@ class CasualModel {
 
     inline bool hb(const Event& e1, const Event& e2) {
         return mhb_closure_.happensBefore(e1, e2) ||
-               (e1.getTargetId() == e2.getTargetId() &&
+               (e1.getThreadId() == e2.getThreadId() &&
                 e1.getEventId() < e2.getEventId());
     }