Merge branch 'master' of https://framagit.org/mwapl/simgrid

[simgrid.git] / src / mc / explo / udpor / ExtensionSetCalculator.cpp

diff --git a/src/mc/explo/udpor/ExtensionSetCalculator.cpp b/src/mc/explo/udpor/ExtensionSetCalculator.cpp
index f8c4bac55971a9f95081653835b35592460adc44..491ec2d9e5adb157fa27698eaa4cd4a4bac7473b 100644 (file)
--- a/src/mc/explo/udpor/ExtensionSetCalculator.cpp
+++ b/src/mc/explo/udpor/ExtensionSetCalculator.cpp
@@ -115,7 +115,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration&
   // Com contains a matching c' = AsyncReceive(m, _) with a
   for (const auto e : C) {
     const bool transition_type_check = [&]() {
-      if (const auto* async_recv = dynamic_cast<const CommSendTransition*>(e->get_transition());
+      if (const auto* async_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
           async_recv != nullptr && async_recv->get_mailbox() == recv_mailbox) {
         return true;
       }
@@ -151,15 +151,15 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
   // in `C`. The issuer of the `CommWait` in `C` is the event in `C`
   // 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) {
+  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) {
-      return wait_comm == e_issuer_receive->get_comm();
+      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) {
-      return wait_comm == e_issuer_send->get_comm();
+      return e_issuer_send->aid_ == wait_action->aid_ && wait_comm == e_issuer_send->get_comm();
     }
 
     return false;
@@ -182,7 +182,6 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
   // do: `CommWait` will never be enabled in the empty configuration (at
   // least two actions must be executed before)
   if (pre_event_a_C.has_value(); const auto unwrapped_pre_event = pre_event_a_C.value()) {
-
     // A necessary condition is that the issuer be present in
     // config({preEvt(a, C)}); otherwise, the `CommWait` could not
     // be enabled since the communication on which it waits would not
@@ -196,7 +195,6 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
       if (const CommRecvTransition* e_issuer_receive =
               dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
           e_issuer_receive != nullptr) {
-
         const unsigned issuer_mailbox = e_issuer_receive->get_mailbox();
 
         // Check from the config -> how many sends have there been
@@ -226,7 +224,6 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
       } else if (const CommSendTransition* e_issuer_send =
                      dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
                  e_issuer_send != nullptr) {
-
         const unsigned issuer_mailbox = e_issuer_send->get_mailbox();
 
         // Check from e_issuer -> what place is the issuer in?
@@ -268,7 +265,6 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
   for (const auto e : C) {
     if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
         e_issuer_send != nullptr) {
-
       // If the provider of the communication for `CommWait` is a
       // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
       // All other actions would be independent with the wait action (including
@@ -321,7 +317,6 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
     } else if (const CommRecvTransition* e_issuer_recv =
                    dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
                e_issuer_recv != nullptr) {
-
       // If the provider of the communication for `CommWait` is a
       // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
       // All other actions would be independent with the wait action (including
@@ -331,7 +326,7 @@ EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&
         continue;
       }
 
-      const auto issuer_mailbox        = e_issuer_send->get_mailbox();
+      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) {
         continue;
@@ -381,4 +376,4 @@ EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&
   return EventSet();
 }
 
-} // namespace simgrid::mc::udpor
\ No newline at end of file
+} // namespace simgrid::mc::udpor