src/mc/explo/udpor/ExtensionSetCalculator.cpp

   1 /* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "src/mc/explo/udpor/ExtensionSetCalculator.hpp"
   7 #include "src/mc/explo/udpor/Configuration.hpp"
   8 #include "src/mc/explo/udpor/History.hpp"
   9 #include "src/mc/explo/udpor/Unfolding.hpp"
  10
  11 #include <functional>
  12 #include <unordered_map>
  13 #include <xbt/asserts.h>
  14 #include <xbt/ex.h>
  15
  16 using namespace simgrid::mc;
  17
  18 namespace simgrid::mc::udpor {
  19
  20 EventSet ExtensionSetCalculator::partially_extend(const Configuration& C, Unfolding* U,
  21                                                   const std::shared_ptr<Transition> action)
  22 {
  23   using Action     = Transition::Type;
  24   using Handler    = std::function<EventSet(const Configuration&, Unfolding*, const std::shared_ptr<Transition>)>;
  25   using HandlerMap = std::unordered_map<Action, Handler>;
  26
  27   const static HandlerMap handlers =
  28       HandlerMap{{Action::COMM_ASYNC_RECV, &ExtensionSetCalculator::partially_extend_CommRecv},
  29                  {Action::COMM_ASYNC_SEND, &ExtensionSetCalculator::partially_extend_CommSend},
  30                  {Action::COMM_WAIT, &ExtensionSetCalculator::partially_extend_CommWait},
  31                  {Action::COMM_TEST, &ExtensionSetCalculator::partially_extend_CommTest},
  32                  {Action::MUTEX_ASYNC_LOCK, &ExtensionSetCalculator::partially_extend_MutexAsyncLock},
  33                  {Action::MUTEX_UNLOCK, &ExtensionSetCalculator::partially_extend_MutexUnlock},
  34                  {Action::MUTEX_WAIT, &ExtensionSetCalculator::partially_extend_MutexWait},
  35                  {Action::MUTEX_TEST, &ExtensionSetCalculator::partially_extend_MutexTest},
  36                  {Action::ACTOR_JOIN, &ExtensionSetCalculator::partially_extend_ActorJoin}};
  37
  38   if (const auto handler = handlers.find(action->type_); handler != handlers.end()) {
  39     return handler->second(C, U, std::move(action));
  40   } else {
  41     xbt_die("There is currently no specialized computation for the transition "
  42             "'%s' for computing extension sets in UDPOR, so the model checker cannot "
  43             "determine how to proceed. Please submit a bug report requesting "
  44             "that the transition be supported in SimGrid using UDPOR and consider "
  45             "using the other model-checking algorithms supported by SimGrid instead "
  46             "in the meantime",
  47             action->to_string().c_str());
  48   }
  49 }
  50
  51 EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& C, Unfolding* U,
  52                                                            const std::shared_ptr<Transition> action)
  53 {
  54   EventSet exC;
  55
  56   const auto send_action        = std::static_pointer_cast<CommSendTransition>(std::move(action));
  57   const auto pre_event_a_C      = C.pre_event(send_action->aid_);
  58   const unsigned sender_mailbox = send_action->get_mailbox();
  59
  60   // 1. Create `e' := <a, config(preEvt(a, C))>` and add `e'` to `ex(C)`
  61   // NOTE: If `preEvt(a, C)` doesn't exist, we're effectively asking
  62   // about `config({})`
  63   if (pre_event_a_C.has_value()) {
  64     const auto* e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), send_action);
  65     exC.insert(e_prime);
  66   } else {
  67     const auto* e_prime = U->discover_event(EventSet(), send_action);
  68     exC.insert(e_prime);
  69   }
  70
  71   // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
  72   // Com contains a matching c' = AsyncReceive(m, _) with `action`
  73   for (const auto e : C) {
  74     const bool transition_type_check = [&]() {
  75       if (const auto* async_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
  76           async_send != nullptr) {
  77         return async_send->get_mailbox() == sender_mailbox;
  78       }
  79       // TODO: Add `TestAny` dependency
  80       return false;
  81     }();
  82
  83     if (transition_type_check) {
  84       const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
  85
  86       // TODO: Check D_K(a, lambda(e)) (only matters in the case of CommTest)
  87       if (true) {
  88         const auto* e_prime = U->discover_event(std::move(K), send_action);
  89         exC.insert(e_prime);
  90       }
  91     }
  92   }
  93
  94   // TODO: Add `TestAny` dependency case
  95   return exC;
  96 }
  97
  98 EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& C, Unfolding* U,
  99                                                            const std::shared_ptr<Transition> action)
 100 {
 101   EventSet exC;
 102
 103   const auto recv_action      = std::static_pointer_cast<CommRecvTransition>(std::move(action));
 104   const unsigned recv_mailbox = recv_action->get_mailbox();
 105   const auto pre_event_a_C    = C.pre_event(recv_action->aid_);
 106
 107   // 1. Create `e' := <a, config(preEvt(a, C))>` and add `e'` to `ex(C)`
 108   if (pre_event_a_C.has_value()) {
 109     const auto* e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), recv_action);
 110     exC.insert(e_prime);
 111   } else {
 112     const auto* e_prime = U->discover_event(EventSet(), recv_action);
 113     exC.insert(e_prime);
 114   }
 115
 116   // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
 117   // Com contains a matching c' = AsyncReceive(m, _) with a
 118   for (const auto e : C) {
 119     const bool transition_type_check = [&]() {
 120       if (const auto* async_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 121           async_recv != nullptr && async_recv->get_mailbox() == recv_mailbox) {
 122         return true;
 123       }
 124       // TODO: Add `TestAny` dependency
 125       return false;
 126     }();
 127
 128     if (transition_type_check) {
 129       const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
 130
 131       // TODO: Check D_K(a, lambda(e)) (ony matters in the case of TestAny)
 132       if (true) {
 133         const auto* e_prime = U->discover_event(std::move(K), recv_action);
 134         exC.insert(e_prime);
 135       }
 136     }
 137   }
 138
 139   // TODO: Add `TestAny` dependency case
 140   return exC;
 141 }
 142
 143 EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& C, Unfolding* U,
 144                                                            std::shared_ptr<Transition> action)
 145 {
 146   EventSet exC;
 147
 148   const auto wait_action   = std::static_pointer_cast<CommWaitTransition>(std::move(action));
 149   const auto wait_comm     = wait_action->get_comm();
 150   const auto pre_event_a_C = C.pre_event(wait_action->aid_);
 151
 152   // Determine the _issuer_ of the communication of the `CommWait` event
 153   // in `C`. The issuer of the `CommWait` in `C` is the event in `C`
 154   // whose transition is the `CommRecv` or `CommSend` whose resulting
 155   // communication this `CommWait` waits on
 156   const auto issuer = std::find_if(C.begin(), C.end(), [&](const UnfoldingEvent* e) {
 157     if (const CommRecvTransition* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 158         e_issuer_receive != nullptr) {
 159       return e_issuer_receive->aid_ == wait_action->aid_ && wait_comm == e_issuer_receive->get_comm();
 160     }
 161
 162     if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 163         e_issuer_send != nullptr) {
 164       return e_issuer_send->aid_ == wait_action->aid_ && wait_comm == e_issuer_send->get_comm();
 165     }
 166
 167     return false;
 168   });
 169   xbt_assert(issuer != C.end(),
 170              "Invariant violation! A (supposedly) enabled `CommWait` transition "
 171              "waiting on communication %lu should not be enabled: the receive/send "
 172              "transition which generated the communication is not an action taken "
 173              "to reach state(C) (the state of the configuration), which should "
 174              "be an impossibility if `%s` is enabled. Please report this as "
 175              "a bug in SimGrid's UDPOR implementation",
 176              wait_action->get_comm(), wait_action->to_string(false).c_str());
 177   const UnfoldingEvent* e_issuer = *issuer;
 178   const History e_issuer_history(e_issuer);
 179
 180   // 1. if `a` is enabled at state(config({preEvt(a,C)})), then
 181   // create `e' := <a, config({preEvt(a,C)})>` and add `e'` to `ex(C)`
 182   //
 183   // First, if `pre_event_a_C == std::nullopt`, then there is nothing to
 184   // do: `CommWait` will never be enabled in the empty configuration (at
 185   // least two actions must be executed before)
 186   if (pre_event_a_C.has_value(); const auto* unwrapped_pre_event = pre_event_a_C.value()) {
 187     // A necessary condition is that the issuer be present in
 188     // config({preEvt(a, C)}); otherwise, the `CommWait` could not
 189     // be enabled since the communication on which it waits would not
 190     // have been created for it!
 191     if (const auto config_pre_event = History(unwrapped_pre_event); config_pre_event.contains(e_issuer)) {
 192       // If the issuer is a `CommRecv` (resp. `CommSend`), then we check that there
 193       // are at least as many `CommSend` (resp. `CommRecv`) transitions in `config_pre_event`
 194       // as needed to reach the receive/send number that is `issuer`.
 195       // ...
 196       // ...
 197       if (const CommRecvTransition* e_issuer_receive =
 198               dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 199           e_issuer_receive != nullptr) {
 200         const unsigned issuer_mailbox = e_issuer_receive->get_mailbox();
 201
 202         // Check from the config -> how many sends have there been
 203         const unsigned send_position =
 204             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
 205               const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 206               if (e_send != nullptr) {
 207                 return e_send->get_mailbox() == issuer_mailbox;
 208               }
 209               return false;
 210             });
 211
 212         // Check from e_issuer -> what place is the issuer in?
 213         const unsigned receive_position =
 214             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 215               const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 216               if (e_receive != nullptr) {
 217                 return e_receive->get_mailbox() == issuer_mailbox;
 218               }
 219               return false;
 220             });
 221
 222         if (send_position >= receive_position) {
 223           exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
 224         }
 225
 226       } else if (const CommSendTransition* e_issuer_send =
 227                      dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 228                  e_issuer_send != nullptr) {
 229         const unsigned issuer_mailbox = e_issuer_send->get_mailbox();
 230
 231         // Check from e_issuer -> what place is the issuer in?
 232         const unsigned send_position =
 233             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 234               const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 235               if (e_send != nullptr) {
 236                 return e_send->get_mailbox() == issuer_mailbox;
 237               }
 238               return false;
 239             });
 240
 241         // Check from the config -> how many sends have there been
 242         const unsigned receive_position =
 243             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
 244               const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 245               if (e_receive != nullptr) {
 246                 return e_receive->get_mailbox() == issuer_mailbox;
 247               }
 248               return false;
 249             });
 250
 251         if (send_position <= receive_position) {
 252           exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
 253         }
 254
 255       } else {
 256         xbt_die("The transition which created the communication on which `%s` waits "
 257                 "is neither an async send nor an async receive. The current UDPOR "
 258                 "implementation does not know how to check if `CommWait` is enabled in "
 259                 "this case. Was a new transition added?",
 260                 e_issuer->get_transition()->to_string().c_str());
 261       }
 262     }
 263   }
 264
 265   // 3. foreach event e in C do
 266   if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 267       e_issuer_send != nullptr) {
 268     for (const auto e : C) {
 269       // If the provider of the communication for `CommWait` is a
 270       // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
 271       // All other actions would be independent with the wait action (including
 272       // another `CommSend` to the same mailbox: `CommWait` is "waiting" for its
 273       // corresponding receive action)
 274       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_RECV) {
 275         continue;
 276       }
 277
 278       const auto issuer_mailbox        = e_issuer_send->get_mailbox();
 279       const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 280       if (e_recv->get_mailbox() != issuer_mailbox) {
 281         continue;
 282       }
 283
 284       // If the `issuer` is not in `config(K)`, this implies that
 285       // `WaitAny()` is always disabled in `config(K)`; hence, it
 286       // is independent of any transition in `config(K)` (according
 287       // to formal definition of independence)
 288       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 289       const auto config_K = History(K);
 290       if (not config_K.contains(e_issuer)) {
 291         continue;
 292       }
 293
 294       // What send # is the issuer
 295       const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 296         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 297         if (e_send != nullptr) {
 298           return e_send->get_mailbox() == issuer_mailbox;
 299         }
 300         return false;
 301       });
 302
 303       // What receive # is the event `e`?
 304       const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 305         const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 306         if (e_receive != nullptr) {
 307           return e_receive->get_mailbox() == issuer_mailbox;
 308         }
 309         return false;
 310       });
 311
 312       if (send_position == receive_position) {
 313         exC.insert(U->discover_event(std::move(K), wait_action));
 314       }
 315     }
 316   } else if (const CommRecvTransition* e_issuer_recv =
 317                  dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 318              e_issuer_recv != nullptr) {
 319     for (const auto e : C) {
 320       // If the provider of the communication for `CommWait` is a
 321       // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
 322       // All other actions would be independent with the wait action (including
 323       // another `CommRecv` to the same mailbox: `CommWait` is "waiting" for its
 324       // corresponding send action)
 325       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_SEND) {
 326         continue;
 327       }
 328
 329       const auto issuer_mailbox        = e_issuer_recv->get_mailbox();
 330       const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 331       if (e_send->get_mailbox() != issuer_mailbox) {
 332         continue;
 333       }
 334
 335       // If the `issuer` is not in `config(K)`, this implies that
 336       // `WaitAny()` is always disabled in `config(K)`; hence, it
 337       // is independent of any transition in `config(K)` (according
 338       // to formal definition of independence)
 339       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 340       const auto config_K = History(K);
 341       if (not config_K.contains(e_issuer)) {
 342         continue;
 343       }
 344
 345       // What receive # is the event `e`?
 346       const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 347         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 348         if (e_send != nullptr) {
 349           return e_send->get_mailbox() == issuer_mailbox;
 350         }
 351         return false;
 352       });
 353
 354       // What send # is the issuer
 355       const unsigned receive_position =
 356           std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 357             const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 358             if (e_receive != nullptr) {
 359               return e_receive->get_mailbox() == issuer_mailbox;
 360             }
 361             return false;
 362           });
 363
 364       if (send_position == receive_position) {
 365         exC.insert(U->discover_event(std::move(K), wait_action));
 366       }
 367     }
 368   } else {
 369     xbt_die("The transition which created the communication on which `%s` waits "
 370             "is neither an async send nor an async receive. The current UDPOR "
 371             "implementation does not know how to check if `CommWait` is enabled in "
 372             "this case. Was a new transition added?",
 373             e_issuer->get_transition()->to_string().c_str());
 374   }
 375
 376   return exC;
 377 }
 378
 379 EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration& C, Unfolding* U,
 380                                                            std::shared_ptr<Transition> action)
 381 {
 382   EventSet exC;
 383
 384   const auto test_action   = std::static_pointer_cast<CommTestTransition>(std::move(action));
 385   const auto test_comm     = test_action->get_comm();
 386   const auto test_aid      = test_action->aid_;
 387   const auto pre_event_a_C = C.pre_event(test_action->aid_);
 388
 389   // Add the previous event as a dependency (if it's there)
 390   if (pre_event_a_C.has_value()) {
 391     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), test_action);
 392     exC.insert(e_prime);
 393   }
 394
 395   // Determine the _issuer_ of the communication of the `CommTest` event
 396   // in `C`. The issuer of the `CommTest` in `C` is the event in `C`
 397   // whose transition is the `CommRecv` or `CommSend` whose resulting
 398   // communication this `CommTest` tests on
 399   const auto issuer = std::find_if(C.begin(), C.end(), [=](const UnfoldingEvent* e) {
 400     if (const CommRecvTransition* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 401         e_issuer_receive != nullptr) {
 402       return e_issuer_receive->aid_ == test_aid && test_comm == e_issuer_receive->get_comm();
 403     }
 404
 405     if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 406         e_issuer_send != nullptr) {
 407       return e_issuer_send->aid_ == test_aid && test_comm == e_issuer_send->get_comm();
 408     }
 409
 410     return false;
 411   });
 412   xbt_assert(issuer != C.end(),
 413              "An enabled `CommTest` transition (%s) is testing a communication"
 414              "%lu not created by a receive/send "
 415              "transition. SimGrid cannot currently handle test actions "
 416              "under which a test is performed on a communication that was "
 417              "not directly created by a receive/send operation of the same actor.",
 418              test_action->to_string(false).c_str(), test_action->get_comm());
 419   const UnfoldingEvent* e_issuer = *issuer;
 420   const History e_issuer_history(e_issuer);
 421
 422   // 3. foreach event e in C do
 423   if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 424       e_issuer_send != nullptr) {
 425     for (const auto e : C) {
 426       // If the provider of the communication for `CommTest` is a
 427       // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
 428       // All other actions would be independent with the test action (including
 429       // another `CommSend` to the same mailbox: `CommTest` is testing the
 430       // corresponding receive action)
 431       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_RECV) {
 432         continue;
 433       }
 434
 435       const auto issuer_mailbox = e_issuer_send->get_mailbox();
 436
 437       if (const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 438           e_recv->get_mailbox() != issuer_mailbox) {
 439         continue;
 440       }
 441
 442       // If the `issuer` is not in `config(K)`, this implies that
 443       // `CommTest()` is always disabled in `config(K)`; hence, it
 444       // is independent of any transition in `config(K)` (according
 445       // to formal definition of independence)
 446       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 447       const auto config_K = History(K);
 448       if (not config_K.contains(e_issuer)) {
 449         continue;
 450       }
 451
 452       // What send # is the issuer
 453       const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 454         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 455         if (e_send != nullptr) {
 456           return e_send->get_mailbox() == issuer_mailbox;
 457         }
 458         return false;
 459       });
 460
 461       // What receive # is the event `e`?
 462       const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 463         const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 464         if (e_receive != nullptr) {
 465           return e_receive->get_mailbox() == issuer_mailbox;
 466         }
 467         return false;
 468       });
 469
 470       if (send_position == receive_position) {
 471         exC.insert(U->discover_event(std::move(K), test_action));
 472       }
 473     }
 474   } else if (const CommRecvTransition* e_issuer_recv =
 475                  dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 476              e_issuer_recv != nullptr) {
 477
 478     for (const auto e : C) {
 479       // If the provider of the communication for `CommTest` is a
 480       // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
 481       // All other actions would be independent with the wait action (including
 482       // another `CommRecv` to the same mailbox: `CommWait` is "waiting" for its
 483       // corresponding send action)
 484       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_SEND) {
 485         continue;
 486       }
 487
 488       const auto issuer_mailbox        = e_issuer_recv->get_mailbox();
 489       const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 490       if (e_send->get_mailbox() != issuer_mailbox) {
 491         continue;
 492       }
 493
 494       // If the `issuer` is not in `config(K)`, this implies that
 495       // `WaitAny()` is always disabled in `config(K)`; hence, it
 496       // is independent of any transition in `config(K)` (according
 497       // to formal definition of independence)
 498       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 499       const auto config_K = History(K);
 500       if (not config_K.contains(e_issuer)) {
 501         continue;
 502       }
 503
 504       // What receive # is the event `e`?
 505       const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 506         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 507         if (e_send != nullptr) {
 508           return e_send->get_mailbox() == issuer_mailbox;
 509         }
 510         return false;
 511       });
 512
 513       // What send # is the issuer
 514       const unsigned receive_position =
 515           std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 516             const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 517             if (e_receive != nullptr) {
 518               return e_receive->get_mailbox() == issuer_mailbox;
 519             }
 520             return false;
 521           });
 522
 523       if (send_position == receive_position) {
 524         exC.insert(U->discover_event(std::move(K), test_action));
 525       }
 526     }
 527   } else {
 528     xbt_die("The transition which created the communication on which `%s` waits "
 529             "is neither an async send nor an async receive. The current UDPOR "
 530             "implementation does not know how to check if `CommWait` is enabled in "
 531             "this case. Was a new transition added?",
 532             e_issuer->get_transition()->to_string().c_str());
 533   }
 534   return exC;
 535 }
 536
 537 EventSet ExtensionSetCalculator::partially_extend_MutexAsyncLock(const Configuration& C, Unfolding* U,
 538                                                                  std::shared_ptr<Transition> action)
 539 {
 540   EventSet exC;
 541   const auto mutex_lock    = std::static_pointer_cast<MutexTransition>(std::move(action));
 542   const auto pre_event_a_C = C.pre_event(mutex_lock->aid_);
 543
 544   // for each event e in C
 545   // 1. If lambda(e) := pre(a) -> add it, otherwise don't bother if
 546   // it's not there
 547   if (pre_event_a_C.has_value()) {
 548     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_lock);
 549     exC.insert(e_prime);
 550   }
 551
 552   // for each event e in C
 553   for (const auto e : C) {
 554     // Check for other locks on the same mutex
 555     if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
 556         e_mutex != nullptr) {
 557
 558       if (e_mutex->type_ == Transition::Type::MUTEX_ASYNC_LOCK && mutex_lock->get_mutex() == e_mutex->get_mutex()) {
 559         const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
 560         exC.insert(U->discover_event(std::move(K), mutex_lock));
 561       }
 562     }
 563   }
 564   return exC;
 565 }
 566
 567 EventSet ExtensionSetCalculator::partially_extend_MutexUnlock(const Configuration& C, Unfolding* U,
 568                                                               std::shared_ptr<Transition> action)
 569 {
 570   EventSet exC;
 571   const auto mutex_unlock  = std::static_pointer_cast<MutexTransition>(std::move(action));
 572   const auto pre_event_a_C = C.pre_event(mutex_unlock->aid_);
 573
 574   // for each event e in C
 575   // 1. If lambda(e) := pre(a) -> add it, otherwise don't bother if
 576   // it's not there
 577   if (pre_event_a_C.has_value()) {
 578     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_unlock);
 579     exC.insert(e_prime);
 580   }
 581
 582   // for each event e in C
 583   for (const auto e : C) {
 584     // Check for MutexTest
 585     if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
 586         e_mutex != nullptr) {
 587
 588       if (e_mutex->type_ == Transition::Type::MUTEX_TEST || e_mutex->type_ == Transition::Type::MUTEX_WAIT) {
 589         // TODO: Check if dependent or not
 590         // This entails getting information about
 591         // the relative position of the mutex in the queue, which
 592         // again means we need more context...
 593         const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
 594         exC.insert(U->discover_event(std::move(K), mutex_unlock));
 595       }
 596     }
 597   }
 598   return exC;
 599 }
 600
 601 EventSet ExtensionSetCalculator::partially_extend_MutexWait(const Configuration& C, Unfolding* U,
 602                                                             std::shared_ptr<Transition> action)
 603 {
 604   return EventSet();
 605 }
 606
 607 EventSet ExtensionSetCalculator::partially_extend_MutexTest(const Configuration& C, Unfolding* U,
 608                                                             std::shared_ptr<Transition> action)
 609 {
 610   return EventSet();
 611 }
 612
 613 EventSet ExtensionSetCalculator::partially_extend_ActorJoin(const Configuration& C, Unfolding* U,
 614                                                             std::shared_ptr<Transition> action)
 615 {
 616   EventSet exC;
 617
 618   const auto join_action   = std::static_pointer_cast<ActorJoinTransition>(std::move(action));
 619   const auto pre_event_a_C = C.pre_event(join_action->aid_);
 620
 621   // Handling ActorJoin is very simple: it is independent with all
 622   // other transitions. Thus the only event it could possibly depend
 623   // on is pre(a, C) or the root
 624   if (pre_event_a_C.has_value()) {
 625     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), join_action);
 626     exC.insert(e_prime);
 627   } else {
 628     const auto e_prime = U->discover_event(EventSet(), join_action);
 629     exC.insert(e_prime);
 630   }
 631
 632   return exC;
 633 }
 634
 635 } // namespace simgrid::mc::udpor