From e5c48c745b7fa71ef1d85c6f5bec74b2c8870585 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Sun, 7 Dec 2025 10:53:42 +0100
Subject: [PATCH 01/20] Support round-robin scheduling for trace exploration

When choosing between different enabled threads while expanding a trace
during the exploration phase of DPOR, McMini can choose arbitrarily
among the enabled threads. Historically, McMini has always chosen the
first enabled thread in thread id order (i.e. picking in order of which
thread was created first in program order). This commit introduces a new
scheduling paradigm whereby McMini selects threads in a round-robin
manner during exploration. The algorithm can be roughly summarized as
follows:

  1. Among unscheduled threads, McMini always picks the smallest thread
  2. If all threads have been scheduled, McMini picks the first enabled
     thread in its round robin schedule and marks the thread as being
     least desired for the next scheduling step.
---
 include/mcmini/model/config.hpp               | 15 +++-
 include/mcmini/model/pending_transitions.hpp  |  1 +
 .../algorithms/classic_dpor.hpp               |  5 +-
 .../algorithms/classic_dpor/stack_item.hpp    |  3 +
 src/mcmini/mcmini.cpp                         | 33 ++++++-
 .../algorithms/classic_dpor.cpp               | 87 ++++++++++++++++---
 6 files changed, 127 insertions(+), 17 deletions(-)

diff --git a/include/mcmini/model/config.hpp b/include/mcmini/model/config.hpp
index f492590..5ce48c4 100644
--- a/include/mcmini/model/config.hpp
+++ b/include/mcmini/model/config.hpp
@@ -13,16 +13,27 @@ namespace model {
 struct config {
   /**
    * The maximum number of transitions that can be run
-   * by any single thread while running the model checker
+   * by any _single thread_ while running the model checker
    */
   uint64_t max_thread_execution_depth;
 
+  /**
+   * The maximum number of transitions that can be contained in any given trace.
+   */
+  uint64_t maximum_total_execution_depth = 1500;
+
   /**
    * The trace id to stop the model checker at
    * to print the contents of the transition stack
    */
   trid_t target_trace_id;
 
+  /**
+   * Whether or not exploration occurs using round robin scheduling (default is
+   * smallest tid first)
+   */
+  bool use_round_robin_scheduling = false;
+
   /**
    * Whether model checking should halt at the first encountered deadlock
    */
@@ -63,4 +74,4 @@ struct config {
   // file path is provided (TODO).
   logging::severity_level global_severity_level = logging::severity_level::info;
 };
-}  // namespace model
+} // namespace model
diff --git a/include/mcmini/model/pending_transitions.hpp b/include/mcmini/model/pending_transitions.hpp
index 668db87..ec65268 100644
--- a/include/mcmini/model/pending_transitions.hpp
+++ b/include/mcmini/model/pending_transitions.hpp
@@ -43,6 +43,7 @@ struct pending_transitions final {
   }
   auto cend() -> decltype(_contents.cend()) const { return _contents.cend(); }
   size_t size() const { return this->_contents.size(); }
