Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Use the init-statement to reduce scope of local variables (Sonar).
authorArnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Tue, 27 Jun 2023 12:51:14 +0000 (14:51 +0200)
committerArnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Tue, 27 Jun 2023 15:15:12 +0000 (17:15 +0200)
src/mc/api/strategy/MaxMatchComm.hpp
src/mc/api/strategy/MinMatchComm.hpp
src/mc/explo/DFSExplorer.cpp
src/mc/explo/odpor/Execution.cpp
src/mc/explo/udpor/ExtensionSetCalculator.cpp

index 1f9a826..2f99c78 100644 (file)
@@ -49,9 +49,8 @@ public:
 
       int aid_value = value_of_state_;
       const Transition* transition = actor.get_transition(actor.get_times_considered()).get();
-     
-      const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
-      if (cast_recv != nullptr) {
+
+      if (auto const* cast_recv = dynamic_cast<CommRecvTransition const*>(transition)) {
          if (mailbox_.count(cast_recv->get_mailbox()) > 0 and
              mailbox_.at(cast_recv->get_mailbox()) > 0) { 
              aid_value--; // This means we have waiting recv corresponding to this recv
@@ -59,9 +58,8 @@ public:
              aid_value++; 
          }
       }
-   
-      const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
-      if (cast_send != nullptr) {
+
+      if (auto const* cast_send = dynamic_cast<CommSendTransition const*>(transition)) {
          if (mailbox_.count(cast_send->get_mailbox()) > 0 and
              mailbox_.at(cast_send->get_mailbox()) < 0) {
              aid_value--; // This means we have waiting recv corresponding to this send
@@ -69,25 +67,22 @@ public:
              aid_value++;
          }
       }
-   
+
       if (aid_value < min_found.second)
          min_found = std::make_pair(aid, aid_value);
     }
     return min_found;
   }
 
-
   void execute_next(aid_t aid, RemoteApp& app) override
   {
     const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered()).get();
     last_transition_             = transition->type_;
 
-    const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
-    if (cast_recv != nullptr)
+    if (auto const* cast_recv = dynamic_cast<CommRecvTransition const*>(transition))
       last_mailbox_ = cast_recv->get_mailbox();
 
-    const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
-    if (cast_send != nullptr)
+    if (auto const* cast_send = dynamic_cast<CommSendTransition const*>(transition))
       last_mailbox_ = cast_send->get_mailbox();
   }
 };
index 607a0a0..9041937 100644 (file)
@@ -54,23 +54,21 @@ public:
       int aid_value = value_of_state_;
       const Transition* transition = actor.get_transition(actor.get_times_considered()).get();
 
-      const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
-      if (cast_recv != nullptr) {
+      if (auto const* cast_recv = dynamic_cast<CommRecvTransition const*>(transition)) {
          if ((mailbox_.count(cast_recv->get_mailbox()) > 0 and
               mailbox_.at(cast_recv->get_mailbox()) <= 0) or mailbox_.count(cast_recv->get_mailbox()) == 0) 
              aid_value--; // This means we don't have waiting recv corresponding to this recv
          else 
              aid_value++; 
       }
-      const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
-      if (cast_send != nullptr) {
+      if (auto const* cast_send = dynamic_cast<CommSendTransition const*>(transition)) {
          if ((mailbox_.count(cast_send->get_mailbox()) > 0 and
               mailbox_.at(cast_send->get_mailbox()) >= 0) or mailbox_.count(cast_send->get_mailbox()) == 0)
              aid_value--;
          else
              aid_value++;
       }
-      
+
       if (aid_value < min_found.second)
          min_found = std::make_pair(aid, aid_value);
     }
@@ -83,12 +81,10 @@ public:
       const Transition* transition = actors_to_run_.at(aid).get_transition(actors_to_run_.at(aid).get_times_considered()).get();
     last_transition_             = transition->type_;
 
-    const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
-    if (cast_recv != nullptr)
+    if (auto const* cast_recv = dynamic_cast<CommRecvTransition const*>(transition))
       last_mailbox_ = cast_recv->get_mailbox();
 
-    const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
-    if (cast_send != nullptr)
+    if (auto const* cast_send = dynamic_cast<CommSendTransition const*>(transition))
       last_mailbox_ = cast_send->get_mailbox();
   }
 };
