Fix two off-by-one errors with clock vectors

Two errors were identified with managing clock
vectors in the Execution class. The index
assigned to the new transition was previously
`size() + 1` when it should have read `size()`.
Furthermore, the loop for checking "happens-between"
events excluded event 0. Both issues are now resolved
and a test with a race at the beginning was added
as verification

diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp
index fe84056..da252f3 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -21,9 +21,8 @@ void Execution::push_transition(const Transition* t)
     }
   }
   // The entry in the vector for `t->aid_` is the size
-  // of the new stack, which will have a size one greater
-  // than that before we insert the new events
-  max_clock_vector[t->aid_] = this->size() + 1;
+  // of the stack
+  max_clock_vector[t->aid_] = this->size();
   contents_.push_back(Event({t, max_clock_vector}));
 }
 
@@ -38,7 +37,7 @@ std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execu
   std::unordered_set<Execution::EventHandle> disqualified_events;
 
   // For each event of the execution
-  for (auto e_i = target; e_i > 0 && e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
+  for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
     // We need `e_i -->_E target` as a necessary condition
     if (not happens_before(e_i, target)) {
       continue;

diff --git a/src/mc/explo/odpor/Execution_test.cpp b/src/mc/explo/odpor/Execution_test.cpp
index 9033557..b233848 100644 (file)
--- a/src/mc/explo/odpor/Execution_test.cpp
+++ b/src/mc/explo/odpor/Execution_test.cpp
@@ -196,4 +196,22 @@ TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials")
       REQUIRE(initial_wrt_event2.value() == static_cast<aid_t>(3));
     }
   }
+
+  SECTION("Example 3: Testing 'Lock' Example")
+  {
+    const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+    const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+    const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+    const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+    const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+
+    Execution execution;
+    execution.push_transition(a1.get());
+    execution.push_transition(a2.get());
+    execution.push_transition(a3.get());
+    execution.push_transition(a4.get());
+    execution.push_transition(a5.get());
+
+    REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{0});
+  }
 }
\ No newline at end of file