+  bool empty() const { return this->_contents.empty(); }
   /**
    * @brief Returns the transition mapped to id `id`, or `nullptr` if no such
    * runner has been mapped to an id.
diff --git a/include/mcmini/model_checking/algorithms/classic_dpor.hpp b/include/mcmini/model_checking/algorithms/classic_dpor.hpp
index 931e001..b186a95 100644
--- a/include/mcmini/model_checking/algorithms/classic_dpor.hpp
+++ b/include/mcmini/model_checking/algorithms/classic_dpor.hpp
@@ -36,12 +36,15 @@ class classic_dpor final : public algorithm {
         classic_dpor::default_coenabledness();
     uint32_t maximum_total_execution_depth = 1500;
     bool assumes_linear_program_flow = false;
+
+    enum class exploration_policy : uint { round_robin, smallest_first };
+    exploration_policy policy = exploration_policy::smallest_first;
   };
 
   classic_dpor() = default;
   classic_dpor(configuration config) : config(std::move(config)) {}
 
- private:
+private:
   configuration config;
 
   bool are_dependent(const model::transition &t1,
diff --git a/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp b/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp
index 8e41fb5..fd5f2a6 100644
--- a/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp
+++ b/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp
@@ -231,6 +231,9 @@ struct stack_item final {
     }
     return r;
   }
+  const bool is_enabled(runner_id_t rid) {
+    return this->enabled_runners.count(rid) > 0;
+  }
   const std::unordered_set<runner_id_t> &get_enabled_runners() const {
     return this->enabled_runners;
   }
diff --git a/src/mcmini/mcmini.cpp b/src/mcmini/mcmini.cpp
index 025c28e..f124d97 100644
--- a/src/mcmini/mcmini.cpp
+++ b/src/mcmini/mcmini.cpp
@@ -190,7 +190,15 @@ void do_model_checking(const config& config) {
   std::cerr << "\n\n**************** INTIAL STATE *********************\n\n";
   std::cerr.flush();
 
-  model_checking::classic_dpor classic_dpor_checker;
+  using mcconfig = model_checking::classic_dpor::configuration;
+  mcconfig mc_config;
+  mc_config.maximum_total_execution_depth =
+      config.maximum_total_execution_depth;
+  mc_config.policy = config.use_round_robin_scheduling
+                         ? mcconfig::exploration_policy::round_robin
+                         : mcconfig::exploration_policy::smallest_first;
+
+  model_checking::classic_dpor classic_dpor_checker(std::move(mc_config));
   c.trace_completed = &finished_trace_classic_dpor;
   c.deadlock = &found_deadlock;
   c.undefined_behavior = &found_undefined_behavior;
@@ -397,18 +405,33 @@ int main_cpp(int argc, const char** argv) {
       mcmini_config.max_thread_execution_depth =
           strtoul(cur_arg[1], nullptr, 10);
 
-      char* endptr;
+      char *endptr;
       if (strtol(cur_arg[1], &endptr, 10) == 0 || endptr[0] != '\0') {
         fprintf(stderr, "%s: illegal value\n", "--max-depth-per-thread");
         exit(1);
       }
       cur_arg += 2;
+    } else if (strcmp(cur_arg[0], "--max-depth-per-trace") == 0 ||
+               strcmp(cur_arg[0], "-M") == 0) {
+      mcmini_config.maximum_total_execution_depth =
+          strtoul(cur_arg[1], nullptr, 10);
+
+      char *endptr;
+      if (strtol(cur_arg[1], &endptr, 10) == 0 || endptr[0] != '\0') {
+        fprintf(stderr, "%s: illegal value\n", "--max-depth-per-trace");
+        exit(1);
+      }
+      cur_arg += 2;
     } else if (strcmp(cur_arg[0], "--interval") == 0 ||
                strcmp(cur_arg[0], "-i") == 0) {
       mcmini_config.record_target_executable_only = true;
       mcmini_config.checkpoint_period =
           std::chrono::seconds(strtoul(cur_arg[1], nullptr, 10));
       cur_arg += 2;
+    } else if ((strcmp(cur_arg[0], "--round-robin") == 0) ||
+               strcmp(cur_arg[0], "-rr") == 0) {
+      mcmini_config.use_round_robin_scheduling = true;
+      cur_arg += 1;
     } else if (strcmp(cur_arg[0], "--from-checkpoint") == 0 ||
                strcmp(cur_arg[0], "-ckpt") == 0) {
       mcmini_config.checkpoint_file = cur_arg[1];
@@ -453,7 +476,9 @@ int main_cpp(int argc, const char** argv) {
           "              [--record|-r <seconds>] \n"
           "              [--from-checkpoint <ckpt>] [--multithreaded-fork] \n"
           "              [--max-depth-per-thread|-m <num>]\n"
+          "              [--max-depth-per-trace|-M <num>]\n"
           "              [--first-deadlock|--first|-f]\n"
+          "              [--round-robin|-rr]\n"
           "              [--log-level|-log <level>]\n"
           "              [--help|-h]\n"
           "              target_executable\n");
@@ -503,10 +528,10 @@ int main_cpp(int argc, const char** argv) {
   return EXIT_SUCCESS;
 }
 
-int main(int argc, const char** argv) {
+int main(int argc, const char **argv) {
   try {
     return main_cpp(argc, argv);
-  } catch (const std::exception& e) {
+  } catch (const std::exception &e) {
     std::cerr << "ERROR: " << e.what() << std::endl;
     return EXIT_FAILURE;
   } catch (...) {
diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index 2504f21..69c0fcf 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -7,6 +7,7 @@
 #include <csignal>
 #include <cstddef>
 #include <iostream>
+#include <list>
 #include <set>
 #include <stdexcept>
 #include <string>
@@ -114,6 +115,9 @@ void classic_dpor::verify_using(coordinator &coordinator,
   /// The initial entry into the stack represents the information DPOR tracks
   /// for state `s_0`.
   log_debug(dpor_logger) << "Initializing the DPOR stack";
+  bool reached_max_depth = false;
+  std::list<runner_id_t> round_robin_sched;
+
   stats model_checking_stats;
   dpor_context context(coordinator);
   auto &dpor_stack = context.stack;
@@ -128,21 +132,67 @@ void classic_dpor::verify_using(coordinator &coordinator,
     // 2. Exploration phase
     while (dpor_stack.back().has_enabled_runners()) {
       if (dpor_stack.size() >= this->config.maximum_total_execution_depth) {
-        throw std::runtime_error(
-            "*** Execution Limit Reached! ***\n\n"
-            "McMini ran a trace with" +
-            std::to_string(dpor_stack.size()) +
-            " transitions which is\n"
-            "the more than McMini was configured to handle in any one trace (" +
-            std::to_string(this->config.maximum_total_execution_depth) +
-            "). Try running mcmini with the \"--max-depth-per-thread\" flag\n"
-            "to limit how far into a trace McMini can go\n");
+        if (!reached_max_depth) {
+          log_unexpected(dpor_logger)
+              << "*** Execution Limit Reached! ***\n\n"
+              << "McMini encountered a trace with" << dpor_stack.size()
+              << " transitions which is the most that McMini was configured"
+              << " to handle in any given trace ("
+              << this->config.maximum_total_execution_depth
+              << "). McMini will continue its search, but it may be "
+                 "incomplete. Rerun McMini with the "
+                 "\"--max-depth-per-thread\" "
+              << "flag for correct results.";
+        }
+        reached_max_depth = true;
+        break;
       }
       // NOTE: For deterministic results, always choose the "first" enabled
       // runner. A runner precedes another runner in being enabled iff it has a
       // smaller id.
       try {
-        const runner_id_t rid = dpor_stack.back().get_first_enabled_runner();
+        runner_id_t rid;
+        switch (config.policy) {
+        case configuration::exploration_policy::smallest_first: {
+          rid = dpor_stack.back().get_first_enabled_runner();
+          break;
+        }
+        case configuration::exploration_policy::round_robin: {
+          auto unscheduled_runners = dpor_stack.back().get_enabled_runners();
+
+          // For round robin scheduling, always prefer to schedule
+          // threads that don't appear in `round_robin_sched` because
+          // these threads are necessarily unscheduled wrt the previous starting
+          // point.
+          //
+          // 1. Among those threads not appearing in the round robin
+          // schedule, always pick the smallest.
+          // 2. If every enabled thread has already been scheduled, then pick
+          // the first based on the round robin schedule and move it to the back
+          // of the list. NOTE: Every enabled runner is in `round_robin_sched`,
+          // but the converse is not necessarily true (i.e. there may be threads
+          // in `round_robin_sched` that aren't enabled)
+          for (const runner_id_t id : round_robin_sched) {
+            unscheduled_runners.erase(id);
+          }
+          if (!unscheduled_runners.empty()) {
+            rid = *std::min_element(unscheduled_runners.begin(),
+                                    unscheduled_runners.end());
+            round_robin_sched.push_back(rid);
+          } else {
+            auto it =
+                std::find_if(round_robin_sched.begin(), round_robin_sched.end(),
+                             [&](const runner_id_t id) {
+                               return dpor_stack.back().is_enabled(id);
+                             });
+            assert(it != round_robin_sched.end());
+            round_robin_sched.splice(round_robin_sched.end(), round_robin_sched,
+                                     it);
+            rid = *it;
+          }
+        }
+        }
+
         this->continue_dpor_by_expanding_trace_with(rid, context);
         model_checking_stats.total_transitions++;
 
@@ -208,6 +258,23 @@ void classic_dpor::verify_using(coordinator &coordinator,
       try {
         this->continue_dpor_by_expanding_trace_with(
             dpor_stack.back().backtrack_set_pop_first(), context);
+
+        // If we're doing round robin scheduling for expanding the trace,
+        // backtracking forces a restart of the round robin process.
+        // Intuitively, this makes sense: round robin only applies when
+        // searching _new_ traces. However, we could be a little more
+        // intelligent here and resume the round robin from where it _should_
+        // continue, but that's a little more complicated.
+        //
+        // That is, if the trace after backtracking is e.g.
+        //
+        // 1, 2, 3, 1, 2, _2_
+        //
+        // where _2_ was inserted as a backtrack point, then we could notice
+        // that _3_ was technically supposed to be next in the round robin
+        // scheduling. The current method would schedule 1, then 2, then 3, ...
+        // since we only account for scheduling that occurs during _expansion_.
+        round_robin_sched.clear();
       } catch (const model::undefined_behavior_exception &ube) {
         if (callbacks.undefined_behavior)
           callbacks.undefined_behavior(coordinator, model_checking_stats, ube);

From 06932df29ae21686ef8799df4ac80f54619dcc2d Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Sun, 7 Dec 2025 11:18:52 +0100
Subject: [PATCH 02/20] Fix deadlock detection for main thread exit

The main thread should be allowed to exit in the model. The
`libmcmini.so` side already handles the case where the main thread exits
for good by simply forcing the main thread to block forever and reporting
back to McMini that the thread indeed exited
---
 .../mcmini/model/transitions/thread/thread_exit.hpp  | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/include/mcmini/model/transitions/thread/thread_exit.hpp b/include/mcmini/model/transitions/thread/thread_exit.hpp
index 7509ff2..faa347f 100644
--- a/include/mcmini/model/transitions/thread/thread_exit.hpp
+++ b/include/mcmini/model/transitions/thread/thread_exit.hpp
@@ -8,14 +8,14 @@ namespace model {
 namespace transitions {
 
 struct thread_exit : public model::transition {
- public:
+public:
   thread_exit(state::runner_id_t executor) : transition(executor) {}
   ~thread_exit() = default;
 
-  status modify(model::mutable_state& s) const override {
+  status modify(model::mutable_state &s) const override {
     using namespace model::objects;
-    auto* thread_state = s.get_state_of_runner<thread>(executor);
-    if (!thread_state->is_running() || executor == RID_MAIN_THREAD) {
+    auto *thread_state = s.get_state_of_runner<thread>(executor);
+    if (!thread_state->is_running()) {
       return status::disabled;
     }
     s.add_state_for_runner(executor, new thread(thread::exited));
@@ -25,5 +25,5 @@ struct thread_exit : public model::transition {
   std::string to_string() const override { return "exits"; }
 };
 
-}  // namespace transitions
-}  // namespace model
+} // namespace transitions
+} // namespace model

From 58befda8575f9034b5603700ad348acc0f812217 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Sun, 7 Dec 2025 11:35:34 +0100
Subject: [PATCH 03/20] Fix bug with "stop at first deadlock"

Support for stoping at the first deadlock wasn't completed. This commit
resolves this
---
 .../model_checking/algorithms/classic_dpor.hpp       |  1 +
 src/mcmini/mcmini.cpp                                |  1 +
 .../model_checking/algorithms/classic_dpor.cpp       | 12 ++++++++++--
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/include/mcmini/model_checking/algorithms/classic_dpor.hpp b/include/mcmini/model_checking/algorithms/classic_dpor.hpp
index b186a95..f9bd7e9 100644
--- a/include/mcmini/model_checking/algorithms/classic_dpor.hpp
+++ b/include/mcmini/model_checking/algorithms/classic_dpor.hpp
@@ -39,6 +39,7 @@ class classic_dpor final : public algorithm {
 
     enum class exploration_policy : uint { round_robin, smallest_first };
     exploration_policy policy = exploration_policy::smallest_first;
+    bool stop_at_first_deadlock = false;
   };
 
   classic_dpor() = default;
diff --git a/src/mcmini/mcmini.cpp b/src/mcmini/mcmini.cpp
index f124d97..47b2876 100644
--- a/src/mcmini/mcmini.cpp
+++ b/src/mcmini/mcmini.cpp
@@ -194,6 +194,7 @@ void do_model_checking(const config& config) {
   mcconfig mc_config;
   mc_config.maximum_total_execution_depth =
       config.maximum_total_execution_depth;
+  mc_config.stop_at_first_deadlock = config.stop_at_first_deadlock;
   mc_config.policy = config.use_round_robin_scheduling
                          ? mcconfig::exploration_policy::round_robin
                          : mcconfig::exploration_policy::smallest_first;
diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index 69c0fcf..10719b0 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -232,8 +232,16 @@ void classic_dpor::verify_using(coordinator &coordinator,
     if (callbacks.trace_completed)
       callbacks.trace_completed(coordinator, model_checking_stats);
 
-    if (callbacks.deadlock &&
-        coordinator.get_current_program_model().is_in_deadlock())
+    if (config.stop_at_first_deadlock &&
+        coordinator.get_current_program_model().is_in_deadlock()) {
+      log_info(dpor_logger)
+          << "First deadlock found. Reporting and stopping model checking.";
+      if (callbacks.deadlock)
+        callbacks.deadlock(coordinator, model_checking_stats);
+
+      return;
+    } else if (callbacks.deadlock &&
+               coordinator.get_current_program_model().is_in_deadlock())
       callbacks.deadlock(coordinator, model_checking_stats);
 
     // 3. Backtrack phase

From 789db743f2248371eb66e1dc4c066e00d04e4a4b Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Tue, 9 Dec 2025 10:24:46 +0100
Subject: [PATCH 04/20] Move race detection inside classic_dpor::dpor_stack

---
 .../algorithms/classic_dpor.hpp               | 11 +---
 .../algorithms/classic_dpor.cpp               | 60 +++++++++----------
 2 files changed, 30 insertions(+), 41 deletions(-)

diff --git a/include/mcmini/model_checking/algorithms/classic_dpor.hpp b/include/mcmini/model_checking/algorithms/classic_dpor.hpp
index f9bd7e9..05bcab9 100644
--- a/include/mcmini/model_checking/algorithms/classic_dpor.hpp
+++ b/include/mcmini/model_checking/algorithms/classic_dpor.hpp
@@ -12,7 +12,7 @@ namespace model_checking {
  * algorithm of Flanagan and Godefroid (2005).
  */
 class classic_dpor final : public algorithm {
- public:
+public:
   using dependency_relation_type =
       double_dispatch_member_function_table<const model::transition,
                                             bool(void)>;
@@ -63,13 +63,6 @@ class classic_dpor final : public algorithm {
   // the DPOR algorithm and are called at specific points in time!
 
   struct dpor_context;
-
-  bool happens_before(const dpor_context &, size_t i, size_t j) const;
-  bool happens_before_thread(const dpor_context &, size_t i,
-                             runner_id_t p) const;
-  bool threads_race_after(const dpor_context &context, size_t i, runner_id_t q,
-                          runner_id_t p) const;
-
   clock_vector accumulate_max_clock_vector_against(const model::transition &,
                                                    const dpor_context &) const;
 
@@ -83,4 +76,4 @@ class classic_dpor final : public algorithm {
       runner_id_t p);
 };
 
-}  // namespace model_checking
+} // namespace model_checking
diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index 10719b0..f47a101 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -45,6 +45,29 @@ struct classic_dpor::dpor_context {
   const transition *get_transition(int i) const {
     return stack.at(i).get_out_transition();
   }
+
+  bool happens_before(size_t i, size_t j) const {
+    const runner_id_t rid = stack.at(i).get_out_transition()->get_executor();
+    const clock_vector &cv = stack.at(j).get_clock_vector();
+    return i <= cv.value_for(rid);
+  }
+
+  bool happens_before_thread(size_t i, runner_id_t p) const {
+    const runner_id_t rid = get_transition(i)->get_executor();
+    const clock_vector &cv =
+        stack.back().get_per_runner_clocks()[p].get_clock_vector();
+    return i <= cv.value_for(rid);
+  }
+
+  bool threads_race_after(size_t i, runner_id_t q, runner_id_t p) const {
+    const size_t transition_stack_height = stack.size() - 1;
+    for (size_t j = i + 1; j < transition_stack_height; j++) {
+      if (q == get_transition(j)->get_executor() &&
+          this->happens_before_thread(j, p))
+        return true;
+    }
+    return false;
+  }
 };
 
 clock_vector classic_dpor::accumulate_max_clock_vector_against(
@@ -75,37 +98,10 @@ bool classic_dpor::are_dependent(const model::transition &t1,
          this->config.dependency_relation.call_or(true, &t1, &t2);
 }
 
-bool classic_dpor::happens_before(const dpor_context &context, size_t i,
-                                  size_t j) const {
-  const runner_id_t rid =
-      context.stack.at(i).get_out_transition()->get_executor();
-  const clock_vector &cv = context.stack.at(j).get_clock_vector();
-  return i <= cv.value_for(rid);
-}
-
-bool classic_dpor::happens_before_thread(const dpor_context &context, size_t i,
-                                         runner_id_t p) const {
-  const runner_id_t rid = context.get_transition(i)->get_executor();
-  const clock_vector &cv =
-      context.stack.back().get_per_runner_clocks()[p].get_clock_vector();
-  return i <= cv.value_for(rid);
-}
-
-bool classic_dpor::threads_race_after(const dpor_context &context, size_t i,
-                                      runner_id_t q, runner_id_t p) const {
-  const size_t transition_stack_height = context.stack.size() - 1;
-  for (size_t j = i + 1; j < transition_stack_height; j++) {
-    if (q == context.get_transition(j)->get_executor() &&
-        this->happens_before_thread(context, j, p))
-      return true;
-  }
-  return false;
-}
-
 void classic_dpor::verify_using(coordinator &coordinator,
                                 const callbacks &callbacks) {
   // The code below is an implementation of the model-checking algorithm of
-  // Flanagan and Godefroid from 2015.
+  // Flanagan and Godefroid from 2005.
 
   // 1. Data structure set up
 
@@ -238,7 +234,6 @@ void classic_dpor::verify_using(coordinator &coordinator,
           << "First deadlock found. Reporting and stopping model checking.";
       if (callbacks.deadlock)
         callbacks.deadlock(coordinator, model_checking_stats);
-
       return;
     } else if (callbacks.deadlock &&
                coordinator.get_current_program_model().is_in_deadlock())
@@ -468,17 +463,18 @@ bool classic_dpor::dynamically_update_backtrack_sets_at_index(
   // TODO: add in co-enabled conditions
   const bool has_reversible_race = this->are_dependent(next_sp, S_i) &&
                                    this->are_coenabled(next_sp, S_i) &&
-                                   !this->happens_before_thread(context, i, p);
+                                   !context.happens_before_thread(i, p);
 
   // If there exists i such that ...
   if (has_reversible_race) {
     std::set<runner_id_t> e;
 
     for (runner_id_t const q : pre_si.get_enabled_runners()) {
-      const bool in_e = q == p || this->threads_race_after(context, i, q, p);
+      const bool in_e = q == p || context.threads_race_after(i, q, p);
 
       // If E != empty set
-      if (in_e && !pre_si.sleep_set_contains(q)) e.insert(q);
+      if (in_e && !pre_si.sleep_set_contains(q))
+        e.insert(q);
     }
 
     if (e.empty()) {

From f2fa56d66ea3f54ba657be6799e5b5ae340defb6 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Wed, 10 Dec 2025 20:59:01 +0100
Subject: [PATCH 05/20] Fix bug in model checker clock vector logic

*** Important bug fix ***
This commit resolves a subtle bug in the model checking logic for
detecting reversible races. The DPOR paper of Flanagan and Godefroid
uses clock vectors to determine in O(1) time whether two transitions in
the transition stack (or trace) t_i and t_j are in a "happens-before"
relationship (calculating the clocks requires traversing the stack
however). The original pseudocode reads

i -->_S j <----> i <= C(j)(proc(S_i))

where S = {1, 2, ..., N} is the sequence of transitions, i and j are in
[1, N], S_i is the `i`th transition, proc(S_i) is the thread id of the
`i`th transition, and `C(j)` is the value of the `j`th clock vector.

The question arises to where `C(j)` is stored. The pseudocode notes that
`C([p := cv2, |S'| := cv2]`. That is, the clock vector `C[l]` where
`l` is the subtrace including transition `l`, is contained in the `l +
1`th state stack position, NOT the `lth`.
---
 src/mcmini/model_checking/algorithms/classic_dpor.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index f47a101..d05ca99 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -47,8 +47,8 @@ struct classic_dpor::dpor_context {
   }
 
   bool happens_before(size_t i, size_t j) const {
-    const runner_id_t rid = stack.at(i).get_out_transition()->get_executor();
-    const clock_vector &cv = stack.at(j).get_clock_vector();
+    const runner_id_t rid = get_transition(i)->get_executor();
+    const clock_vector &cv = stack.at(j + 1).get_clock_vector();
     return i <= cv.value_for(rid);
   }
 

From 7db1d1e46e74c541e95cd302d8f783404860d00e Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Wed, 10 Dec 2025 21:11:56 +0100
Subject: [PATCH 06/20] Add thread start and thread exit to dependency relation

---
 .../mcmini/model/transitions/thread/thread_exit.hpp   |  1 +
 .../mcmini/model/transitions/thread/thread_start.hpp  | 11 ++++++-----
 src/mcmini/model_checking/algorithms/classic_dpor.cpp |  4 ++++
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/include/mcmini/model/transitions/thread/thread_exit.hpp b/include/mcmini/model/transitions/thread/thread_exit.hpp
index faa347f..daf8576 100644
--- a/include/mcmini/model/transitions/thread/thread_exit.hpp
+++ b/include/mcmini/model/transitions/thread/thread_exit.hpp
@@ -21,6 +21,7 @@ struct thread_exit : public model::transition {
     s.add_state_for_runner(executor, new thread(thread::exited));
     return status::exists;
   }
+  bool depends(const model::transition *t) const { return false; }
 
   std::string to_string() const override { return "exits"; }
 };
diff --git a/include/mcmini/model/transitions/thread/thread_start.hpp b/include/mcmini/model/transitions/thread/thread_start.hpp
index db9821e..ed4f1fa 100644
--- a/include/mcmini/model/transitions/thread/thread_start.hpp
+++ b/include/mcmini/model/transitions/thread/thread_start.hpp
@@ -7,19 +7,20 @@ namespace model {
 namespace transitions {
 
 struct thread_start : public model::transition {
- public:
+public:
   thread_start(state::runner_id_t executor) : transition(executor) {}
   ~thread_start() = default;
 
-  status modify(model::mutable_state& s) const override {
+  status modify(model::mutable_state &s) const override {
     // No modification necessary: we simply move into the next state
     using namespace model::objects;
-    auto* thread_state = s.get_state_of_runner<thread>(executor);
+    auto *thread_state = s.get_state_of_runner<thread>(executor);
     return thread_state->is_embryo() ? status::disabled : status::exists;
   }
+  bool depends(const model::transition *t) const { return false; }
 
   std::string to_string() const override { return "starts"; }
 };
 
-}  // namespace transitions
-}  // namespace model
+} // namespace transitions
+} // namespace model
diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index d05ca99..a790128 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -505,6 +505,10 @@ classic_dpor::dependency_relation_type classic_dpor::default_dependencies() {
       &transitions::thread_create::depends);
   dr.register_dd_entry<const transitions::thread_join>(
       &transitions::thread_join::depends);
+  dr.register_dd_entry<const transitions::thread_start>(
+      &transitions::thread_start::depends);
+  dr.register_dd_entry<const transitions::thread_exit>(
+      &transitions::thread_exit::depends);
   dr.register_dd_entry<const transitions::mutex_lock,
                        const transitions::mutex_init>(
       &transitions::mutex_lock::depends);

From 15f8b3a8c57cd787e359fac5a8408d1d7c2e0a46 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Wed, 10 Dec 2025 21:12:38 +0100
Subject: [PATCH 07/20] Add initial implementation of greedy relinearization

When exploring new traces, DPOR states that any exploration forward is
correct. When there are multiple enabled threads at any given point
which haven't been previously explored, DPOR can choose between any one
of them. Histotrically, McMini chose to schedule the thread with the
lowest id first before others. Recently, round-robin scheduling was
introduced that allowed McMini instead to fairly schedule threads for as
long as possible. The goal was to enable McMini to find shallower bugs
more quickly.

The challenge with round robin scheduling is that it produces traces
that are challenging to analyze. This is because a trace will
constantly be switching between threads to schedule making it difficult
for a user to see what's going on. The solution is to relinearize the
traces. The goal is to produce a new trace that obeys the same happens
before relation but which is more readable. There are two approaches to
doing this:

1. Choose the linearization that always schedules groups of threads for
   as long as possible (greedy)
2. Produce a linearization that minimizes the number of context switches
   a person must go through when analyzing the trace.

The latter is much more challenging (and possibly NP-hard although this
is only a hunch). The former is very easy.
---
 .../algorithms/classic_dpor.cpp               | 188 +++++++++++++++++-
 1 file changed, 184 insertions(+), 4 deletions(-)

diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index a790128..e403b64 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -68,6 +68,8 @@ struct classic_dpor::dpor_context {
     }
     return false;
   }
+  std::vector<const transition *> linearize_lowest_first();
+  std::vector<const transition *> linearize_greedy() { return {}; }
 };
 
 clock_vector classic_dpor::accumulate_max_clock_vector_against(
@@ -139,13 +141,10 @@ void classic_dpor::verify_using(coordinator &coordinator,
                  "incomplete. Rerun McMini with the "
                  "\"--max-depth-per-thread\" "
               << "flag for correct results.";
+          reached_max_depth = true;
         }
-        reached_max_depth = true;
         break;
       }
-      // NOTE: For deterministic results, always choose the "first" enabled
-      // runner. A runner precedes another runner in being enabled iff it has a
-      // smaller id.
       try {
         runner_id_t rid;
         switch (config.policy) {
@@ -559,3 +558,184 @@ classic_dpor::coenabled_relation_type classic_dpor::default_coenabledness() {
       &transitions::condition_variable_destroy::coenabled_with);
   return cr;
 }
+
+std::vector<const transition *>
+classic_dpor::dpor_context::linearize_lowest_first() {
+  if (this->stack.empty())
+    return {};
+
+  // N = number of _transitions_ in the stack
+  // Each element is one _state_, so there's one
+  // less transition
+  const size_t N = this->stack.size() - 1;
+
+  // --- Phase 1 ---
+  // Dependency Graph Construction
+  //
+  //
+  // `adj_list` holds the dependencies between every point in the trace. Nodes
+  // are representing using integers and correspond to the index in the
+  // transition stack.
+  //
+  // `e in adj_list[i] <--> happens_before(i, e)`.
+  //
+  // NOTE: For each `i`, the nodes are ordered in topological order. This is
+  // because the transitions in the stack are already topologically ordered by
+  // construction, and we process nodes in order.
+  std::vector<std::vector<int>> adj_list(N);
+  std::vector<std::vector<bool>> redundant(N);
+
+  for (size_t i = 0; i < N; i++) {
+    for (size_t j = i + 1; j < N; j++) {
+      if (happens_before(i, j)) {
+        adj_list[i].push_back(j);
+        redundant[i].push_back(true);
+      }
+    }
+  }
+
+  // --- Phase 2 ---
+  // Compute Chain Decomposition
+  //
+  // Decomposes the DAG into a minimum number of disjoint paths (chains).
+  std::vector<bool> unmarked(N, true);
+  std::vector<int> chain_id(N);  // chain_id[v]: index of the chain containing v
+  std::vector<std::list<int>> C; // C[h]: list of nodes in chain h
+
+  // Iterating in increasing topological order (see note above)
+  for (size_t v = 0; v < N; ++v) {
+    if (unmarked[v]) {
+      C.emplace_back(); // Start a new chain
+      int current_chain_id = C.size() - 1;
+      int current_node = v;
+
+      while (current_node != -1) {
+        C.back().push_back(current_node);
+        chain_id[current_node] = current_chain_id;
+        unmarked[current_node] = false;
+
+        int next_node = -1;
+        // Find the first unmarked neighbor 'w' (smallest topological rank)
+        for (int w : adj_list[current_node]) {
+          if (unmarked[w]) {
+            next_node = w;
+            break;
+          }
+        }
+        current_node = next_node;
+      }
+    }
+  }
+
+  // --- Phase 2: Compute Reachability and Redundancy ---
+  // reach[i][c]: min{j ; node j in C[c] and path i -> j exists}
+  // where "<" refers to topological order
+  //
+  // Intuitively, `reach[i][c]` denotes the "smallest" (topologically-speaking)
+  // node in chain `c` that has a path to node `i`.
+  const int num_chains = C.size();
+  const int INF = N + 1;
+  std::vector<std::vector<int>> reach(N, std::vector<int>(num_chains, INF));
+
+  // The key loop: iterates in DECREASING topological order
+  for (size_t k = 0; k <= N - 1; k++) {
+    size_t v = N - k - 1;
+    auto &reach_v = reach[v];
+
+    // Process outgoing edges of v (target 'w' is in INCREASING order)
+    for (int w : adj_list[v]) {
+      if (w < reach_v[chain_id[w]]) {
+        redundant[v][w] = false;
+
+        // Update reach[i] using reach[j]:
+        // If v can reach w via a non-redundant edge, v can reach everything j
+        // reaches.
+        for (int c = 0; c < num_chains; ++c)
+          reach_v[c] = std::min(reach_v[c], reach[w][c]);
+      }
+    }
+    reach_v[chain_id[v]] = v;
+  }
+
+  // --- Phase 3 ---
+  // Remove redundant edges from the adjacency list
+  for (size_t k = 0; k < N; k++) {
+    auto &out_edges = adj_list[k];
+    auto &redundant_edges = redundant[k];
+    size_t j = 0;
+    for (size_t i = 0; i < out_edges.size(); ++i)
+      if (redundant_edges[i])
+        out_edges[j++] = out_edges[i];
+    out_edges.resize(j);
+  }
+
+  // --- Phase 4 ---
+  // Topological Sort and Final Processing
+  // Generate a topological sort using the newly reduced dependency graph
+  std::vector<int> linearization;
+  std::vector<int> ready_set; // Indicies into the transition stack
+  std::vector<int> in_degree(N, 0);
+  for (size_t u = 0; u < N; ++u)
+    for (int v : adj_list[u])
+      in_degree[v]++;
+
+  for (size_t i = 0; i < N; ++i)
+    if (in_degree[i] == 0)
+      ready_set.push_back(i);
+
+  runner_id_t last_rid = -1; // -1 indicates no last rid
+  while (!ready_set.empty()) {
+    int next_vertex = -1;
+    int selected_index = -1;
+
+    // Find the vertex with the same executor as the last one
+    if (last_rid != -1) {
+      for (size_t i = 0; i < ready_set.size(); ++i) {
+        const runner_id_t r =
+            stack.at(ready_set[i]).get_out_transition()->get_executor();
+        if (r == last_rid) {
+          next_vertex = ready_set[i];
+          selected_index = i;
+          break; // Found the best greedy match that avoids inversion
+        }
+      }
+    }
+
+    // If no color match, or at the start, pick the thread with the lowest id
+    if (next_vertex == -1) {
+      // INVARIANT: Since mid_rid
+      runner_id_t min_rid = RID_INVALID;
+      for (size_t i = 0; i < ready_set.size(); ++i) {
+        const runner_id_t r =
+            stack.at(ready_set[i]).get_out_transition()->get_executor();
+        if (r < min_rid) {
+          next_vertex = ready_set[i];
+          selected_index = i;
+        }
+      }
+    }
+
+    linearization.push_back(next_vertex);
+    last_rid = stack.at(next_vertex).get_out_transition()->get_executor();
+
+    // Remove the selected vertex from the ready set
+    // Swap with the back and pop for O(1) removal from vector (since order in S
+    // doesn't matter)
+    std::swap(ready_set[selected_index], ready_set.back());
+    ready_set.pop_back();
+
+    for (int v : adj_list[next_vertex]) {
+      in_degree[v]--;
+      if (in_degree[v] == 0) {
+        ready_set.push_back(v);
+      }
+    }
+  }
+
+  // --- Phase 5 ---
+  // Convert the linearization into a transition trace
+  std::vector<const transition *> linearized_trace(N);
+  for (size_t i = 0; i < N; i++)
+    linearized_trace[i] = stack.at(linearization[i]).get_out_transition();
+  return linearized_trace;
+}
\ No newline at end of file

From 5caf740618f1fc23a458307345998fdbf862da40 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Thu, 11 Dec 2025 01:11:15 +0100
Subject: [PATCH 08/20] Fix clock vector aggregation

The same bug that affected clock vectors when computing "happens-before"
also plagued the aggregation function when computing the maximum clock
vector over all dependent transitions in the transition stack. The
problem is the same as before: the appropriate vector clock is stored
in the state _after_, not the same state (the `i`th transition has its
per-transition clock vector stored in state `(i + 1)`.)
---
 .../algorithms/classic_dpor/stack_item.hpp    |  6 ++--
 .../algorithms/classic_dpor.cpp               | 29 ++++++++++++++-----
 2 files changed, 24 insertions(+), 11 deletions(-)

diff --git a/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp b/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp
index fd5f2a6..ec3e3d0 100644
--- a/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp
+++ b/include/mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp
@@ -219,9 +219,9 @@ struct stack_item final {
     return backtrack_thread;
   }
 
-  clock_vector get_clock_vector() const { return this->cv; }
-  const std::array<runner_item, MAX_TOTAL_THREADS_IN_PROGRAM>
-      &get_per_runner_clocks() const {
+  const clock_vector &get_clock_vector() const { return this->cv; }
+  const std::array<runner_item, MAX_TOTAL_THREADS_IN_PROGRAM> &
+  get_per_runner_clocks() const {
     return this->per_runner_clocks;
   }
   runner_id_t get_first_enabled_runner() const {
diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index e403b64..e235656 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -42,14 +42,28 @@ struct classic_dpor::dpor_context {
 
   dpor_context(::coordinator &c) : coordinator(c) {}
 
+public:
+  const size_t state_stack_size() const { return stack.size(); }
+  const size_t transition_stack_size() const {
+    size_t ss = state_stack_size();
+    return ss > 1 ? (ss - 1) : 0;
+  }
+
   const transition *get_transition(int i) const {
     return stack.at(i).get_out_transition();
   }
 
+  const clock_vector &clock(size_t j) const {
+    // C(j) in the DPOR paper
+    // NOTE: The clock vector for the `i`th transition is stored in the state
+    // into which the transition points, NOT the state from which the transition
+    // starts (hence the j + 1)
+    return stack.at(j + 1).get_clock_vector();
+  }
+
   bool happens_before(size_t i, size_t j) const {
-    const runner_id_t rid = get_transition(i)->get_executor();
-    const clock_vector &cv = stack.at(j + 1).get_clock_vector();
-    return i <= cv.value_for(rid);
+    const runner_id_t procSi = get_transition(i)->get_executor();
+    return i <= clock(j).value_for(procSi);
   }
 
   bool happens_before_thread(size_t i, runner_id_t p) const {
@@ -79,11 +93,10 @@ clock_vector classic_dpor::accumulate_max_clock_vector_against(
   // (case-sensitive) in the paper, viz. the transition between states `s_i` and
   // `s_{i+1}`.
   clock_vector result;
-  for (const stack_item &s_i : context.stack) {
-    if (s_i.get_out_transition() != nullptr &&
-        this->are_dependent(*s_i.get_out_transition(), t)) {
-      result = clock_vector::max(result, s_i.get_clock_vector());
-    }
+  for (size_t i = 0; i < context.transition_stack_size(); i++) {
+    const model::transition *S_i = context.get_transition(i);
+    if (this->are_dependent(*S_i, t))
+      result = clock_vector::max(result, context.clock(i));
   }
   return result;
 }

From 409ff475ab650054dd880a348fedc4da8ce859bf Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Thu, 11 Dec 2025 01:13:42 +0100
Subject: [PATCH 09/20] Fix subtle dependency issue in ddt

The double dispatch table has two means of handling functions: either a
single interface exists that applies to all other instances, or else a
specific function exists overriding a specific dependency pairing. The
goal is to enable some operations to apply a uniform rule regardless of
the other transition we're comparing to (e.g. a thread start is
independent of everything, and instead of needing to specify N functions
one for each other kind of operation we can instead specify it once).
There was an edge case in which comparison with a type which has
registered _other_ specific handlers resulted in the global handlers not
being called. This happened because we didn't subsequently check if a
global function existed if the pairing failed.
---
 include/mcmini/misc/ddt.hpp | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/include/mcmini/misc/ddt.hpp b/include/mcmini/misc/ddt.hpp
index f8db347..e7500bb 100644
--- a/include/mcmini/misc/ddt.hpp
+++ b/include/mcmini/misc/ddt.hpp
@@ -155,20 +155,21 @@ struct double_dispatch_member_function_table<InterfaceType,
                        unspecified_callback_handle);
   }
 
-  ReturnType call_or(ReturnType fallback, InterfaceType* t1, InterfaceType* t2,
+  ReturnType call_or(ReturnType fallback, InterfaceType *t1, InterfaceType *t2,
                      Args... args) const {
     const auto t1_type = std::type_index(typeid(*t1));
     const auto t2_type = std::type_index(typeid(*t2));
     if (internal_table.count(t1_type) > 0) {
       if (internal_table.at(t1_type).count(t2_type) > 0) {
-        const auto& pair = internal_table.at(t1_type).at(t2_type);
+        const auto &pair = internal_table.at(t1_type).at(t2_type);
         return pair.first(t1, t2, pair.second, std::forward<Args>(args)...);
       }
-    } else if (interface_member_function_table.count(t1_type) > 0) {
-      const auto& pair = interface_member_function_table.at(t1_type);
+    }
+    if (interface_member_function_table.count(t1_type) > 0) {
+      const auto &pair = interface_member_function_table.at(t1_type);
       return pair.first(t1, t2, pair.second, std::forward<Args>(args)...);
     } else if (interface_member_function_table.count(t2_type) > 0) {
-      const auto& pair = interface_member_function_table.at(t2_type);
+      const auto &pair = interface_member_function_table.at(t2_type);
       // NOTE: t2 should come before t1 here since
       // `casting_function_interface_table` always casts its first argument
       return pair.first(t2, t1, pair.second, std::forward<Args>(args)...);
@@ -176,12 +177,12 @@ struct double_dispatch_member_function_table<InterfaceType,
     return fallback;
   }
 
-  ReturnType call(InterfaceType* t1, InterfaceType* t2, Args... args) const {
+  ReturnType call(InterfaceType *t1, InterfaceType *t2, Args... args) const {
     const auto t1_type = std::type_index(typeid(*t1));
     const auto t2_type = std::type_index(typeid(*t2));
     if (internal_table.count(t1_type) > 0) {
       if (internal_table.at(t1_type).count(t2_type) > 0) {
-        const auto& pair = internal_table.at(t1_type).at(t2_type);
+        const auto &pair = internal_table.at(t1_type).at(t2_type);
         return pair.first(t1, t2, pair.second, std::forward(args)...);
       }
     }

From c9bdf9fb17c09095a3570ffdc7e58f88246e5503 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Thu, 11 Dec 2025 01:19:55 +0100
Subject: [PATCH 10/20] Simplify dependencies

---
 .../algorithms/classic_dpor.cpp               | 91 ++++++++-----------
 1 file changed, 40 insertions(+), 51 deletions(-)

diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index e235656..0b92ff5 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -513,62 +513,51 @@ bool classic_dpor::dynamically_update_backtrack_sets_at_index(
 
 classic_dpor::dependency_relation_type classic_dpor::default_dependencies() {
   classic_dpor::dependency_relation_type dr;
-  dr.register_dd_entry<const transitions::thread_create>(
-      &transitions::thread_create::depends);
-  dr.register_dd_entry<const transitions::thread_join>(
-      &transitions::thread_join::depends);
-  dr.register_dd_entry<const transitions::thread_start>(
-      &transitions::thread_start::depends);
-  dr.register_dd_entry<const transitions::thread_exit>(
-      &transitions::thread_exit::depends);
-  dr.register_dd_entry<const transitions::mutex_lock,
-                       const transitions::mutex_init>(
-      &transitions::mutex_lock::depends);
-  dr.register_dd_entry<const transitions::mutex_lock,
-                       const transitions::mutex_lock>(
-      &transitions::mutex_lock::depends);
-  dr.register_dd_entry<const transitions::condition_variable_wait,
-                       const transitions::condition_variable_init>(
-      &transitions::condition_variable_wait::depends);
-  dr.register_dd_entry<const transitions::condition_variable_wait,
-                       const transitions::mutex_lock>(
-      &transitions::condition_variable_wait::depends);
-  dr.register_dd_entry<const transitions::condition_variable_signal,
-                       const transitions::condition_variable_wait>(
-      &transitions::condition_variable_signal::depends);
-  dr.register_dd_entry<const transitions::condition_variable_signal,
-                       const transitions::mutex_lock>(
-      &transitions::condition_variable_signal::depends);
+  using namespace transitions;
+  dr.register_dd_entry<const thread_create>(&thread_create::depends);
+  dr.register_dd_entry<const thread_join>(&thread_join::depends);
+  dr.register_dd_entry<const thread_start>(&thread_start::depends);
+  dr.register_dd_entry<const thread_exit>(&thread_exit::depends);
+  dr.register_dd_entry<const mutex_lock, const mutex_init>(
+      &mutex_lock::depends);
+  dr.register_dd_entry<const mutex_lock, const mutex_lock>(
+      &mutex_lock::depends);
+  dr.register_dd_entry<const condition_variable_wait,
+                       const condition_variable_init>(
+      &condition_variable_wait::depends);
+  dr.register_dd_entry<const condition_variable_wait, const mutex_lock>(
+      &condition_variable_wait::depends);
+  dr.register_dd_entry<const condition_variable_signal,
+                       const condition_variable_wait>(
+      &condition_variable_signal::depends);
+  dr.register_dd_entry<const condition_variable_signal, const mutex_lock>(
+      &condition_variable_signal::depends);
   return dr;
 }
 
 classic_dpor::coenabled_relation_type classic_dpor::default_coenabledness() {
+  using namespace transitions;
   classic_dpor::dependency_relation_type cr;
-  cr.register_dd_entry<const transitions::thread_create>(
-      &transitions::thread_create::coenabled_with);
-  cr.register_dd_entry<const transitions::thread_join>(
-      &transitions::thread_join::coenabled_with);
-  cr.register_dd_entry<const transitions::mutex_lock,
-                       const transitions::mutex_unlock>(
-      &transitions::mutex_lock::coenabled_with);
-  cr.register_dd_entry<const transitions::condition_variable_signal,
-                       const transitions::condition_variable_wait>(
-      &transitions::condition_variable_signal::coenabled_with);
-  cr.register_dd_entry<const transitions::condition_variable_signal,
-                       const transitions::mutex_unlock>(
-      &transitions::condition_variable_signal::coenabled_with);
-  cr.register_dd_entry<const transitions::condition_variable_broadcast,
-                       const transitions::condition_variable_wait>(
-      &transitions::condition_variable_broadcast::coenabled_with);
-  cr.register_dd_entry<const transitions::condition_variable_broadcast,
-                       const transitions::mutex_unlock>(
-      &transitions::condition_variable_broadcast::coenabled_with);
-  cr.register_dd_entry<const transitions::condition_variable_destroy,
-                       const transitions::condition_variable_wait>(
-      &transitions::condition_variable_destroy::coenabled_with);
-  cr.register_dd_entry<const transitions::condition_variable_destroy,
-                       const transitions::condition_variable_signal>(
-      &transitions::condition_variable_destroy::coenabled_with);
+  cr.register_dd_entry<const thread_create>(&thread_create::coenabled_with);
+  cr.register_dd_entry<const thread_join>(&thread_join::coenabled_with);
+  cr.register_dd_entry<const mutex_lock, const mutex_unlock>(
+      &mutex_lock::coenabled_with);
+  cr.register_dd_entry<const condition_variable_signal,
+                       const condition_variable_wait>(
+      &condition_variable_signal::coenabled_with);
+  cr.register_dd_entry<const condition_variable_signal, const mutex_unlock>(
+      &condition_variable_signal::coenabled_with);
+  cr.register_dd_entry<const condition_variable_broadcast,
+                       const condition_variable_wait>(
+      &condition_variable_broadcast::coenabled_with);
+  cr.register_dd_entry<const condition_variable_broadcast, const mutex_unlock>(
+      &condition_variable_broadcast::coenabled_with);
+  cr.register_dd_entry<const condition_variable_destroy,
+                       const condition_variable_wait>(
+      &condition_variable_destroy::coenabled_with);
+  cr.register_dd_entry<const condition_variable_destroy,
+                       const condition_variable_signal>(
+      &condition_variable_destroy::coenabled_with);
   return cr;
 }
 

From 513175c5aed936d5dfd105d299ace95326aa8dc2 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Thu, 11 Dec 2025 01:21:20 +0100
Subject: [PATCH 11/20] Finalize greedy linearization function

---
 .../algorithms/classic_dpor.cpp               | 57 +++++++++++++------
 1 file changed, 39 insertions(+), 18 deletions(-)

diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index 0b92ff5..afb6c55 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -415,7 +415,8 @@ void classic_dpor::dynamically_update_backtrack_sets(dpor_context &context) {
       coordinator.get_current_program_model().get_num_runners();
 
   std::set<runner_id_t> thread_ids;
-  for (runner_id_t i = 0; i < num_threads; i++) thread_ids.insert(i);
+  for (runner_id_t i = 0; i < num_threads; i++)
+    thread_ids.insert(i);
 
   const ssize_t t_stack_top = (ssize_t)(context.stack.size()) - 2;
   const runner_id_t last_runner_to_execute =
@@ -463,7 +464,8 @@ void classic_dpor::dynamically_update_backtrack_sets(dpor_context &context) {
        * will be the maxmimum `i` since we're searching
        * backwards
        */
-      if (should_stop) break;
+      if (should_stop)
+        break;
     }
   }
 }
@@ -501,7 +503,8 @@ bool classic_dpor::dynamically_update_backtrack_sets_at_index(
         // in the set E, chose that thread to backtrack
         // on. This is equivalent to not having to do
         // anything
-        if (pre_si.backtrack_set_contains(q)) return true;
+        if (pre_si.backtrack_set_contains(q))
+          return true;
       }
 
       // Otherwise select an arbitrary thread to backtrack upon.
@@ -642,21 +645,21 @@ classic_dpor::dpor_context::linearize_lowest_first() {
   // The key loop: iterates in DECREASING topological order
   for (size_t k = 0; k <= N - 1; k++) {
     size_t v = N - k - 1;
-    auto &reach_v = reach[v];
 
     // Process outgoing edges of v (target 'w' is in INCREASING order)
-    for (int w : adj_list[v]) {
-      if (w < reach_v[chain_id[w]]) {
-        redundant[v][w] = false;
+    for (size_t i = 0; i < adj_list[v].size(); i++) {
+      const int w = adj_list[v][i];
+      if (w < reach[v][chain_id[w]]) {
+        redundant[v][i /* INDEX of w */] = false;
 
         // Update reach[i] using reach[j]:
         // If v can reach w via a non-redundant edge, v can reach everything j
         // reaches.
         for (int c = 0; c < num_chains; ++c)
-          reach_v[c] = std::min(reach_v[c], reach[w][c]);
+          reach[v][c] = std::min(reach[v][c], reach[w][c]);
       }
     }
-    reach_v[chain_id[v]] = v;
+    reach[v][chain_id[v]] = v;
   }
 
   // --- Phase 3 ---
@@ -664,13 +667,32 @@ classic_dpor::dpor_context::linearize_lowest_first() {
   for (size_t k = 0; k < N; k++) {
     auto &out_edges = adj_list[k];
     auto &redundant_edges = redundant[k];
+    assert(out_edges.size() == redundant_edges.size());
     size_t j = 0;
     for (size_t i = 0; i < out_edges.size(); ++i)
-      if (redundant_edges[i])
+      if (!redundant_edges[i])
         out_edges[j++] = out_edges[i];
     out_edges.resize(j);
   }
 
+#if DEBUG
+  // Validation: every point in the adjacency list happens before
+  for (size_t i = 0; i < N; i++)
+    for (size_t j = i + 1; j < N; j++)
+      if (std::find(adj_list[i].begin(), adj_list[i].end(), j) !=
+          adj_list[i].end()) {
+        assert(happens_before(i, j));
+      } else {
+        if (happens_before(i, j)) {
+
+          auto s = std::find_if(adj_list[i].begin(), adj_list[i].end(),
+                                [&](int w) { return happens_before(w, j); });
+          assert(s != adj_list[i].end());
+        }
+        // Not in adj so ok in `false` case
+      }
+#endif
+
   // --- Phase 4 ---
   // Topological Sort and Final Processing
   // Generate a topological sort using the newly reduced dependency graph
@@ -685,16 +707,15 @@ classic_dpor::dpor_context::linearize_lowest_first() {
     if (in_degree[i] == 0)
       ready_set.push_back(i);
 
-  runner_id_t last_rid = -1; // -1 indicates no last rid
+  runner_id_t last_rid = RUNNER_ID_MAX; // -1 indicates no last rid
   while (!ready_set.empty()) {
     int next_vertex = -1;
     int selected_index = -1;
 
     // Find the vertex with the same executor as the last one
-    if (last_rid != -1) {
+    if (last_rid != RUNNER_ID_MAX) {
       for (size_t i = 0; i < ready_set.size(); ++i) {
-        const runner_id_t r =
-            stack.at(ready_set[i]).get_out_transition()->get_executor();
+        const runner_id_t r = get_transition(ready_set[i])->get_executor();
         if (r == last_rid) {
           next_vertex = ready_set[i];
           selected_index = i;
@@ -708,11 +729,11 @@ classic_dpor::dpor_context::linearize_lowest_first() {
       // INVARIANT: Since mid_rid
       runner_id_t min_rid = RID_INVALID;
       for (size_t i = 0; i < ready_set.size(); ++i) {
-        const runner_id_t r =
-            stack.at(ready_set[i]).get_out_transition()->get_executor();
+        const runner_id_t r = get_transition(ready_set[i])->get_executor();
         if (r < min_rid) {
           next_vertex = ready_set[i];
           selected_index = i;
+          min_rid = r;
         }
       }
     }
@@ -736,8 +757,8 @@ classic_dpor::dpor_context::linearize_lowest_first() {
 
   // --- Phase 5 ---
   // Convert the linearization into a transition trace
-  std::vector<const transition *> linearized_trace(N);
+  std::vector<const transition *> linearized_trace(N, nullptr);
   for (size_t i = 0; i < N; i++)
-    linearized_trace[i] = stack.at(linearization[i]).get_out_transition();
+    linearized_trace[i] = get_transition(linearization[i]);
   return linearized_trace;
 }
\ No newline at end of file

From 792f9da313278b8d0f82f5938330931969ee9b60 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Thu, 11 Dec 2025 02:35:48 +0100
Subject: [PATCH 12/20] Add `verbose` and ``quiet-program-output` flags

---
 include/mcmini/model/config.hpp | 11 +++++++++++
 src/mcmini/mcmini.cpp           | 13 ++++++++++++-
 2 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/include/mcmini/model/config.hpp b/include/mcmini/model/config.hpp
index 5ce48c4..e9de31e 100644
--- a/include/mcmini/model/config.hpp
+++ b/include/mcmini/model/config.hpp
@@ -52,6 +52,17 @@ struct config {
    */
   bool use_multithreaded_fork = false;
 
+  /**
+   * Whether to print every trace, or one those that cause a bug
+   */
+  bool verbose = false;
+
+  /**
+   * Whether the STDOUT/STDERR of the program is sent to /dev/null during
+   * execution
+   */
+  bool quiet_program_output = false;
+
   /**
    * The time between consecutive checkpoint images when `libmcmini.so` is
    * running in record mode.
diff --git a/src/mcmini/mcmini.cpp b/src/mcmini/mcmini.cpp
index 47b2876..ec35d4c 100644
--- a/src/mcmini/mcmini.cpp
+++ b/src/mcmini/mcmini.cpp
@@ -200,7 +200,8 @@ void do_model_checking(const config& config) {
                          : mcconfig::exploration_policy::smallest_first;
 
   model_checking::classic_dpor classic_dpor_checker(std::move(mc_config));
-  c.trace_completed = &finished_trace_classic_dpor;
+  if (config.verbose)
+    c.trace_completed = &finished_trace_classic_dpor;
   c.deadlock = &found_deadlock;
   c.undefined_behavior = &found_undefined_behavior;
   c.abnormal_termination = &found_abnormal_termination;
@@ -448,6 +449,14 @@ int main_cpp(int argc, const char** argv) {
                strcmp(cur_arg[0], "-mtf") == 0) {
       mcmini_config.use_multithreaded_fork = true;
       cur_arg++;
+    } else if (strcmp(cur_arg[0], "--verbose") == 0 ||
+               strcmp(cur_arg[0], "-v") == 0) {
+      mcmini_config.verbose = true;
+      cur_arg++;
+    } else if (strcmp(cur_arg[0], "--quiet-program-output") == 0 ||
+               strcmp(cur_arg[0], "-q") == 0) {
+      mcmini_config.quiet_program_output = true;
+      cur_arg++;
     } else if (cur_arg[0][1] == 'm' && isdigit(cur_arg[0][2])) {
       mcmini_config.max_thread_execution_depth =
           strtoul(cur_arg[1], nullptr, 10);
@@ -481,6 +490,8 @@ int main_cpp(int argc, const char** argv) {
           "              [--first-deadlock|--first|-f]\n"
           "              [--round-robin|-rr]\n"
           "              [--log-level|-log <level>]\n"
+          "              [--verbose|-v]\n"
+          "              [--quiet-program-output|-q]\n"
           "              [--help|-h]\n"
           "              target_executable\n");
       exit(1);

From 9a65d0f5e3c5bc83ba4c8d7d5d8a5739bb4e84eb Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Wed, 17 Dec 2025 23:30:39 +0100
Subject: [PATCH 13/20] Approaching implementation for optimal paths

---
 .../algorithms/classic_dpor.cpp               | 516 ++++++++++++++++--
 1 file changed, 464 insertions(+), 52 deletions(-)

diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index afb6c55..2b7d43a 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -1,7 +1,4 @@
-#include "mcmini/model_checking/algorithms/classic_dpor.hpp"
-
-#include <sys/types.h>
-
+#include <algorithm>
 #include <array>
 #include <cassert>
 #include <csignal>
@@ -11,9 +8,16 @@
 #include <set>
 #include <stdexcept>
 #include <string>
+#include <sys/types.h>
 #include <unordered_set>
 #include <vector>
 
+#ifndef MCMINI_USE_SCIP
+#include "scip/scip.h"
+#include "scip/scipdefplugins.h"
+#include <numeric>
+#endif
+
 #include "mcmini/coordinator/coordinator.hpp"
 #include "mcmini/defines.h"
 #include "mcmini/log/logger.hpp"
@@ -25,6 +29,7 @@
 #include "mcmini/model/transitions/mutex/mutex_init.hpp"
 #include "mcmini/model/transitions/semaphore/callbacks.hpp"
 #include "mcmini/model/transitions/thread/callbacks.hpp"
+#include "mcmini/model_checking/algorithms/classic_dpor.hpp"
 #include "mcmini/model_checking/algorithms/classic_dpor/clock_vector.hpp"
 #include "mcmini/model_checking/algorithms/classic_dpor/runner_item.hpp"
 #include "mcmini/model_checking/algorithms/classic_dpor/stack_item.hpp"
@@ -45,14 +50,22 @@ struct classic_dpor::dpor_context {
 public:
   const size_t state_stack_size() const { return stack.size(); }
   const size_t transition_stack_size() const {
-    size_t ss = state_stack_size();
-    return ss > 1 ? (ss - 1) : 0;
+    const size_t ss = state_stack_size();
+    return ss > 0 ? (ss - 1) : 0;
   }
 
   const transition *get_transition(int i) const {
     return stack.at(i).get_out_transition();
   }
 
+  const transition *get_transition(size_t i) const {
+    return stack.at(i).get_out_transition();
+  }
+
+  const runner_id_t tid(size_t i) const {
+    return get_transition(i)->get_executor();
+  }
+
   const clock_vector &clock(size_t j) const {
     // C(j) in the DPOR paper
     // NOTE: The clock vector for the `i`th transition is stored in the state
@@ -82,8 +95,9 @@ struct classic_dpor::dpor_context {
     }
     return false;
   }
-  std::vector<const transition *> linearize_lowest_first();
-  std::vector<const transition *> linearize_greedy() { return {}; }
+  std::vector<std::vector<size_t>> transitive_reduction() const;
+  std::vector<const transition *> linearize_lowest_first() const;
+  std::vector<const transition *> linearize_optimal() const;
 };
 
 clock_vector classic_dpor::accumulate_max_clock_vector_against(
@@ -146,7 +160,7 @@ void classic_dpor::verify_using(coordinator &coordinator,
         if (!reached_max_depth) {
           log_unexpected(dpor_logger)
               << "*** Execution Limit Reached! ***\n\n"
-              << "McMini encountered a trace with" << dpor_stack.size()
+              << "McMini encountered a trace with " << dpor_stack.size()
               << " transitions which is the most that McMini was configured"
               << " to handle in any given trace ("
               << this->config.maximum_total_execution_depth
@@ -202,6 +216,12 @@ void classic_dpor::verify_using(coordinator &coordinator,
         }
 
         this->continue_dpor_by_expanding_trace_with(rid, context);
+        log_info(dpor_logger)
+            << context.coordinator.get_current_program_model();
+        auto lin = context.linearize_optimal();
+        for (auto *t : lin) {
+          log_info(dpor_logger) << t->debug_string();
+        }
         model_checking_stats.total_transitions++;
 
         // Now ask the question: will the next operation of this thread
@@ -564,30 +584,41 @@ classic_dpor::coenabled_relation_type classic_dpor::default_coenabledness() {
   return cr;
 }
 
-std::vector<const transition *>
-classic_dpor::dpor_context::linearize_lowest_first() {
+std::vector<std::vector<size_t>>
+classic_dpor::dpor_context::transitive_reduction() const {
+  // This code is heavily inspired by the code in the LEDA library
+  // (https://leda.uni-trier.de), specifically the
+  // `LEDA-7.2.2/src/graph/graph_alg/_transclosure.cpp`
+  //
+  // The transitive reduction R of a digraph G is the graph of the fewest arcs
+  // such that a path exists between nodes u and v in G iff a path exists
+  // between u and v in R. Essentially, it's the smallest graph with the same
+  // dependency relation of G.
+  //
+  // In our case, we're considering a trace T := t1, t2, ..., tN of `N`
+  // total transitions. Each transition can be thought of as a node in a digraph
+  // with the edges representing "happens-before" dependencies between them. The
+  // transitive reduction of this digraph then represents those transitions in
+  // an "immediate" race: ti --> tj and for all transitions tk in-between,
+  // either ti --/--> tk or tk --/-->tj.
   if (this->stack.empty())
     return {};
+  const size_t N = this->transition_stack_size();
+  const size_t INF = N + 1;
 
-  // N = number of _transitions_ in the stack
-  // Each element is one _state_, so there's one
-  // less transition
-  const size_t N = this->stack.size() - 1;
-
-  // --- Phase 1 ---
-  // Dependency Graph Construction
-  //
-  //
   // `adj_list` holds the dependencies between every point in the trace. Nodes
   // are representing using integers and correspond to the index in the
   // transition stack.
   //
   // `e in adj_list[i] <--> happens_before(i, e)`.
   //
+  // `redundant[i][j] <---> adj_list[i][j] can be removed in the transition
+  // reduction`
+  //
   // NOTE: For each `i`, the nodes are ordered in topological order. This is
   // because the transitions in the stack are already topologically ordered by
   // construction, and we process nodes in order.
-  std::vector<std::vector<int>> adj_list(N);
+  std::vector<std::vector<size_t>> adj_list(N);
   std::vector<std::vector<bool>> redundant(N);
 
   for (size_t i = 0; i < N; i++) {
@@ -599,29 +630,33 @@ classic_dpor::dpor_context::linearize_lowest_first() {
     }
   }
 
-  // --- Phase 2 ---
   // Compute Chain Decomposition
   //
   // Decomposes the DAG into a minimum number of disjoint paths (chains).
+  //
+  //  chain_id[v]: index of the chain containing v
+  //  C[h]: list of nodes in chain h
+  //
+  // See Dilworth's theorem.
   std::vector<bool> unmarked(N, true);
-  std::vector<int> chain_id(N);  // chain_id[v]: index of the chain containing v
-  std::vector<std::list<int>> C; // C[h]: list of nodes in chain h
+  std::vector<size_t> chain_id(N);
+  std::vector<std::list<size_t>> C;
 
   // Iterating in increasing topological order (see note above)
   for (size_t v = 0; v < N; ++v) {
     if (unmarked[v]) {
       C.emplace_back(); // Start a new chain
-      int current_chain_id = C.size() - 1;
-      int current_node = v;
+      size_t current_chain_id = C.size() - 1;
+      size_t current_node = v;
 
-      while (current_node != -1) {
+      while (current_node != INF) {
         C.back().push_back(current_node);
         chain_id[current_node] = current_chain_id;
         unmarked[current_node] = false;
 
-        int next_node = -1;
         // Find the first unmarked neighbor 'w' (smallest topological rank)
-        for (int w : adj_list[current_node]) {
+        size_t next_node = INF;
+        for (size_t w : adj_list[current_node]) {
           if (unmarked[w]) {
             next_node = w;
             break;
@@ -632,14 +667,15 @@ classic_dpor::dpor_context::linearize_lowest_first() {
     }
   }
 
-  // --- Phase 2: Compute Reachability and Redundancy ---
-  // reach[i][c]: min{j ; node j in C[c] and path i -> j exists}
+  // Compute Reachability and Redundancy
+  //
+  // reach[i][c] = min{j ; node j in C[c] and path i -> j exists}
+  //
   // where "<" refers to topological order
   //
   // Intuitively, `reach[i][c]` denotes the "smallest" (topologically-speaking)
-  // node in chain `c` that has a path to node `i`.
+  // node in chain `c` to which `i` has a path.
   const int num_chains = C.size();
-  const int INF = N + 1;
   std::vector<std::vector<int>> reach(N, std::vector<int>(num_chains, INF));
 
   // The key loop: iterates in DECREASING topological order
@@ -652,7 +688,6 @@ classic_dpor::dpor_context::linearize_lowest_first() {
       if (w < reach[v][chain_id[w]]) {
         redundant[v][i /* INDEX of w */] = false;
 
-        // Update reach[i] using reach[j]:
         // If v can reach w via a non-redundant edge, v can reach everything j
         // reaches.
         for (int c = 0; c < num_chains; ++c)
@@ -662,7 +697,6 @@ classic_dpor::dpor_context::linearize_lowest_first() {
     reach[v][chain_id[v]] = v;
   }
 
-  // --- Phase 3 ---
   // Remove redundant edges from the adjacency list
   for (size_t k = 0; k < N; k++) {
     auto &out_edges = adj_list[k];
@@ -692,27 +726,408 @@ classic_dpor::dpor_context::linearize_lowest_first() {
         // Not in adj so ok in `false` case
       }
 #endif
+  return adj_list;
+}
 
-  // --- Phase 4 ---
-  // Topological Sort and Final Processing
-  // Generate a topological sort using the newly reduced dependency graph
-  std::vector<int> linearization;
-  std::vector<int> ready_set; // Indicies into the transition stack
+std::vector<const transition *>
+classic_dpor::dpor_context::linearize_optimal() const {
+#ifndef MCMINI_USE_SCIP
+  // Given a fixed trace `T` of `N` transitions and a happens-before relation
+  // `happens-before_T: [1, N] x [1, N] -> {0, 1}` over the indices of `T`, the
+  // goal is to produce a new trace `T'` such that `happens-before_T(i, j) =
+  // happens-before_T'(i, j)` and such that the number of inversions is
+  // minimized. An inversion is a point in the trace where the thread ID of the
+  // `i`th transition doesn't match the thread ID of the `(i + 1)`th transition.
+  //
+  // The intuition in producing such a trace `T'` is that reasoning about this
+  // trace is "easier" than any other because the number of context switches
+  // (inversions) a user must perform to analyze a new trace is minimized.
+  // Moreover, since `T'` obeys the same "happens-before" relation as the
+  // original trace `T`, it produces the exact same bug.
+  //
+  // We can map relinearization into a graph problem. Let `Tids := {tid : exists
+  // i, T[i]->get_executor() = tid }`. We construct an unweighted, labeled
+  // digraph `K` where
+  //
+  //    1. V(K) := {1, 2, ..., N}
+  //    2. E(K) := {(i, j) in [1, N] x [1, N] : happens-before_T(i, j)}
+  //    3. tid : V -> Tids, tid(v) := T[v].get_executor()
+  //
+  // Since `happens-before_T` is transitive, we note that `K =
+  // Transitive-Closure(K)` since `happens-before_T` is transitive. Moreover,
+  // the array `[1, 2, ..., N]` is a valid topological sorting of `K` since `i >
+  // j --> happens-before_T(i, j) = 0`.
+  //
+  // An equivalent formulation of the problem is to find a topological sorting
+  // of K of minimal inversions. Computing such a minimal topological sort can
+  // be reduced to the sequential ordering problem (SOP) (see
+  // https://people.idsia.ch/~roberto/SOP.pdf for a reference). The SOP problem
+  // is related to the Asymmetric Traveling Salesperson Problem (ATSP). In the
+  // ATSP, the goal is to find a Hamiltonian Cycle in a weighted directed graph
+  // of minimal weight. SOP adds one more constraint and requires that certain
+  // nodes are visited before others based on a relation `R` over the vertices.
+  //
+  // We construct a new graph `G` from `K`. Here, we
+  // note that although the SOP problem and ATSP problems work with cycles, we
+  // can add a source and sink node to our DAG with zero weight edges between
+  // each other and the respective start and end nodes of the digraph (those
+  // with in-degree and out-degree equalt to 0 respectively) to map exactly to
+  // the SOP problem.
+  //
+  // Denote `H := Transitive-Reduction(K)`. Recall each node `v` in `K` and by
+  // proxy `H` corresponds to a transition in the transition stack `T`. Let
+  // `tid(v)` denote the labeling function of `K`. Then let
+  //
+  //    1. V(G) := V(H) + {source, sink}
+  //    2. E(G) := V(H) x V(H) + {(u, sink) : u in V(H), out-degree[u] = 0} +
+  //    {(source, u) : u in V(H), in-degree[u] = 0}}
+  //    3. For all e = (u, v) in E(G),
+  //
+  //       w(e) := if tid(u) == tid(v) || (u == source) || (v == sink) then 0
+  //       else 1
+  //
+  // Let `C := SOP(G, E(H))` denote the Hamiltonian Cycle of minimum weight
+  // subjet to `E(H)`. Then `C := m_1, m_2, ..., m_N` corresponds to the minimal
+  // topological sorting. Clearly, `C` is a valid topological sorting since it
+  // contains all nodes of `H` and in an order obeying `E(H)`. By construction,
+  // the total weight of `C` equals the number of inversions in `C`, since an
+  // edge is weighted iff they are inverted and don't connect either the sink or
+  // source. Since `C` is of minimal weight,. it is also of minimal inversions.
+  //
+  // The SOP instance can be solved by reduction using integer constraints.
+  // Here, we use the Miller-Tucker-Zemlin (MTZ) formulation of the TSP problem.
+  // In MTZ, a variable `x_ij in {0, 1}` is added to represent whether the edge
+  // `(i, j)` is taken. For eache node `v_i`, a variable `u_i` is added to
+  // indicate the order the node is visited in the cycle. Constraints are added
+  // to ensure that exactly one `x_ij` goes into and exits each node and such
+  // that if (i, j) is taken then `u_i < u_j` We can adjust the MTZ to work on
+  // an SOP instance by adding precendence constraints on the variables `u_i` by
+  // always forcing `u_i <= u_j + 1` iff `i` happens-before `j`.
+  //
+  // Reducing the number of variables is key to making the solver efficient.
+  // There are two optimizations we apply in the context of our specific
+  // optimization problem instance:
+  //
+  // A) For each edge (u, v) in E(H), only (u, v) needs to be added to G
+  // since a path that includes (v, u) would not satisfy the ordering
+  // constraint. Moreover, any edge (u', v') in E(K) such that there exists
+  // a node k such that (u', k) and (k, v') in E(H) can be eliminated from
+  // G. This is equivalent to eliminating any edges in G that are contained
+  // in the `Transitive-Closure(H) = K`. In general,
+  //
+  //    1. V(G) := V(H) + {source, sink}
+  //    2. E(G) := E(H) + {(u, v) in V(H) x V(H) : (u, v) and (v, u) not in K} +
+  //    {(u, sink) : u in V(H), out-degree[u] = 0} +
+  //    {(source, u) : u in V(H), in-degree[u] = 0}}
+  //    3. For all e = (u, v) in E(G),
+  //
+  //       w(e) := if tid(u) == tid(v) || (u == source) || (v == sink) then 0
+  //       else 1
+  //
+  // B) We observe the following. Firstly, for any two nodes `(u, v) in
+  // H_TC`, `tid[u] = tid[v] ==> u --> v`. I.e., there is always a
+  // happens-before relation between two nodes of the same label.
+  //
+  // For each sequence V = v_1, v_2, ..., v_r in E(H) such that
+  //
+  //    1. For all i in [1, r) out-degree[u_i] = in-degree[u_(i + 1)] = 1
+  //
+  //    V must appear in the SOP Hamiltonian cycle C of minimal
+  //    weight.
+  //
+  // Informally, given a contiguous "block" of transitions which must appear in
+  // order but are otherwise independent with other transitions except possibly
+  // the first and last transitions of the block, anything that doesn't
+  // "happen-before" the first transition in the block can be placed anywhere
+  // inside the block (otherwise there would be a transitive dependency
+  // somewhere in the block). Since the block ordering "forces" a certain
+  // ordering of the transitions, the number of inversions `I` in the block is
+  // fixed. For any `j` such that `v_1 --/--> j`, `tid[v_1] != tid[j]` and
+  // by transitivity `u --/--> j` and hence `tid[u] != tid[j]` for all u in V.
+  // `u --/--> j` further implies `(u, j) and (j, u) in G` for all `u in C`.
+  // Since `tid[u] != tid[j]`, `w_uj = w_ju = 1`. Since any Hamiltonian cycle
+  // must include all nodes in order, either the edge `(v_1, v_2)` is included
+  // or `(v_1, u_1), ..., (u_n, v_2)` for some `u_l` sequence such that `v_1
+  // --\--> u_1`. Since w_(v_1, v_2) <= 1 but `w_(v_1, u_1) = w_(u_n, v_2)`, the
+  // weight of taking the interior edge instead of two exterior ones smaller
+  // than taking the two outer ones. We can essentially treat (v_1, v_2), ...,
+  // (v_(r-1), v_r) as a subgraph with all incoming and outgoing edges of
+  // weight 1.
+  //
+  // Consequently, we can first group together simple chains and solve the
+  // smaller SOP instance and still obtain the same optimal result.
+  //
+  // To compute the reduced graph, we use the Disjoint Set Union. See
+  // https://cp-algorithms.com/data_structures/disjoint_set_union.html
+  struct dsu {
+    std::vector<size_t> parent;
+    std::vector<size_t> sizes;
+
+  public:
+    dsu(size_t n) : sizes(n, 1) {
+      parent.resize(n);
+      std::iota(parent.begin(), parent.end(), 0);
+    }
+
+    size_t find(size_t i) {
+      if (parent[i] == i)
+        return i;
+      return parent[i] = find(parent[i]);
+    }
+
+    void unite(size_t i, size_t j) {
+      size_t root_i = find(i);
+      size_t root_j = find(j);
+      if (root_i != root_j) {
+        if (sizes[root_i] < sizes[root_j])
+          std::swap(root_i, root_j);
+        parent[root_i] = root_j;
+        sizes[root_i] += sizes[root_j];
+      }
+    }
+  };
+
+  // Let `H_red` be the edge-reduced, transitive reduction graph. For each edge
+  // (u, v) in E(G_tr), if out(u) = in(v) = 1, then we can effectively combine
+  // `u` and `v`  together into a single node iff they refer to transitions run
+  // by the same thread. `supernodes` maps nodes in the reduced graph to the
+  // original graph `H`.
+  //
+  // supernodes[i] = [u_1, u_2, ..., u_(l+1)] <---> (u_j, u_{j+1}) in V(H) and
+  // out-degree[u_j] = in-degree[u_(j+1)] = 1
+  //
+  // The immediate transitive dependencies of supernodes[i].back() = u_(l+1)
+  // are the same as the transitive dependencies of the supernode.
+  const auto H = this->transitive_reduction();
+  const size_t N = H.size();
+  std::vector<size_t> out_degree(N, 0);
+  std::vector<size_t> in_degree(N, 0);
+  std::vector<std::vector<size_t>> supernodes;
+  {
+    dsu dsu(N);
+    {
+      std::vector<size_t> tids(N, 0);
+
+      for (size_t u = 0; u < N; ++u) {
+        out_degree[u] = H[u].size();
+        tids[u] = tid(u);
+        for (size_t v : H[u])
+          in_degree[v]++;
+      }
+
+      for (size_t u = 0; u < N; ++u) {
+        if (out_degree[u] == 1) {
+          size_t v = H[u][0]; // The only neighbor
+          if (in_degree[v] == 1 && tids[u] == tids[v])
+            dsu.unite(u, v);
+        }
+      }
+    }
+    {
+      std::map<size_t, std::vector<size_t>> groups;
+      for (size_t i = 0; i < N; ++i)
+        groups[dsu.find(i)].push_back(i);
+
+      supernodes.reserve(groups.size());
+      for (auto &p : groups)
+        supernodes.push_back(std::move(p.second));
+    }
+  }
+
+  SCIP *scip = nullptr;
+  SCIPcreate(&scip);
+  SCIPincludeDefaultPlugins(scip);
+  SCIPcreateProbBasic(scip, "Minimize_Inversions");
+  SCIPsetObjsense(scip, SCIP_OBJSENSE_MINIMIZE);
+
+  const size_t M = supernodes.size();
+  std::vector<SCIP_VAR *> u(M);
+  std::vector<std::vector<SCIP_VAR *>> x(
+      M + 1, std::vector<SCIP_VAR *>(M + 1, nullptr));
+
+  // Path variables: 1 <= u_i <= M
+  for (size_t i = 0; i < M; i++) {
+    const std::string name = "u_" + std::to_string(i);
+    SCIPcreateVarBasic(scip, &u[i], name.c_str(), 1.0, (double)M, 0.0,
+                       SCIP_VARTYPE_CONTINUOUS);
+    SCIPaddVar(scip, u[i]);
+  }
+
+  // All edges in the transitive reduction, add forward edge x_ij in {0, 1}
+  for (size_t i = 0; i < M; ++i) {
+    for (size_t j : H[supernodes[i].back()]) {
+      assert(i < j);
+      assert(x[i][j] == nullptr);
+      std::string name = "x_" + std::to_string(i) + std::to_string(j);
+      SCIPcreateVarBasic(scip, &x[i][j], name.c_str(), 0.0, 1.0,
+                         tid(i) != tid(j), SCIP_VARTYPE_BINARY);
+      SCIPaddVar(scip, x[i][j]);
+    }
+  }
+
+  // All edges not contained in the transitive closure
+  // Add forward _and_ backward edges x_ij and x_ji
+  for (size_t i = 0; i < M; ++i)
+    for (size_t j = i + 1; j < M; j++)
+      if (!happens_before(supernodes[i].front(), supernodes[j].front())) {
+        assert(x[i][j] == nullptr);
+        assert(x[j][i] == nullptr);
+        const double w_e = tid(i) != tid(j);
+        {
+          const std::string name = "x_" + std::to_string(i) + std::to_string(j);
+          SCIPcreateVarBasic(scip, &x[i][j], name.c_str(), 0.0, 1.0, w_e,
+                             SCIP_VARTYPE_BINARY);
+          SCIPaddVar(scip, x[i][j]);
+        }
+        {
+          const std::string name = "x_" + std::to_string(j) + std::to_string(i);
+          SCIPcreateVarBasic(scip, &x[j][i], name.c_str(), 0.0, 1.0, w_e,
+                             SCIP_VARTYPE_BINARY);
+          SCIPaddVar(scip, x[j][i]);
+        }
+      }
+
+  // Source/sink variables --> only added to DAG's entrances + exits
+  for (size_t i = 0; i < M; ++i) {
+    if (out_degree[supernodes[i].back()] == 0) {
+      const std::string name = "x_" + std::to_string(i) + std::to_string(M + 1);
+      SCIPcreateVarBasic(scip, &x[i][M + 1], name.c_str(), 0.0, 1.0, 0.0,
+                         SCIP_VARTYPE_BINARY);
+      SCIPaddVar(scip, x[i][M + 1]);
+    }
+
+    if (in_degree[supernodes[i].front()] == 0) {
+      const std::string name = "x_" + std::to_string(M + 1) + std::to_string(i);
+      SCIPcreateVarBasic(scip, &x[M + 1][i], name.c_str(), 0.0, 1.0, 0.0,
+                         SCIP_VARTYPE_BINARY);
+      SCIPaddVar(scip, x[M + 1][i]);
+    }
+  }
+
+  // MTZ Constraints
+  // A. Exactly one exit and one entrance per node (including source/sink)
+  for (size_t i = 0; i < M + 1; ++i) {
+    SCIP_CONS *enter_cons = nullptr;
+    SCIP_CONS *leave_cons = nullptr;
+    const std::string enter = "enter_" + std::to_string(i);
+    const std::string leave = "leave_" + std::to_string(i);
+    SCIPcreateConsBasicLinear(scip, &enter_cons, enter.c_str(), 0, nullptr,
+                              nullptr, 1.0, 1.0);
+    SCIPcreateConsBasicLinear(scip, &leave_cons, leave.c_str(), 0, nullptr,
+                              nullptr, 1.0, 1.0);
+    for (size_t j = 0; j < M + 1; ++j) {
+      if (x[i][j])
+        SCIPaddCoefLinear(scip, leave_cons, x[i][j], 1.0);
+      if (x[j][i])
+        SCIPaddCoefLinear(scip, enter_cons, x[j][i], 1.0);
+    }
+    SCIPaddCons(scip, enter_cons);
+    SCIPaddCons(scip, leave_cons);
+    SCIPreleaseCons(scip, &enter_cons);
+    SCIPreleaseCons(scip, &leave_cons);
+  }
+
+  // B. MTZ Subtour Elimination:
+  // -INF <= u_i - u_j + M*x_ij <= (M - 1) for i, j in [1, M], i != j
+  for (size_t i = 0; i < M; ++i) {
+    for (size_t j = 0; j < M; ++j) {
+      if (i == j)
+        continue;
+      SCIP_CONS *cons = nullptr;
+      const std::string name =
+          "subtour_" + std::to_string(i) + "_" + std::to_string(j);
+      SCIPcreateConsBasicLinear(scip, &cons, name.c_str(), 0, nullptr, nullptr,
+                                -SCIPinfinity(scip), (double)(M - 1));
+      SCIPaddCoefLinear(scip, cons, u[i], 1.0);
+      SCIPaddCoefLinear(scip, cons, u[j], -1.0);
+      SCIPaddCoefLinear(scip, cons, x[i][j], (double)M);
+      SCIPaddCons(scip, cons);
+      SCIPreleaseCons(scip, &cons);
+    }
+  }
+
+  // C. Precedence Constraints: INF >= u_target - u_i >= 1
+  for (size_t i = 0; i < M; ++i) {
+    for (size_t target : H[supernodes[i].back()]) {
+      SCIP_CONS *cons = nullptr;
+      const std::string name =
+          "precedence_" + std::to_string(i) + "_" + std::to_string(target);
+      SCIPcreateConsBasicLinear(scip, &cons, name.c_str(), 0, nullptr, nullptr,
+                                1.0, SCIPinfinity(scip));
+      SCIPaddCoefLinear(scip, cons, u[target], 1.0);
+      SCIPaddCoefLinear(scip, cons, u[i], -1.0);
+      SCIPaddCons(scip, cons);
+      SCIPreleaseCons(scip, &cons);
+    }
+  }
+
+  SCIPsolve(scip);
+  SCIP_SOL *sol = SCIPgetBestSol(scip);
+
+  std::vector<size_t> linearization;
+  struct NodePosition {
+    size_t id;
+    double u_value;
+  };
+
+  if (sol != nullptr) {
+    std::vector<NodePosition> sequence(N);
+    for (size_t i = 0; i < M; ++i) {
+      double val = SCIPgetSolVal(scip, sol, u[i]);
+      sequence.push_back({i, val});
+    }
+    std::sort(sequence.begin(), sequence.end(),
+              [](const NodePosition &a, const NodePosition &b) {
+                return a.u_value < b.u_value;
+              });
+    for (const auto &item : sequence)
+      std::move(supernodes[item.id].begin(), supernodes[item.id].end(),
+                std::back_inserter(linearization));
+  } else {
+    std::cerr << "No solution found!" << std::endl;
+    return {};
+  }
+  {
+    for (size_t i = 0; i < N; ++i) {
+      SCIPreleaseVar(scip, &u[i]);
+      for (size_t j = 0; j < N; ++j) {
+        if (x[i][j])
+          SCIPreleaseVar(scip, &x[i][j]);
+      }
+    }
+    SCIPfree(&scip);
+  }
+
+  std::vector<const transition *> linearized_trace(N, nullptr);
+  for (size_t i = 0; i < N; i++)
+    linearized_trace[i] = get_transition(linearization[i]);
+  return linearized_trace;
+#else
+  // Fallback to greedy if SCIP isn't available
+  return linearize_lowest_first();
+#endif
+}
+
+std::vector<const transition *>
+classic_dpor::dpor_context::linearize_lowest_first() const {
+  const auto adj_list = this->transitive_reduction();
+  const size_t N = adj_list.size();
+  const size_t INF = N + 1;
+  std::vector<size_t> linearization;
+  std::vector<size_t> ready_set;
   std::vector<int> in_degree(N, 0);
   for (size_t u = 0; u < N; ++u)
-    for (int v : adj_list[u])
+    for (size_t v : adj_list[u])
       in_degree[v]++;
 
   for (size_t i = 0; i < N; ++i)
     if (in_degree[i] == 0)
       ready_set.push_back(i);
 
-  runner_id_t last_rid = RUNNER_ID_MAX; // -1 indicates no last rid
+  runner_id_t last_rid = RUNNER_ID_MAX;
   while (!ready_set.empty()) {
-    int next_vertex = -1;
-    int selected_index = -1;
-
-    // Find the vertex with the same executor as the last one
+    size_t next_vertex = INF;
+    size_t selected_index = INF;
     if (last_rid != RUNNER_ID_MAX) {
       for (size_t i = 0; i < ready_set.size(); ++i) {
         const runner_id_t r = get_transition(ready_set[i])->get_executor();
@@ -724,9 +1139,8 @@ classic_dpor::dpor_context::linearize_lowest_first() {
       }
     }
 
-    // If no color match, or at the start, pick the thread with the lowest id
-    if (next_vertex == -1) {
-      // INVARIANT: Since mid_rid
+    // If no ID match, or at the start, pick the thread with the lowest id
+    if (next_vertex == INF) {
       runner_id_t min_rid = RID_INVALID;
       for (size_t i = 0; i < ready_set.size(); ++i) {
         const runner_id_t r = get_transition(ready_set[i])->get_executor();
@@ -739,7 +1153,7 @@ classic_dpor::dpor_context::linearize_lowest_first() {
     }
 
     linearization.push_back(next_vertex);
-    last_rid = stack.at(next_vertex).get_out_transition()->get_executor();
+    last_rid = get_transition(next_vertex)->get_executor();
 
     // Remove the selected vertex from the ready set
     // Swap with the back and pop for O(1) removal from vector (since order in S
@@ -755,8 +1169,6 @@ classic_dpor::dpor_context::linearize_lowest_first() {
     }
   }
 
-  // --- Phase 5 ---
-  // Convert the linearization into a transition trace
   std::vector<const transition *> linearized_trace(N, nullptr);
   for (size_t i = 0; i < N; i++)
     linearized_trace[i] = get_transition(linearization[i]);

From fdbf425af2e764eb837f30174fcabee112cf8ba3 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Thu, 18 Dec 2025 01:57:12 +0100
Subject: [PATCH 14/20] Add supernode translation to complete SCIP solver!

---
 .../algorithms/classic_dpor.cpp               | 107 ++++++++++++++----
 1 file changed, 82 insertions(+), 25 deletions(-)

diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index 2b7d43a..27b18b0 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -216,12 +216,6 @@ void classic_dpor::verify_using(coordinator &coordinator,
         }
 
         this->continue_dpor_by_expanding_trace_with(rid, context);
-        log_info(dpor_logger)
-            << context.coordinator.get_current_program_model();
-        auto lin = context.linearize_optimal();
-        for (auto *t : lin) {
-          log_info(dpor_logger) << t->debug_string();
-        }
         model_checking_stats.total_transitions++;
 
         // Now ask the question: will the next operation of this thread
@@ -729,6 +723,29 @@ classic_dpor::dpor_context::transitive_reduction() const {
   return adj_list;
 }
 
+void SCIP_dump(SCIP *scip) {
+  SCIP_CALL_ABORT(SCIPprintOrigProblem(scip, nullptr, "lp", false));
+  // SCIP_VAR **vars = SCIPgetVars(scip);
+  // std::cout << "=== VARIABLES ===\n";
+  // for (int i = 0; vars[i] != nullptr; ++i) {
+  //   SCIP_VAR *var = vars[i];
+  //   std::cout << "var[" << i << "]: " << SCIPvarGetName(var)
+  //             << "  lb = " << SCIPvarGetLbGlobal(var)
+  //             << "  ub = " << SCIPvarGetUbGlobal(var) << "\n";
+  // }
+
+  // SCIP_CONS **conss = SCIPgetConss(scip);
+  // std::cout << "\n=== CONSTRAINTS ===\n";
+  // for (int i = 0; conss[i] != nullptr; ++i) {
+  //   SCIP_CONS *cons = conss[i];
+  //   const char *name = SCIPconsGetName(cons);
+  //   std::cout << "cons[" << i << "]: " << (name ? name : "<no name>") <<
+  //   "\n"; SCIP_CALL_ABORT(SCIPprintCons(scip, cons, stdout)); std::cout <<
+  //   "\n";
+  // }
+  // std::cout << "\n=== DUMP COMPLETE ===" << std::endl;
+}
+
 std::vector<const transition *>
 classic_dpor::dpor_context::linearize_optimal() const {
 #ifndef MCMINI_USE_SCIP
@@ -888,21 +905,33 @@ classic_dpor::dpor_context::linearize_optimal() const {
   };
 
   // Let `H_red` be the edge-reduced, transitive reduction graph. For each edge
-  // (u, v) in E(G_tr), if out(u) = in(v) = 1, then we can effectively combine
+  // `(u, v) in E(H)`, if out(u) = in(v) = 1, then we can effectively combine
   // `u` and `v`  together into a single node iff they refer to transitions run
   // by the same thread. `supernodes` maps nodes in the reduced graph to the
   // original graph `H`.
   //
+  // ```
+  // Where `i` refers to a node ID in the reduced graph H_red
   // supernodes[i] = [u_1, u_2, ..., u_(l+1)] <---> (u_j, u_{j+1}) in V(H) and
   // out-degree[u_j] = in-degree[u_(j+1)] = 1
-  //
-  // The immediate transitive dependencies of supernodes[i].back() = u_(l+1)
-  // are the same as the transitive dependencies of the supernode.
+  // ```
+  // Where `i` refers to a member of V(H)
+  // dsu.find(i) = j <---> i is a part of supernode j in the reduced graph
+  //```
+  // The immediate transitive dependencies of `supernodes[i].back()` = u_(l+1)
+  // are the same as the transitive dependencies of the supernode. Moreoever,
+  // using the argument in the proof above, the set of edges
+  // {(u_i, v) in V(H) x V(H) : (u_i, v) and (v, u_i) not in K} is the same for
+  // any u_i. Here, we pick the first one `supernodes[i].front()`
   const auto H = this->transitive_reduction();
   const size_t N = H.size();
   std::vector<size_t> out_degree(N, 0);
   std::vector<size_t> in_degree(N, 0);
+
+  // INVARIANT: supernodes[i] is sorted by ID (and hence sorted in topological
+  // order)
   std::vector<std::vector<size_t>> supernodes;
+  std::unordered_map<size_t, size_t> H_to_supernode;
   {
     dsu dsu(N);
     {
@@ -929,11 +958,32 @@ classic_dpor::dpor_context::linearize_optimal() const {
         groups[dsu.find(i)].push_back(i);
 
       supernodes.reserve(groups.size());
-      for (auto &p : groups)
+      for (auto &p : groups) {
+        const size_t new_supernode_id = supernodes.size();
+        for (size_t i : p.second)
+          H_to_supernode[i] = new_supernode_id;
         supernodes.push_back(std::move(p.second));
+      }
     }
   }
 
+  // In what follows, there are implicitly two graphs:
+  //
+  // 1. The original transitive reduction `H` containing the "happens-before"
+  // DAG wihtout transitive dependencies with `N` nodes.
+  //
+  // 2. The reduced DAG `H_red` with `M <= N` nodes where nodes `(u, v)` in `H`
+  // where `out-degree[u] = in-degree[v] = 1` are combined together to reduce
+  // the number of variables. This graph isn't explicitly stored in memory.
+  // Instead, for each node in `H_red`, a list of back references in `H`
+  // indicating
+  //
+  // Iterations happen over nodes IDs in `H_red`. There a few important
+  // observations (here `i`s and `j`s are over super node indices)
+  // ```
+  // supernode[i].front() --/--> supernode[j].front() --> i -->_S' j
+  // out_degree_super[i] = out_degree[supernodes[i].back()]
+  // in_degree_super[i] = in_degree[supernodes[i].front()]
   SCIP *scip = nullptr;
   SCIPcreate(&scip);
   SCIPincludeDefaultPlugins(scip);
@@ -956,11 +1006,15 @@ classic_dpor::dpor_context::linearize_optimal() const {
   // All edges in the transitive reduction, add forward edge x_ij in {0, 1}
   for (size_t i = 0; i < M; ++i) {
     for (size_t j : H[supernodes[i].back()]) {
+      assert(supernodes[H_to_supernode[j]].front() == j);
+      j = H_to_supernode[j];
       assert(i < j);
       assert(x[i][j] == nullptr);
       std::string name = "x_" + std::to_string(i) + std::to_string(j);
       SCIPcreateVarBasic(scip, &x[i][j], name.c_str(), 0.0, 1.0,
-                         tid(i) != tid(j), SCIP_VARTYPE_BINARY);
+                         tid(supernodes[i].back()) !=
+                             tid(supernodes[j].front()),
+                         SCIP_VARTYPE_BINARY);
       SCIPaddVar(scip, x[i][j]);
     }
   }
@@ -972,7 +1026,8 @@ classic_dpor::dpor_context::linearize_optimal() const {
       if (!happens_before(supernodes[i].front(), supernodes[j].front())) {
         assert(x[i][j] == nullptr);
         assert(x[j][i] == nullptr);
-        const double w_e = tid(i) != tid(j);
+        const double w_e =
+            tid(supernodes[i].back()) != tid(supernodes[j].front());
         {
           const std::string name = "x_" + std::to_string(i) + std::to_string(j);
           SCIPcreateVarBasic(scip, &x[i][j], name.c_str(), 0.0, 1.0, w_e,
@@ -990,17 +1045,17 @@ classic_dpor::dpor_context::linearize_optimal() const {
   // Source/sink variables --> only added to DAG's entrances + exits
   for (size_t i = 0; i < M; ++i) {
     if (out_degree[supernodes[i].back()] == 0) {
-      const std::string name = "x_" + std::to_string(i) + std::to_string(M + 1);
-      SCIPcreateVarBasic(scip, &x[i][M + 1], name.c_str(), 0.0, 1.0, 0.0,
+      const std::string name = "x_" + std::to_string(i) + std::to_string(M);
+      SCIPcreateVarBasic(scip, &x[i][M], name.c_str(), 0.0, 1.0, 0.0,
                          SCIP_VARTYPE_BINARY);
-      SCIPaddVar(scip, x[i][M + 1]);
+      SCIPaddVar(scip, x[i][M]);
     }
 
     if (in_degree[supernodes[i].front()] == 0) {
-      const std::string name = "x_" + std::to_string(M + 1) + std::to_string(i);
-      SCIPcreateVarBasic(scip, &x[M + 1][i], name.c_str(), 0.0, 1.0, 0.0,
+      const std::string name = "x_" + std::to_string(M) + std::to_string(i);
+      SCIPcreateVarBasic(scip, &x[M][i], name.c_str(), 0.0, 1.0, 0.0,
                          SCIP_VARTYPE_BINARY);
-      SCIPaddVar(scip, x[M + 1][i]);
+      SCIPaddVar(scip, x[M][i]);
     }
   }
 
@@ -1031,7 +1086,7 @@ classic_dpor::dpor_context::linearize_optimal() const {
   // -INF <= u_i - u_j + M*x_ij <= (M - 1) for i, j in [1, M], i != j
   for (size_t i = 0; i < M; ++i) {
     for (size_t j = 0; j < M; ++j) {
-      if (i == j)
+      if (!x[i][j])
         continue;
       SCIP_CONS *cons = nullptr;
       const std::string name =
@@ -1049,6 +1104,7 @@ classic_dpor::dpor_context::linearize_optimal() const {
   // C. Precedence Constraints: INF >= u_target - u_i >= 1
   for (size_t i = 0; i < M; ++i) {
     for (size_t target : H[supernodes[i].back()]) {
+      target = H_to_supernode[target];
       SCIP_CONS *cons = nullptr;
       const std::string name =
           "precedence_" + std::to_string(i) + "_" + std::to_string(target);
@@ -1060,7 +1116,6 @@ classic_dpor::dpor_context::linearize_optimal() const {
       SCIPreleaseCons(scip, &cons);
     }
   }
-
   SCIPsolve(scip);
   SCIP_SOL *sol = SCIPgetBestSol(scip);
 
@@ -1071,7 +1126,8 @@ classic_dpor::dpor_context::linearize_optimal() const {
   };
 
   if (sol != nullptr) {
-    std::vector<NodePosition> sequence(N);
+    std::vector<NodePosition> sequence;
+    sequence.reserve(M);
     for (size_t i = 0; i < M; ++i) {
       double val = SCIPgetSolVal(scip, sol, u[i]);
       sequence.push_back({i, val});
@@ -1088,9 +1144,10 @@ classic_dpor::dpor_context::linearize_optimal() const {
     return {};
   }
   {
-    for (size_t i = 0; i < N; ++i) {
-      SCIPreleaseVar(scip, &u[i]);
-      for (size_t j = 0; j < N; ++j) {
+    for (size_t i = 0; i < M + 1; ++i) {
+      if (i < M)
+        SCIPreleaseVar(scip, &u[i]);
+      for (size_t j = 0; j < M + 1; ++j) {
         if (x[i][j])
           SCIPreleaseVar(scip, &x[i][j]);
       }

From a3903488e399a3c7e5e65fa32f9ed0e12e4096fa Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Fri, 19 Dec 2025 00:07:22 +0100
Subject: [PATCH 15/20] Add SCIP search to CMakeLists.txt

---
 CMakeLists.txt                                |  9 +++++++
 .../algorithms/classic_dpor.cpp               | 25 +++----------------
 2 files changed, 13 insertions(+), 21 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index c2fa5fc..87ad999 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -18,6 +18,11 @@ set(MCMINI_DIR "${CMAKE_SOURCE_DIR}")
 set(MCMINI_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/include")
 set(MCMINI_CMAKE_MODULE_DIR "${CMAKE_SOURCE_DIR}/cmake")
 set(MCMINI_WITH_DMTCP OFF)
+set(MCMINI_USE_SCIP OFF)
+
+if(MCMINI_USE_SCIP)
+find_package(scip)
+endif()
 
 # Project source files
 set(MCMINI_C_SRC
@@ -117,6 +122,10 @@ target_compile_options(mcmini
 target_link_libraries(mcmini
   PUBLIC
     "${MCMINI_EXTRA_LINK_FLAGS}")
+if (MCMINI_USE_SCIP)
+target_link_libraries(mcmini PUBLIC scip)
+target_compile_definitions(mcmini PUBLIC MCMINI_USE_SCIP)
+endif()
 
 add_subdirectory(src/examples)
 add_subdirectory(test)
diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index 27b18b0..3b9d285 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -12,7 +12,7 @@
 #include <unordered_set>
 #include <vector>
 
-#ifndef MCMINI_USE_SCIP
+#ifdef MCMINI_USE_SCIP
 #include "scip/scip.h"
 #include "scip/scipdefplugins.h"
 #include <numeric>
@@ -723,32 +723,15 @@ classic_dpor::dpor_context::transitive_reduction() const {
   return adj_list;
 }
 
+#ifdef MCMINI_USE_SCIP
 void SCIP_dump(SCIP *scip) {
   SCIP_CALL_ABORT(SCIPprintOrigProblem(scip, nullptr, "lp", false));
-  // SCIP_VAR **vars = SCIPgetVars(scip);
-  // std::cout << "=== VARIABLES ===\n";
-  // for (int i = 0; vars[i] != nullptr; ++i) {
-  //   SCIP_VAR *var = vars[i];
-  //   std::cout << "var[" << i << "]: " << SCIPvarGetName(var)
-  //             << "  lb = " << SCIPvarGetLbGlobal(var)
-  //             << "  ub = " << SCIPvarGetUbGlobal(var) << "\n";
-  // }
-
-  // SCIP_CONS **conss = SCIPgetConss(scip);
-  // std::cout << "\n=== CONSTRAINTS ===\n";
-  // for (int i = 0; conss[i] != nullptr; ++i) {
-  //   SCIP_CONS *cons = conss[i];
-  //   const char *name = SCIPconsGetName(cons);
-  //   std::cout << "cons[" << i << "]: " << (name ? name : "<no name>") <<
-  //   "\n"; SCIP_CALL_ABORT(SCIPprintCons(scip, cons, stdout)); std::cout <<
-  //   "\n";
-  // }
-  // std::cout << "\n=== DUMP COMPLETE ===" << std::endl;
 }
+#endif
 
 std::vector<const transition *>
 classic_dpor::dpor_context::linearize_optimal() const {
-#ifndef MCMINI_USE_SCIP
+#ifdef MCMINI_USE_SCIP
   // Given a fixed trace `T` of `N` transitions and a happens-before relation
   // `happens-before_T: [1, N] x [1, N] -> {0, 1}` over the indices of `T`, the
   // goal is to produce a new trace `T'` such that `happens-before_T(i, j) =

From b542633316ecf362cb30771f0c1c216e71ada04b Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Fri, 19 Dec 2025 20:20:24 +0100
Subject: [PATCH 16/20] Adjust callback interface to use virtual functions

Previously, a class could receive notifications about different events
during the verification of a program (e.g. when a deadlock was
encountered). This has been replaced with a more intuitive interface
using virtual functions. The specific reporting functionality for
printing was moved into a separate class instead of existing spread out
all over `mcmini.cpp`
---
 CMakeLists.txt                                |   3 +-
 include/mcmini/model/config.hpp               |  62 +++++
 include/mcmini/model_checking/algorithm.hpp   |  48 ++--
 .../algorithms/classic_dpor.hpp               |  25 +-
 include/mcmini/model_checking/reporter.hpp    |  31 +++
 src/mcmini/mcmini.cpp                         | 222 ++++++------------
 .../algorithms/classic_dpor.cpp               |  46 ++--
 src/mcmini/model_checking/reporter.cpp        |  86 +++++++
 8 files changed, 322 insertions(+), 201 deletions(-)
 create mode 100644 include/mcmini/model_checking/reporter.hpp
 create mode 100644 src/mcmini/model_checking/reporter.cpp

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 87ad999..3df3929 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -14,11 +14,11 @@ set(CMAKE_CXX_STANDARD_REQUIRED TRUE)
 # Project configuration
 option(BUILD_TESTS OFF)
 option(VERBOSE_TESTING OFF)
+option(MCMINI_USE_SCIP OFF)
 set(MCMINI_DIR "${CMAKE_SOURCE_DIR}")
 set(MCMINI_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/include")
 set(MCMINI_CMAKE_MODULE_DIR "${CMAKE_SOURCE_DIR}/cmake")
 set(MCMINI_WITH_DMTCP OFF)
-set(MCMINI_USE_SCIP OFF)
 
 if(MCMINI_USE_SCIP)
 find_package(scip)
@@ -54,6 +54,7 @@ set(MCMINI_CPP_SRC
   src/mcmini/model/transitions/process.cpp
   src/mcmini/model/transitions/thread.cpp
   src/mcmini/model/transitions/semaphore.cpp
+  src/mcmini/model_checking/reporter.cpp
   src/mcmini/model_checking/algorithms/classic_dpor.cpp
   src/mcmini/model_checking/algorithms/clock_vector.cpp
   src/mcmini/real_world/dmtcp_process_source.cpp
diff --git a/include/mcmini/model/config.hpp b/include/mcmini/model/config.hpp
index e9de31e..f581776 100644
--- a/include/mcmini/model/config.hpp
+++ b/include/mcmini/model/config.hpp
@@ -39,6 +39,68 @@ struct config {
    */
   bool stop_at_first_deadlock = false;
 
+  /**
+   * Whether relinearization should occur before displying buggy traces.
+   *
+   * A relinearization `T'` of a trace `T` is a permutation `sigma_n` such that
+   * `happens_before_T(i, j) <--> happens_before_T'(sigma(i), sigma(j))`.
+   * Informally, it is a reordering of the transitions in the trace that
+   * produces the same final state (and hence the same bugs, crashes, etc).
+   *
+   * The interest in relinearization is that although round-robin exploration in
+   * theory should enable McMini to capture shallower bugs more readily, the
+   * tradeoff is less readable traces when they're produced because the user
+   * will frequently have to switch between different threads to analyze the
+   * trace. Frequent switching makes it challenging to have a global idea of the
+   * issue causing a bug, even for small traces.
+   *
+   * With this enabled, McMini will first reorder the transitions using a greedy
+   * approach as follows:
+   *
+   * 1. When given the choice, McMini will first choose transitions of the same
+   * thread ID as the thread ID of the last chosen transition.
+   * 2. When McMini is forced by the happens-before relation to order a
+   * transition of a different thread ID, among the possible choices it chooses
+   * the smallest.
+   */
+  bool relinearize_traces = false;
+
+  /**
+   * Whether or not traces are relinearized optimally. Implies
+   * `relinearize_traces`.
+   *
+   * By default, relinearizations are created using a greedy algorithm by
+   * grouping together, as long as possible, transitions of the same thread ID
+   * subject to the happens-before relation over them. However, a
+   * relinearization produced using the greedy method is not guaranteed to
+   * minimize the number of "context switches" a user has to make. That is,
+   * there may exist a better linearization obeying the same happens-before
+   * relation but with a fewer number of changes between thread IDs.
+   *
+   * The optimization problem can be formulated as follows:
+   *
+   * Consider a colored DAG, G, with vertices V and edges E and a coloring
+   * function f: V —> C (where C is a finite set of colors). A linearization L
+   * of the vertices of G is a sequence of vertices v_I such
+   * that the order of v_I obeys the dag: a node ‘u’ appears before any node
+   * with which a directed edge from that node to any other node (formally u < v
+   * in L iff (u,v) in E).
+   *
+   * A colored linearization is the sequence of colors c_1, c_2, … of a
+   * linearization v_1, v_2, …, where c_i = f(v_i). Let h: L —> N
+   * denote the number of “inversions” in a linearization L.
+   * A linearization L has an inversion (v_i, v_i+1) iff f(v_i) != f(v_i+1). Let
+   * Inv: L -> Nat denote the number of inversions in a linearization L. Then
+   * MinInversions is the problem
+   *
+   * min (Inv L) where L is a linearization of G.
+   *
+   * The problem can be modeled as an instance of the Sequential Ordering
+   * Problem. Since in general this problem is challenging to solve, linearizing
+   * large traces may become impractical.
+   */
+  bool use_optimal_linearization = false;
+
   /**
    * Informs McMini that the target executable should be run under DMTCP with
    * `libmcmini.so` configured in record mode.
diff --git a/include/mcmini/model_checking/algorithm.hpp b/include/mcmini/model_checking/algorithm.hpp
index 5fce879..f488ab6 100644
--- a/include/mcmini/model_checking/algorithm.hpp
+++ b/include/mcmini/model_checking/algorithm.hpp
@@ -1,7 +1,5 @@
 #pragma once
 
-#include <functional>
-
 #include "mcmini/coordinator/coordinator.hpp"
 #include "mcmini/model/exception.hpp"
 #include "mcmini/model/program.hpp"
@@ -15,24 +13,34 @@ namespace model_checking {
  * the correctness of a program modeled under McMini.
  */
 class algorithm {
- public:
+public:
+  enum class exploration_policy : uint { round_robin, smallest_first };
+
+  struct context {
+    virtual const model::program &get_model() const = 0;
+    virtual std::vector<const model::transition *>
+    linearize_lowest_first() const = 0;
+    virtual std::vector<const model::transition *>
+    linearize_optimal() const = 0;
+  };
+
   struct callbacks {
-   public:
-    callbacks() = default;
-    std::function<void(const coordinator &, const stats &)> crash;
-    std::function<void(const coordinator &, const stats &)> deadlock;
-    std::function<void(const coordinator &, const stats &)> data_race;
-    std::function<void(const coordinator &, const stats &)> unknown_error;
-    std::function<void(const coordinator &, const stats &)> trace_completed;
-    std::function<void(const coordinator &, const stats &,
-                       const real_world::process::termination_error &)>
-        abnormal_termination;
-    std::function<void(const coordinator &, const stats &,
-                       const real_world::process::nonzero_exit_code_error &)>
-        nonzero_exit_code;
-    std::function<void(const coordinator &, const stats &,
-                       const model::undefined_behavior_exception &)>
-        undefined_behavior;
+    virtual void crash(const context &, const stats &) const {}
+    virtual void deadlock(const context &, const stats &) const {}
+    virtual void data_race(const context &, const stats &) const {}
+    virtual void trace_completed(const context &, const stats &) const {}
+
+    virtual void
+    abnormal_termination(const context &, const stats &,
+                         const real_world::process::termination_error &) const {
+    }
+    virtual void nonzero_exit_code(
+        const context &, const stats &,
+        const real_world::process::nonzero_exit_code_error &) const {}
+
+    virtual void
+    undefined_behavior(const context &, const stats &,
+                       const model::undefined_behavior_exception &) const {}
   };
 
   /**
@@ -72,4 +80,4 @@ class algorithm {
   }
 };
 
-};  // namespace model_checking
+}; // namespace model_checking
diff --git a/include/mcmini/model_checking/algorithms/classic_dpor.hpp b/include/mcmini/model_checking/algorithms/classic_dpor.hpp
index 05bcab9..adf6a0a 100644
--- a/include/mcmini/model_checking/algorithms/classic_dpor.hpp
+++ b/include/mcmini/model_checking/algorithms/classic_dpor.hpp
@@ -29,24 +29,37 @@ class classic_dpor final : public algorithm {
   static dependency_relation_type default_dependencies();
   static coenabled_relation_type default_coenabledness();
 
-  struct configuration {
+  struct config {
+  public:
+    config() = default;
+    config(const model::config &c)
+        : maximum_total_execution_depth(c.maximum_total_execution_depth),
+          stop_at_first_deadlock(c.stop_at_first_deadlock),
+          relinearize_traces(c.relinearize_traces),
+          use_optimal_linearization(c.use_optimal_linearization),
+          policy(c.use_round_robin_scheduling
+                     ? exploration_policy::round_robin
+                     : exploration_policy::smallest_first) {}
+
+  public:
     dependency_relation_type dependency_relation =
         classic_dpor::default_dependencies();
     coenabled_relation_type coenabled_relation =
         classic_dpor::default_coenabledness();
     uint32_t maximum_total_execution_depth = 1500;
+    bool stop_at_first_deadlock = false;
+    bool relinearize_traces = false;
+    bool use_optimal_linearization = false;
     bool assumes_linear_program_flow = false;
-
-    enum class exploration_policy : uint { round_robin, smallest_first };
     exploration_policy policy = exploration_policy::smallest_first;
-    bool stop_at_first_deadlock = false;
   };
 
   classic_dpor() = default;
-  classic_dpor(configuration config) : config(std::move(config)) {}
+  classic_dpor(config config) : config(std::move(config)) {}
+  classic_dpor(const model::config &config) : config(config) {}
 
 private:
-  configuration config;
+  config config;
 
   bool are_dependent(const model::transition &t1,
                      const model::transition &t2) const;
diff --git a/include/mcmini/model_checking/reporter.hpp b/include/mcmini/model_checking/reporter.hpp
new file mode 100644
index 0000000..fa7fbb7
--- /dev/null
+++ b/include/mcmini/model_checking/reporter.hpp
@@ -0,0 +1,31 @@
+#pragma once
+#include "mcmini/model/config.hpp"
+#include "mcmini/model/exception.hpp"
+#include "mcmini/model_checking/algorithm.hpp"
+
+namespace model_checking {
+class reporter : public algorithm::callbacks {
+private:
+  const bool verbose;
+
+public:
+  reporter() = default;
+  reporter(const model::config &c) : verbose(c.verbose) {}
+
+public:
+  // void crash(const algorithm::context &, const stats &) const override;
+  void deadlock(const algorithm::context &, const stats &) const override;
+  // void data_race(const algorithm::context &, const stats &) const override;
+  void trace_completed(const algorithm::context &,
+                       const stats &) const override;
+  void abnormal_termination(
+      const algorithm::context &, const stats &,
+      const real_world::process::termination_error &) const override;
+  // void nonzero_exit_code(
+  //     const algorithm::context &, const stats &,
+  //     const real_world::process::nonzero_exit_code_error &) const override;
+  void undefined_behavior(
+      const algorithm::context &, const stats &,
+      const model::undefined_behavior_exception &) const override;
+};
+} // namespace model_checking
\ No newline at end of file
diff --git a/src/mcmini/mcmini.cpp b/src/mcmini/mcmini.cpp
index ec35d4c..27371e2 100644
--- a/src/mcmini/mcmini.cpp
+++ b/src/mcmini/mcmini.cpp
@@ -11,6 +11,7 @@
 #include "mcmini/model/transitions/thread/thread_exit.hpp"
 #include "mcmini/model_checking/algorithm.hpp"
 #include "mcmini/model_checking/algorithms/classic_dpor.hpp"
+#include "mcmini/model_checking/reporter.hpp"
 #include "mcmini/real_world/fifo.hpp"
 #include "mcmini/real_world/process/dmtcp_process_source.hpp"
 #include "mcmini/real_world/process/multithreaded_fork_process_source.hpp"
@@ -43,174 +44,89 @@ using namespace model_checking;
 using namespace objects;
 using namespace real_world;
 
-visible_object_state* translate_recorded_object_to_model(
-    const ::visible_object& recorded_object,
+logging::logger setup_logger("mcmini");
+
+visible_object_state *translate_recorded_object_to_model(
+    const ::visible_object &recorded_object,
     const std::unordered_map<
-        void*, std::vector<std::pair<runner_id_t, condition_variable_status>>>
+        void *, std::vector<std::pair<runner_id_t, condition_variable_status>>>
         cv_waiting_threads) {
   // TODO: A function table would be slightly better, but this works perfectly
   // fine too.
   switch (recorded_object.type) {
-    case MUTEX: {
-      auto mutex_state =
-          static_cast<objects::mutex::state>(recorded_object.mut_state);
-      pthread_mutex_t* mutex_location =
-          (pthread_mutex_t*)recorded_object.location;
-      return new objects::mutex(mutex_state, mutex_location);
-    }
-    case CONDITION_VARIABLE: {
-      // Create the condition variable model object with full state information
-      auto cv_state = static_cast<objects::condition_variable::state>(
-          recorded_object.cond_state.status);
-
-      runner_id_t interacting_thread =
-          recorded_object.cond_state.interacting_thread;
-      pthread_mutex_t* associated_mutex =
-          recorded_object.cond_state.associated_mutex;
-      int count = recorded_object.cond_state.count;
-      // get waiting threads from the map
-      auto it = cv_waiting_threads.find(recorded_object.location);
-      std::vector<std::pair<runner_id_t, condition_variable_status>>
-          waiters_with_state =
-              (it != cv_waiting_threads.end())
-                  ? it->second
-                  : std::vector<
-                        std::pair<runner_id_t, condition_variable_status>>();
-      return new objects::condition_variable(cv_state, interacting_thread,
-                                             associated_mutex, count,
-                                             waiters_with_state);
-    }
-    case SEMAPHORE: {
-      return new objects::semaphore(static_cast<objects::semaphore::state>(
-                                        recorded_object.sem_state.status),
-                                    recorded_object.sem_state.count);
-    }
-    // Other objects here
-    // case ...  { }
-    // ...
-    default: {
-      std::cerr << "The new object type" << recorded_object.type
-                << "hasn't been implemented yet\n";
-      std::abort();
-    }
+  case MUTEX: {
+    auto mutex_state =
+        static_cast<objects::mutex::state>(recorded_object.mut_state);
+    pthread_mutex_t *mutex_location =
+        (pthread_mutex_t *)recorded_object.location;
+    return new objects::mutex(mutex_state, mutex_location);
   }
-}
-
-runner_state* translate_recorded_runner_to_model(
-    const ::visible_object& recorded_object) {
-  switch (recorded_object.type) {
-    case THREAD: {
-      return new objects::thread(recorded_object.thrd_state.status);
-    }
-    default: {
-      std::abort();
-    }
+  case CONDITION_VARIABLE: {
+    // Create the condition variable model object with full state information
+    auto cv_state = static_cast<objects::condition_variable::state>(
+        recorded_object.cond_state.status);
+
+    runner_id_t interacting_thread =
+        recorded_object.cond_state.interacting_thread;
+    pthread_mutex_t *associated_mutex =
+        recorded_object.cond_state.associated_mutex;
+    int count = recorded_object.cond_state.count;
+    // get waiting threads from the map
+    auto it = cv_waiting_threads.find(recorded_object.location);
+    std::vector<std::pair<runner_id_t, condition_variable_status>>
+        waiters_with_state =
+            (it != cv_waiting_threads.end())
+                ? it->second
+                : std::vector<
+                      std::pair<runner_id_t, condition_variable_status>>();
+    return new objects::condition_variable(cv_state, interacting_thread,
+                                           associated_mutex, count,
+                                           waiters_with_state);
   }
-}
-
-void finished_trace_classic_dpor(const coordinator& c, const stats& stats) {
-  std::stringstream ss;
-  const auto& program_model = c.get_current_program_model();
-  ss << "TRACE " << stats.trace_id << "\n";
-  for (const auto& t : program_model.get_trace()) {
-    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
-  }
-  ss << "\nNEXT THREAD OPERATIONS\n";
-  for (const auto& tpair : program_model.get_pending_transitions()) {
-    ss << "thread " << tpair.first << ": " << tpair.second->to_string() << "\n";
+  case SEMAPHORE: {
+    return new objects::semaphore(static_cast<objects::semaphore::state>(
+                                      recorded_object.sem_state.status),
+                                  recorded_object.sem_state.count);
   }
-  std::cout << ss.str();
-  std::cout.flush();
-}
-
-void found_undefined_behavior(const coordinator& c, const stats& stats,
-                              const undefined_behavior_exception& ub) {
-  std::cerr << "UNDEFINED BEHAVIOR:\n" << ub.what() << std::endl;
-  finished_trace_classic_dpor(c, stats);
-}
-
-void found_abnormal_termination(
-    const coordinator& c, const stats& stats,
-    const real_world::process::termination_error& ub) {
-  std::cerr << "Abnormally Termination (signo: " << ub.signo
-            << ", signal: " << sig_to_str.at(ub.signo) << "):\n"
-            << ub.what() << std::endl;
-
-  std::stringstream ss;
-  const auto& program_model = c.get_current_program_model();
-  ss << "TRACE " << stats.trace_id << "\n";
-  for (const auto& t : program_model.get_trace()) {
-    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+  // Other objects here
+  // case ...  { }
+  // ...
+  default: {
+    std::cerr << "The new object type" << recorded_object.type
+              << "hasn't been implemented yet\n";
+    std::abort();
   }
-  const transition* terminator =
-      program_model.get_pending_transition_for(ub.culprit);
-  ss << "thread " << terminator->get_executor() << ": "
-     << terminator->to_string() << "\n";
-
-  ss << "\nNEXT THREAD OPERATIONS\n";
-  for (const auto& tpair : program_model.get_pending_transitions()) {
-    if (tpair.first == terminator->get_executor()) {
-      ss << "thread " << tpair.first << ": executing"
-         << "\n";
-    } else {
-      ss << "thread " << tpair.first << ": " << tpair.second->to_string()
-         << "\n";
-    }
   }
-  ss << stats.total_transitions + 1 << " total transitions executed"
-     << "\n";
-  std::cout << ss.str();
-  std::cout.flush();
 }
 
-void found_deadlock(const coordinator& c, const stats& stats) {
-  std::cerr << "DEADLOCK" << std::endl;
-  std::stringstream ss;
-  const auto& program_model = c.get_current_program_model();
-  for (const auto& t : program_model.get_trace()) {
-    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+runner_state *
+translate_recorded_runner_to_model(const ::visible_object &recorded_object) {
+  switch (recorded_object.type) {
+  case THREAD: {
+    return new objects::thread(recorded_object.thrd_state.status);
+  }
+  default: {
+    std::abort();
   }
-  ss << "\nNEXT THREAD OPERATIONS\n";
-  for (const auto& tpair : program_model.get_pending_transitions()) {
-    ss << "thread " << tpair.first << ": " << tpair.second->to_string() << "\n";
   }
-  std::cout << ss.str();
-  std::cout.flush();
 }
 
-void do_model_checking(const config& config) {
+void do_model_checking(const config &config) {
   algorithm::callbacks c;
   target target_program(config.target_executable,
                         config.target_executable_args);
+  target_program.set_quiet(config.quiet_program_output);
   coordinator coordinator(program::starting_from_main(),
                           transition_registry::default_registry(),
                           make_unique<fork_process_source>(target_program));
-  std::cerr << "\n\n**************** INTIAL STATE *********************\n\n";
-  coordinator.get_current_program_model().dump_state(std::cerr);
-  std::cerr << "\n\n**************** INTIAL STATE *********************\n\n";
-  std::cerr.flush();
-
-  using mcconfig = model_checking::classic_dpor::configuration;
-  mcconfig mc_config;
-  mc_config.maximum_total_execution_depth =
-      config.maximum_total_execution_depth;
-  mc_config.stop_at_first_deadlock = config.stop_at_first_deadlock;
-  mc_config.policy = config.use_round_robin_scheduling
-                         ? mcconfig::exploration_policy::round_robin
-                         : mcconfig::exploration_policy::smallest_first;
-
-  model_checking::classic_dpor classic_dpor_checker(std::move(mc_config));
-  if (config.verbose)
-    c.trace_completed = &finished_trace_classic_dpor;
-  c.deadlock = &found_deadlock;
-  c.undefined_behavior = &found_undefined_behavior;
-  c.abnormal_termination = &found_abnormal_termination;
-  classic_dpor_checker.verify_using(coordinator, c);
+  model_checking::reporter reporter(config);
+  model_checking::classic_dpor classic_dpor_checker(config);
+  classic_dpor_checker.verify_using(coordinator, reporter);
   std::cout << "Model checking completed!" << std::endl;
 }
 
-void do_model_checking_from_dmtcp_ckpt_file(const config& config) {
-  volatile mcmini_shm_file* rw_region =
+void do_model_checking_from_dmtcp_ckpt_file(const config &config) {
+  volatile mcmini_shm_file *rw_region =
       xpc_resources::get_instance().get_rw_region()->as<mcmini_shm_file>();
 
   std::unique_ptr<process_source> dmtcp_template_handle;
@@ -227,7 +143,6 @@ void do_model_checking_from_dmtcp_ckpt_file(const config& config) {
   // Make sure that `dmtcp_restart` has executed and that the template
   // process is ready for execution; otherwise, the state restoration will not
   // work as expected.
-  algorithm::callbacks c;
   transition_registry tr = transition_registry::default_registry();
   coordinator coordinator(program(), tr, std::move(dmtcp_template_handle));
   {
@@ -324,18 +239,15 @@ void do_model_checking_from_dmtcp_ckpt_file(const config& config) {
   std::cerr << "\n\n**************** INTIAL STATE *********************\n\n";
   std::cerr.flush();
 
-  model_checking::classic_dpor classic_dpor_checker;
-  c.trace_completed = &finished_trace_classic_dpor;
-  c.undefined_behavior = &found_undefined_behavior;
-  c.deadlock = &found_deadlock;
-  c.abnormal_termination = &found_abnormal_termination;
-  classic_dpor_checker.verify_using(coordinator, c);
+  model_checking::reporter reporter(config);
+  model_checking::classic_dpor classic_dpor_checker(config);
+  classic_dpor_checker.verify_using(coordinator, reporter);
   std::cerr << "Deep debugging completed!" << std::endl;
 }
 
 #include "mcmini/log/logger.hpp"
 
-void do_recording(const config& config) {
+void do_recording(const config &config) {
   char dir[PATH_MAX];
   // FIXME:  This depends on mcmini starting in root dir of git repo.
   std::string libmcini_dir = getcwd(dir, sizeof(dir)) ? dir : "PATH_TOO_LONG";
@@ -434,6 +346,14 @@ int main_cpp(int argc, const char** argv) {
                strcmp(cur_arg[0], "-rr") == 0) {
       mcmini_config.use_round_robin_scheduling = true;
       cur_arg += 1;
+    } else if ((strcmp(cur_arg[0], "--optimal-relinearization") == 0) ||
+               strcmp(cur_arg[0], "-orelin") == 0) {
+      mcmini_config.use_optimal_linearization = true;
+      cur_arg += 1;
+    } else if ((strcmp(cur_arg[0], "--relinearize") == 0) ||
+               strcmp(cur_arg[0], "-relin") == 0) {
+      mcmini_config.relinearize_traces = true;
+      cur_arg += 1;
     } else if (strcmp(cur_arg[0], "--from-checkpoint") == 0 ||
                strcmp(cur_arg[0], "-ckpt") == 0) {
       mcmini_config.checkpoint_file = cur_arg[1];
diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index 3b9d285..7347c7c 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -21,6 +21,7 @@
 #include "mcmini/coordinator/coordinator.hpp"
 #include "mcmini/defines.h"
 #include "mcmini/log/logger.hpp"
+#include "mcmini/model/config.hpp"
 #include "mcmini/model/exception.hpp"
 #include "mcmini/model/program.hpp"
 #include "mcmini/model/transition.hpp"
@@ -41,7 +42,8 @@ using namespace model_checking;
 
 logger dpor_logger("dpor");
 
-struct classic_dpor::dpor_context {
+struct classic_dpor::dpor_context : public algorithm::context {
+public:
   ::coordinator &coordinator;
   std::vector<model_checking::stack_item> stack;
 
@@ -98,6 +100,9 @@ struct classic_dpor::dpor_context {
   std::vector<std::vector<size_t>> transitive_reduction() const;
   std::vector<const transition *> linearize_lowest_first() const;
   std::vector<const transition *> linearize_optimal() const;
+  const program &get_model() const {
+    return this->coordinator.get_current_program_model();
+  }
 };
 
 clock_vector classic_dpor::accumulate_max_clock_vector_against(
@@ -175,11 +180,11 @@ void classic_dpor::verify_using(coordinator &coordinator,
       try {
         runner_id_t rid;
         switch (config.policy) {
-        case configuration::exploration_policy::smallest_first: {
+        case algorithm::exploration_policy::smallest_first: {
           rid = dpor_stack.back().get_first_enabled_runner();
           break;
         }
-        case configuration::exploration_policy::round_robin: {
+        case algorithm::exploration_policy::round_robin: {
           auto unscheduled_runners = dpor_stack.back().get_enabled_runners();
 
           // For round robin scheduling, always prefer to schedule
@@ -237,33 +242,29 @@ void classic_dpor::verify_using(coordinator &coordinator,
               "The program exited abnormally");
         }
       } catch (const model::undefined_behavior_exception &ube) {
-        if (callbacks.undefined_behavior)
-          callbacks.undefined_behavior(coordinator, model_checking_stats, ube);
+        callbacks.undefined_behavior(context, model_checking_stats, ube);
         return;
       } catch (const real_world::process::termination_error &te) {
-        if (callbacks.abnormal_termination)
-          callbacks.abnormal_termination(coordinator, model_checking_stats, te);
+        callbacks.abnormal_termination(context, model_checking_stats, te);
         return;
       } catch (const real_world::process::nonzero_exit_code_error &nzec) {
-        if (callbacks.nonzero_exit_code)
-          callbacks.nonzero_exit_code(coordinator, model_checking_stats, nzec);
+        callbacks.nonzero_exit_code(context, model_checking_stats, nzec);
         return;
       }
     }
 
-    if (callbacks.trace_completed)
-      callbacks.trace_completed(coordinator, model_checking_stats);
+    callbacks.trace_completed(context, model_checking_stats);
 
-    if (config.stop_at_first_deadlock &&
-        coordinator.get_current_program_model().is_in_deadlock()) {
-      log_info(dpor_logger)
-          << "First deadlock found. Reporting and stopping model checking.";
-      if (callbacks.deadlock)
-        callbacks.deadlock(coordinator, model_checking_stats);
-      return;
-    } else if (callbacks.deadlock &&
-               coordinator.get_current_program_model().is_in_deadlock())
-      callbacks.deadlock(coordinator, model_checking_stats);
+    if (coordinator.get_current_program_model().is_in_deadlock()) {
+      if (config.stop_at_first_deadlock) {
+        log_info(dpor_logger)
+            << "First deadlock found. Reporting and stopping model checking.";
+        callbacks.deadlock(context, model_checking_stats);
+        return;
+      } else {
+        callbacks.deadlock(context, model_checking_stats);
+      }
+    }
 
     // 3. Backtrack phase
     while (!dpor_stack.empty() && dpor_stack.back().backtrack_set_empty())
@@ -305,8 +306,7 @@ void classic_dpor::verify_using(coordinator &coordinator,
         // since we only account for scheduling that occurs during _expansion_.
         round_robin_sched.clear();
       } catch (const model::undefined_behavior_exception &ube) {
-        if (callbacks.undefined_behavior)
-          callbacks.undefined_behavior(coordinator, model_checking_stats, ube);
+        callbacks.undefined_behavior(context, model_checking_stats, ube);
         return;
       }
     }
diff --git a/src/mcmini/model_checking/reporter.cpp b/src/mcmini/model_checking/reporter.cpp
new file mode 100644
index 0000000..902d38d
--- /dev/null
+++ b/src/mcmini/model_checking/reporter.cpp
@@ -0,0 +1,86 @@
+#include "mcmini/model_checking/reporter.hpp"
+#include "mcmini/signal.hpp"
+
+using namespace model;
+using namespace model_checking;
+
+void reporter::trace_completed(const algorithm::context &c,
+                               const stats &stats) const {
+  if (!verbose)
+    return;
+  std::stringstream ss;
+  ss << "TRACE " << stats.trace_id << "\n";
+  for (const auto &t : c.get_model().get_trace()) {
+    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+  }
+  ss << "\nNEXT THREAD OPERATIONS\n";
+  for (const auto &tpair : c.get_model().get_pending_transitions()) {
+    ss << "thread " << tpair.first << ": " << tpair.second->to_string() << "\n";
+  }
+  std::cout << ss.str();
+  std::cout.flush();
+}
+
+void reporter::deadlock(const algorithm::context &c, const stats &stats) const {
+  std::cerr << "DEADLOCK" << std::endl;
+  std::stringstream ss;
+  for (const auto &t : c.get_model().get_trace()) {
+    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+  }
+  ss << "\nNEXT THREAD OPERATIONS\n";
+  for (const auto &tpair : c.get_model().get_pending_transitions()) {
+    ss << "thread " << tpair.first << ": " << tpair.second->to_string() << "\n";
+  }
+  std::cout << ss.str();
+  std::cout.flush();
+}
+
+void reporter::undefined_behavior(
+    const algorithm::context &c, const stats &stats,
+    const undefined_behavior_exception &ub) const {
+  std::cerr << "UNDEFINED BEHAVIOR:\n" << ub.what() << std::endl;
+  std::stringstream ss;
+  ss << "TRACE " << stats.trace_id << "\n";
+  for (const auto &t : c.get_model().get_trace()) {
+    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+  }
+  ss << "\nNEXT THREAD OPERATIONS\n";
+  for (const auto &tpair : c.get_model().get_pending_transitions()) {
+    ss << "thread " << tpair.first << ": " << tpair.second->to_string() << "\n";
+  }
+  std::cout << ss.str();
+  std::cout.flush();
+}
+
+void reporter::abnormal_termination(
+    const algorithm::context &c, const stats &stats,
+    const real_world::process::termination_error &ub) const {
+  std::cerr << "Abnormally Termination (signo: " << ub.signo
+            << ", signal: " << sig_to_str.at(ub.signo) << "):\n"
+            << ub.what() << std::endl;
+
+  std::stringstream ss;
+  ss << "TRACE " << stats.trace_id << "\n";
+  for (const auto &t : c.get_model().get_trace()) {
+    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+  }
+  const transition *terminator =
+      c.get_model().get_pending_transition_for(ub.culprit);
+  ss << "thread " << terminator->get_executor() << ": "
+     << terminator->to_string() << "\n";
+
+  ss << "\nNEXT THREAD OPERATIONS\n";
+  for (const auto &tpair : c.get_model().get_pending_transitions()) {
+    if (tpair.first == terminator->get_executor()) {
+      ss << "thread " << tpair.first << ": executing"
+         << "\n";
+    } else {
+      ss << "thread " << tpair.first << ": " << tpair.second->to_string()
+         << "\n";
+    }
+  }
+  ss << stats.total_transitions + 1 << " total transitions executed"
+     << "\n";
+  std::cout << ss.str();
+  std::cout.flush();
+}
\ No newline at end of file

From 3e972cf4da0d35113b5790a64f66b235e419a9cc Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Fri, 19 Dec 2025 20:24:45 +0100
Subject: [PATCH 17/20] Simplify deadlock exit condition

---
 src/mcmini/model/program.cpp | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/mcmini/model/program.cpp b/src/mcmini/model/program.cpp
index f29563c..cab2e5b 100644
--- a/src/mcmini/model/program.cpp
+++ b/src/mcmini/model/program.cpp
@@ -107,8 +107,8 @@ void program::model_execution_of(runner_id_t p, const transition *npo) {
   trace.push(next_steps.replace_unowned(npo));
 }
 
-state::objid_t program::discover_object(
-    const visible_object_state *initial_state) {
+state::objid_t
+program::discover_object(const visible_object_state *initial_state) {
   return this->state_seq.add_object(initial_state);
 }
 
@@ -134,7 +134,8 @@ bool program::is_in_deadlock() const {
 
   // If any transition is enabled, we are not in deadlock
   for (const auto &pair : this->get_pending_transitions()) {
-    if (pair.second->is_enabled_in(this->state_seq)) return false;
+    if (pair.second->is_enabled_in(this->state_seq))
+      return false;
   }
 
   // Furthermore, if there are NO enabled transitions, we need to check if this
@@ -151,12 +152,10 @@ bool program::is_in_deadlock() const {
   // probably still want to show a bug if other userspace threads manage to get
   // into a deadlock even while the main thread could exit, so we don't treat
   // that case specially.
-  bool all_exited = true;
-  for (const auto &pair : this->get_pending_transitions()) {
+  for (const auto &pair : this->get_pending_transitions())
     if (!this->state_seq.get_state_of_runner(pair.first)->has_exited())
-      all_exited = false;
-  }
-  return !all_exited;
+      return true; // All blocked and at least one hasn't exited
+  return false;
 }
 
 std::ostream &program::dump_state(std::ostream &os) const {

From 170a91bdc79ade7e98e27ef96534740bae3d434f Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Fri, 19 Dec 2025 20:25:25 +0100
Subject: [PATCH 18/20] Disable messaging from SCIP solver when linearizing
 traces

---
 src/mcmini/model_checking/algorithms/classic_dpor.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/mcmini/model_checking/algorithms/classic_dpor.cpp b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
index 7347c7c..58ca691 100644
--- a/src/mcmini/model_checking/algorithms/classic_dpor.cpp
+++ b/src/mcmini/model_checking/algorithms/classic_dpor.cpp
@@ -969,6 +969,7 @@ classic_dpor::dpor_context::linearize_optimal() const {
   // in_degree_super[i] = in_degree[supernodes[i].front()]
   SCIP *scip = nullptr;
   SCIPcreate(&scip);
+  SCIPsetMessagehdlr(scip, NULL);
   SCIPincludeDefaultPlugins(scip);
   SCIPcreateProbBasic(scip, "Minimize_Inversions");
   SCIPsetObjsense(scip, SCIP_OBJSENSE_MINIMIZE);

From e787142c0c967da0de8a9a93b1d90ac50137d73e Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Fri, 19 Dec 2025 20:37:48 +0100
Subject: [PATCH 19/20] Print relinearized traces when given specific flags

McMini now will print different relinearizations of traces when given
either the `-relin` or `-orelin` flags. The former corresponds to the
greedy relinearization approach while the latter corresponds to the
optimal reordering based on the SCIP solver. McMini must be compiled
with SCIP; otherwise, optimal reordering will fallback to the greedy
approach
---
 include/mcmini/model_checking/algorithm.hpp   |  3 +
 .../algorithms/classic_dpor.hpp               |  4 -
 include/mcmini/model_checking/reporter.hpp    | 11 ++-
 src/mcmini/model_checking/reporter.cpp        | 81 +++++++++++--------
 4 files changed, 60 insertions(+), 39 deletions(-)

diff --git a/include/mcmini/model_checking/algorithm.hpp b/include/mcmini/model_checking/algorithm.hpp
index f488ab6..df5bc65 100644
--- a/include/mcmini/model_checking/algorithm.hpp
+++ b/include/mcmini/model_checking/algorithm.hpp
@@ -22,6 +22,9 @@ class algorithm {
     linearize_lowest_first() const = 0;
     virtual std::vector<const model::transition *>
     linearize_optimal() const = 0;
+    std::vector<const model::transition *> linearize_trace(bool optimal) const {
+      return optimal ? linearize_optimal() : linearize_lowest_first();
+    }
   };
 
   struct callbacks {
diff --git a/include/mcmini/model_checking/algorithms/classic_dpor.hpp b/include/mcmini/model_checking/algorithms/classic_dpor.hpp
index adf6a0a..7eba8e7 100644
--- a/include/mcmini/model_checking/algorithms/classic_dpor.hpp
+++ b/include/mcmini/model_checking/algorithms/classic_dpor.hpp
@@ -35,8 +35,6 @@ class classic_dpor final : public algorithm {
     config(const model::config &c)
         : maximum_total_execution_depth(c.maximum_total_execution_depth),
           stop_at_first_deadlock(c.stop_at_first_deadlock),
-          relinearize_traces(c.relinearize_traces),
-          use_optimal_linearization(c.use_optimal_linearization),
           policy(c.use_round_robin_scheduling
                      ? exploration_policy::round_robin
                      : exploration_policy::smallest_first) {}
@@ -48,8 +46,6 @@ class classic_dpor final : public algorithm {
         classic_dpor::default_coenabledness();
     uint32_t maximum_total_execution_depth = 1500;
     bool stop_at_first_deadlock = false;
-    bool relinearize_traces = false;
-    bool use_optimal_linearization = false;
     bool assumes_linear_program_flow = false;
     exploration_policy policy = exploration_policy::smallest_first;
   };
diff --git a/include/mcmini/model_checking/reporter.hpp b/include/mcmini/model_checking/reporter.hpp
index fa7fbb7..954d850 100644
--- a/include/mcmini/model_checking/reporter.hpp
+++ b/include/mcmini/model_checking/reporter.hpp
@@ -7,10 +7,19 @@ namespace model_checking {
 class reporter : public algorithm::callbacks {
 private:
   const bool verbose;
+  const bool relinearize_traces;
+  const bool use_optimal_linearization;
+
+private:
+  void dump_relinearized_trace(std::ostream &, const algorithm::context &,
+                               const stats &) const;
 
 public:
   reporter() = default;
-  reporter(const model::config &c) : verbose(c.verbose) {}
+  reporter(const model::config &c)
+      : verbose(c.verbose),
+        relinearize_traces(c.relinearize_traces || c.use_optimal_linearization),
+        use_optimal_linearization(c.use_optimal_linearization) {}
 
 public:
   // void crash(const algorithm::context &, const stats &) const override;
diff --git a/src/mcmini/model_checking/reporter.cpp b/src/mcmini/model_checking/reporter.cpp
index 902d38d..806959a 100644
--- a/src/mcmini/model_checking/reporter.cpp
+++ b/src/mcmini/model_checking/reporter.cpp
@@ -4,83 +4,96 @@
 using namespace model;
 using namespace model_checking;
 
+void reporter::dump_relinearized_trace(std::ostream &os,
+                                       const algorithm::context &c,
+                                       const stats &) const {
+  if (relinearize_traces) {
+    os << "\nRELINEARIZED TRACE\n";
+    for (const auto &t : c.linearize_trace(use_optimal_linearization)) {
+      os << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+    }
+  }
+}
+
 void reporter::trace_completed(const algorithm::context &c,
                                const stats &stats) const {
   if (!verbose)
     return;
-  std::stringstream ss;
-  ss << "TRACE " << stats.trace_id << "\n";
+  std::cout << "TRACE " << stats.trace_id << "\n";
   for (const auto &t : c.get_model().get_trace()) {
-    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+    std::cout << "thread " << t->get_executor() << ": " << t->to_string()
+              << "\n";
   }
-  ss << "\nNEXT THREAD OPERATIONS\n";
+  dump_relinearized_trace(std::cout, c, stats);
+  std::cout << "\nNEXT THREAD OPERATIONS\n";
   for (const auto &tpair : c.get_model().get_pending_transitions()) {
-    ss << "thread " << tpair.first << ": " << tpair.second->to_string() << "\n";
+    std::cout << "thread " << tpair.first << ": " << tpair.second->to_string()
+              << "\n";
   }
-  std::cout << ss.str();
   std::cout.flush();
 }
 
 void reporter::deadlock(const algorithm::context &c, const stats &stats) const {
-  std::cerr << "DEADLOCK" << std::endl;
-  std::stringstream ss;
+  std::cout << "DEADLOCK (trace ID: " << stats.trace_id << ")" << std::endl;
   for (const auto &t : c.get_model().get_trace()) {
-    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+    std::cout << "thread " << t->get_executor() << ": " << t->to_string()
+              << "\n";
   }
-  ss << "\nNEXT THREAD OPERATIONS\n";
+  dump_relinearized_trace(std::cout, c, stats);
+  std::cout << "\nNEXT THREAD OPERATIONS\n";
   for (const auto &tpair : c.get_model().get_pending_transitions()) {
-    ss << "thread " << tpair.first << ": " << tpair.second->to_string() << "\n";
+    std::cout << "thread " << tpair.first << ": " << tpair.second->to_string()
+              << "\n";
   }
-  std::cout << ss.str();
   std::cout.flush();
 }
 
 void reporter::undefined_behavior(
     const algorithm::context &c, const stats &stats,
     const undefined_behavior_exception &ub) const {
-  std::cerr << "UNDEFINED BEHAVIOR:\n" << ub.what() << std::endl;
-  std::stringstream ss;
-  ss << "TRACE " << stats.trace_id << "\n";
+  std::cout << "UNDEFINED BEHAVIOR:\n" << ub.what() << std::endl;
+  std::cout << "TRACE " << stats.trace_id << "\n";
   for (const auto &t : c.get_model().get_trace()) {
-    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+    std::cout << "thread " << t->get_executor() << ": " << t->to_string()
+              << "\n";
   }
-  ss << "\nNEXT THREAD OPERATIONS\n";
+  dump_relinearized_trace(std::cout, c, stats);
+  std::cout << "\nNEXT THREAD OPERATIONS\n";
   for (const auto &tpair : c.get_model().get_pending_transitions()) {
-    ss << "thread " << tpair.first << ": " << tpair.second->to_string() << "\n";
+    std::cout << "thread " << tpair.first << ": " << tpair.second->to_string()
+              << "\n";
   }
-  std::cout << ss.str();
   std::cout.flush();
 }
 
 void reporter::abnormal_termination(
     const algorithm::context &c, const stats &stats,
     const real_world::process::termination_error &ub) const {
-  std::cerr << "Abnormally Termination (signo: " << ub.signo
+  std::cout << "Abnormally Termination (signo: " << ub.signo
             << ", signal: " << sig_to_str.at(ub.signo) << "):\n"
             << ub.what() << std::endl;
 
-  std::stringstream ss;
-  ss << "TRACE " << stats.trace_id << "\n";
+  std::cout << "TRACE " << stats.trace_id << "\n";
   for (const auto &t : c.get_model().get_trace()) {
-    ss << "thread " << t->get_executor() << ": " << t->to_string() << "\n";
+    std::cout << "thread " << t->get_executor() << ": " << t->to_string()
+              << "\n";
   }
+  dump_relinearized_trace(std::cout, c, stats);
   const transition *terminator =
       c.get_model().get_pending_transition_for(ub.culprit);
-  ss << "thread " << terminator->get_executor() << ": "
-     << terminator->to_string() << "\n";
+  std::cout << "thread " << terminator->get_executor() << ": "
+            << terminator->to_string() << "\n";
 
-  ss << "\nNEXT THREAD OPERATIONS\n";
+  std::cout << "\nNEXT THREAD OPERATIONS\n";
   for (const auto &tpair : c.get_model().get_pending_transitions()) {
     if (tpair.first == terminator->get_executor()) {
-      ss << "thread " << tpair.first << ": executing"
-         << "\n";
+      std::cout << "thread " << tpair.first << ": executing"
+                << "\n";
     } else {
-      ss << "thread " << tpair.first << ": " << tpair.second->to_string()
-         << "\n";
+      std::cout << "thread " << tpair.first << ": " << tpair.second->to_string()
+                << "\n";
     }
   }
-  ss << stats.total_transitions + 1 << " total transitions executed"
-     << "\n";
-  std::cout << ss.str();
-  std::cout.flush();
+  std::cout << stats.total_transitions + 1 << " total transitions executed"
+            << std::endl;
 }
\ No newline at end of file

From 2e47c488f09f23997c722a063549661241769db5 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Fri, 19 Dec 2025 20:39:53 +0100
Subject: [PATCH 20/20] Remove unnecessary printfs from libmcmini

---
 src/lib/template/loop.c | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/lib/template/loop.c b/src/lib/template/loop.c
index c37dd55..b574322 100644
--- a/src/lib/template/loop.c
+++ b/src/lib/template/loop.c
@@ -75,7 +75,6 @@ int rt_sigqueueinfo(pid_t tgid, int sig, siginfo_t *info) {
 
 void mc_template_receive_sigchld(int sig, siginfo_t *info, void *) {
     assert(global_model_checker_pid != NO_DEFINED_MCMINI_PID);
-    printf("signalling!!\n");
     fsync(STDOUT_FILENO);
     int status;
     bool signal_mcmini = false;
@@ -92,12 +91,11 @@ void mc_template_receive_sigchld(int sig, siginfo_t *info, void *) {
     }
     else if (WIFSIGNALED(status)) {
       int signo = WTERMSIG(status);
-      printf("signaled %d", status);
+      // printf("signaled %d", status);
       fsync(STDOUT_FILENO);
       signal_mcmini = is_bad_signal(signo);
     }
     if (signal_mcmini) {
-      printf("signalling McMini!!\n");
       fsync(STDOUT_FILENO);
       // TODO: We can use `sigqueue(3)` to pass the exit status of
       // the child to the McMini process