index 5bf8cd0..80bd804 100644 (file)
@@ -428,8 +428,7 @@ void DFSExplorer::backtrack()
         XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime);
         State& prev_state = *stack_[e];
         if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) {
-          const auto result = prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e));
-          switch (result) {
+          switch (prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e))) {
             case odpor::WakeupTree::InsertionResult::root: {
               XBT_DEBUG("ODPOR: Reversible race with `%u` unaccounted for in the wakeup tree for "
                         "the execution prior to event `%u`:",
index ef10e4f..1ac75ce 100644 (file)
@@ -412,10 +412,8 @@ std::optional<PartialExecution> Execution::get_shortest_odpor_sq_subset_insertio
   auto w_now = w;
 
   for (const auto& next_E_p : v) {
-    const aid_t p = next_E_p->aid_;
-
     // Is `p in `I_[E](w)`?
-    if (E_v.is_initial_after_execution_of(w_now, p)) {
+    if (const aid_t p = next_E_p->aid_; E_v.is_initial_after_execution_of(w_now, p)) {
       // Remove `p` from w and continue
 
       // INVARIANT: If `p` occurs in `w`, it had better refer to the same
@@ -487,4 +485,4 @@ bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::Even
   return false;
 }
 
-} // namespace simgrid::mc::odpor
\ No newline at end of file
+} // namespace simgrid::mc::odpor
index e2e2e67..0884ee5 100644 (file)
@@ -72,8 +72,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration&
   // Com contains a matching c' = AsyncReceive(m, _) with `action`
   for (const auto e : C) {
     const bool transition_type_check = [&]() {
-      if (const auto* async_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
-          async_send != nullptr) {
+      if (const auto* async_send = dynamic_cast<const CommSendTransition*>(e->get_transition())) {
         return async_send->get_mailbox() == sender_mailbox;
       }
       // TODO: Add `TestAny` dependency
@@ -152,13 +151,11 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
   // whose transition is the `CommRecv` or `CommSend` whose resulting
   // communication this `CommWait` waits on
   const auto issuer = std::find_if(C.begin(), C.end(), [&](const UnfoldingEvent* e) {
-    if (const CommRecvTransition* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
-        e_issuer_receive != nullptr) {
+    if (const auto* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition())) {
       return e_issuer_receive->aid_ == wait_action->aid_ && wait_comm == e_issuer_receive->get_comm();
     }
 
-    if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
-        e_issuer_send != nullptr) {
+    if (const auto* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition())) {
       return e_issuer_send->aid_ == wait_action->aid_ && wait_comm == e_issuer_send->get_comm();
     }
 
@@ -192,16 +189,13 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
       // as needed to reach the receive/send number that is `issuer`.
       // ...
       // ...
-      if (const CommRecvTransition* e_issuer_receive =
-              dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
-          e_issuer_receive != nullptr) {
+      if (const auto* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition())) {
         const unsigned issuer_mailbox = e_issuer_receive->get_mailbox();
 
         // Check from the config -> how many sends have there been
         const unsigned send_position =
             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
-              const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
-              if (e_send != nullptr) {
+              if (const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition())) {
                 return e_send->get_mailbox() == issuer_mailbox;
               }
               return false;
@@ -210,8 +204,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
         // Check from e_issuer -> what place is the issuer in?
         const unsigned receive_position =
             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
-              const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
-              if (e_receive != nullptr) {
+              if (const auto* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition())) {
                 return e_receive->get_mailbox() == issuer_mailbox;
               }
               return false;
@@ -221,16 +214,13 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
           exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
         }
 
-      } else if (const CommSendTransition* e_issuer_send =
-                     dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
-                 e_issuer_send != nullptr) {
+      } else if (const auto* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition())) {
         const unsigned issuer_mailbox = e_issuer_send->get_mailbox();
 
         // Check from e_issuer -> what place is the issuer in?
         const unsigned send_position =
             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
-              const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
-              if (e_send != nullptr) {
+              if (const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition())) {
                 return e_send->get_mailbox() == issuer_mailbox;
               }
               return false;
@@ -239,8 +229,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
         // Check from the config -> how many sends have there been
         const unsigned receive_position =
             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
-              const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
-              if (e_receive != nullptr) {
+              if (const auto* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition())) {
                 return e_receive->get_mailbox() == issuer_mailbox;
               }
               return false;
@@ -261,8 +250,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
   }
 
   // 3. foreach event e in C do
-  if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
-      e_issuer_send != nullptr) {
+  if (const auto* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition())) {
     for (const auto e : C) {
       // If the provider of the communication for `CommWait` is a
       // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
@@ -274,8 +262,8 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
       }
 
       const auto issuer_mailbox        = e_issuer_send->get_mailbox();
-      const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
-      if (e_recv->get_mailbox() != issuer_mailbox) {
+      if (const auto* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
+          e_recv->get_mailbox() != issuer_mailbox) {
         continue;
       }
 
@@ -291,8 +279,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
 
       // What send # is the issuer
       const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
-        const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
-        if (e_send != nullptr) {
+        if (const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition())) {
           return e_send->get_mailbox() == issuer_mailbox;
         }
         return false;
@@ -300,8 +287,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
 
       // What receive # is the event `e`?
       const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
-        const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
-        if (e_receive != nullptr) {
+        if (const auto* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition())) {
           return e_receive->get_mailbox() == issuer_mailbox;
         }
         return false;
@@ -311,9 +297,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
         exC.insert(U->discover_event(std::move(K), wait_action));
       }
     }
-  } else if (const CommRecvTransition* e_issuer_recv =
-                 dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
-             e_issuer_recv != nullptr) {
+  } else if (const auto* e_issuer_recv = dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition())) {
     for (const auto e : C) {
       // If the provider of the communication for `CommWait` is a
       // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
@@ -325,8 +309,8 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
       }
 
       const auto issuer_mailbox        = e_issuer_recv->get_mailbox();
-      const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
-      if (e_send->get_mailbox() != issuer_mailbox) {
+      if (const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
+          e_send->get_mailbox() != issuer_mailbox) {
         continue;
       }
 
@@ -342,8 +326,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
 
       // What receive # is the event `e`?
       const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
-        const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
-        if (e_send != nullptr) {
+        if (const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition())) {
           return e_send->get_mailbox() == issuer_mailbox;
         }
         return false;
@@ -352,8 +335,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
       // What send # is the issuer
       const unsigned receive_position =
           std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
-            const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
-            if (e_receive != nullptr) {
+            if (const auto* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition())) {
               return e_receive->get_mailbox() == issuer_mailbox;
             }
             return false;
@@ -395,13 +377,11 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&
   // whose transition is the `CommRecv` or `CommSend` whose resulting
   // communication this `CommTest` tests on
   const auto issuer = std::find_if(C.begin(), C.end(), [=](const UnfoldingEvent* e) {
-    if (const CommRecvTransition* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
-        e_issuer_receive != nullptr) {
+    if (const auto* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition())) {
       return e_issuer_receive->aid_ == test_aid && test_comm == e_issuer_receive->get_comm();
     }
 
-    if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
-        e_issuer_send != nullptr) {
+    if (const auto* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition())) {
       return e_issuer_send->aid_ == test_aid && test_comm == e_issuer_send->get_comm();
     }
 
@@ -418,8 +398,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&
   const History e_issuer_history(e_issuer);
 
   // 3. foreach event e in C do
-  if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
-      e_issuer_send != nullptr) {
+  if (const auto* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition())) {
     for (const auto e : C) {
       // If the provider of the communication for `CommTest` is a
       // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
@@ -432,7 +411,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&
 
       const auto issuer_mailbox = e_issuer_send->get_mailbox();
 
-      if (const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
+      if (const auto* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
           e_recv->get_mailbox() != issuer_mailbox) {
         continue;
       }
@@ -449,8 +428,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&
 
       // What send # is the issuer
       const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
-        const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
-        if (e_send != nullptr) {
+        if (const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition())) {
           return e_send->get_mailbox() == issuer_mailbox;
         }
         return false;
@@ -458,8 +436,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&
 
       // What receive # is the event `e`?
       const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
-        const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
-        if (e_receive != nullptr) {
+        if (const auto* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition())) {
           return e_receive->get_mailbox() == issuer_mailbox;
         }
         return false;
@@ -469,9 +446,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&
         exC.insert(U->discover_event(std::move(K), test_action));
       }
     }
-  } else if (const CommRecvTransition* e_issuer_recv =
-                 dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
-             e_issuer_recv != nullptr) {
+  } else if (const auto* e_issuer_recv = dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition())) {
     for (const auto e : C) {
       // If the provider of the communication for `CommTest` is a
       // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
@@ -483,8 +458,8 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&
       }
 
       const auto issuer_mailbox        = e_issuer_recv->get_mailbox();
-      const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
-      if (e_send->get_mailbox() != issuer_mailbox) {
+      if (const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
+          e_send->get_mailbox() != issuer_mailbox) {
         continue;
       }
 
@@ -500,8 +475,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&
 
       // What receive # is the event `e`?
       const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
-        const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
-        if (e_send != nullptr) {
+        if (const auto* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition())) {
           return e_send->get_mailbox() == issuer_mailbox;
         }
         return false;
@@ -510,8 +484,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&
       // What send # is the issuer
       const unsigned receive_position =
           std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
-            const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
-            if (e_receive != nullptr) {
+            if (const auto* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition())) {
               return e_receive->get_mailbox() == issuer_mailbox;
             }
             return false;
@@ -553,12 +526,10 @@ EventSet ExtensionSetCalculator::partially_extend_MutexAsyncLock(const Configura
   // for each event e in C
   for (const auto e : C) {
     // Check for other locks on the same mutex
-    if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
-        e_mutex != nullptr) {
-      if (e_mutex->type_ == Transition::Type::MUTEX_ASYNC_LOCK && mutex_lock->get_mutex() == e_mutex->get_mutex()) {
-        const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
-        exC.insert(U->discover_event(std::move(K), mutex_lock));
-      }
+    if (const auto* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
+        e_mutex->type_ == Transition::Type::MUTEX_ASYNC_LOCK && mutex_lock->get_mutex() == e_mutex->get_mutex()) {
+      const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+      exC.insert(U->discover_event(std::move(K), mutex_lock));
     }
   }
   return exC;
@@ -586,16 +557,14 @@ EventSet ExtensionSetCalculator::partially_extend_MutexUnlock(const Configuratio
   // for each event e in C
   for (const auto e : C) {
     // Check for MutexTest
-    if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
-        e_mutex != nullptr) {
-      if (e_mutex->type_ == Transition::Type::MUTEX_TEST || e_mutex->type_ == Transition::Type::MUTEX_WAIT) {
-        // TODO: Check if dependent or not
-        // This entails getting information about
-        // the relative position of the mutex in the queue, which
-        // again means we need more context...
-        const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
-        exC.insert(U->discover_event(std::move(K), mutex_unlock));
-      }
+    if (const auto* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
+        e_mutex->type_ == Transition::Type::MUTEX_TEST || e_mutex->type_ == Transition::Type::MUTEX_WAIT) {
+      // TODO: Check if dependent or not
+      // This entails getting information about
+      // the relative position of the mutex in the queue, which
+      // again means we need more context...
+      const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+      exC.insert(U->discover_event(std::move(K), mutex_unlock));
     }
   }
   return exC;
@@ -622,7 +591,7 @@ EventSet ExtensionSetCalculator::partially_extend_MutexWait(const Configuration&
   // for each event e in C
   for (const auto e : C) {
     // Check for any unlocks
-    if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
+    if (const auto* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
         e_mutex != nullptr && e_mutex->type_ == Transition::Type::MUTEX_UNLOCK) {
       // TODO: Check if dependent or not
       // This entails getting information about
@@ -644,7 +613,7 @@ EventSet ExtensionSetCalculator::partially_extend_MutexTest(const Configuration&
 
   // for each event e in C
   // 1. If lambda(e) := pre(a) -> add it. Note that if
-  // pre_evevnt_a_C.has_value() == false, this implies `C` is
+  // pre_event_a_C.has_value() == false, this implies `C` is
   // empty or which we treat as implicitly containing the bottom event
   if (pre_event_a_C.has_value()) {
     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_test);
@@ -657,7 +626,7 @@ EventSet ExtensionSetCalculator::partially_extend_MutexTest(const Configuration&
   // for each event e in C
   for (const auto e : C) {
     // Check for any unlocks
-    if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
+    if (const auto* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
         e_mutex != nullptr && e_mutex->type_ == Transition::Type::MUTEX_UNLOCK) {
       // TODO: Check if dependent or not
       // This entails getting information about