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       const auto e_prime = U->discover_event(std::move(K), send_action);
  88       exC.insert(e_prime);
  89     }
  90   }
  91
  92   // TODO: Add `TestAny` dependency case
  93   return exC;
  94 }
  95
  96 EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& C, Unfolding* U,
  97                                                            const std::shared_ptr<Transition> action)
  98 {
  99   EventSet exC;
 100
 101   const auto recv_action      = std::static_pointer_cast<CommRecvTransition>(std::move(action));
 102   const unsigned recv_mailbox = recv_action->get_mailbox();
 103   const auto pre_event_a_C    = C.pre_event(recv_action->aid_);
 104
 105   // 1. Create `e' := <a, config(preEvt(a, C))>` and add `e'` to `ex(C)`
 106   if (pre_event_a_C.has_value()) {
 107     const auto* e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), recv_action);
 108     exC.insert(e_prime);
 109   } else {
 110     const auto* e_prime = U->discover_event(EventSet(), recv_action);
 111     exC.insert(e_prime);
 112   }
 113
 114   // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
 115   // Com contains a matching c' = AsyncReceive(m, _) with a
 116   for (const auto e : C) {
 117     const bool transition_type_check = [&]() {
 118       if (const auto* async_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 119           async_recv != nullptr && async_recv->get_mailbox() == recv_mailbox) {
 120         return true;
 121       }
 122       // TODO: Add `TestAny` dependency
 123       return false;
 124     }();
 125
 126     if (transition_type_check) {
 127       const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
 128
 129       // TODO: Check D_K(a, lambda(e)) (ony matters in the case of TestAny)
 130       if (true) {
 131         const auto* e_prime = U->discover_event(std::move(K), recv_action);
 132         exC.insert(e_prime);
 133       }
 134     }
 135   }
 136
 137   // TODO: Add `TestAny` dependency case
 138   return exC;
 139 }
 140
 141 EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& C, Unfolding* U,
 142                                                            std::shared_ptr<Transition> action)
 143 {
 144   EventSet exC;
 145
 146   const auto wait_action   = std::static_pointer_cast<CommWaitTransition>(std::move(action));
 147   const auto wait_comm     = wait_action->get_comm();
 148   const auto pre_event_a_C = C.pre_event(wait_action->aid_);
 149
 150   // Determine the _issuer_ of the communication of the `CommWait` event
 151   // in `C`. The issuer of the `CommWait` in `C` is the event in `C`
 152   // whose transition is the `CommRecv` or `CommSend` whose resulting
 153   // communication this `CommWait` waits on
 154   const auto issuer = std::find_if(C.begin(), C.end(), [&](const UnfoldingEvent* e) {
 155     if (const CommRecvTransition* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 156         e_issuer_receive != nullptr) {
 157       return e_issuer_receive->aid_ == wait_action->aid_ && wait_comm == e_issuer_receive->get_comm();
 158     }
 159
 160     if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 161         e_issuer_send != nullptr) {
 162       return e_issuer_send->aid_ == wait_action->aid_ && wait_comm == e_issuer_send->get_comm();
 163     }
 164
 165     return false;
 166   });
 167   xbt_assert(issuer != C.end(),
 168              "Invariant violation! A (supposedly) enabled `CommWait` transition "
 169              "waiting on communication %u should not be enabled: the receive/send "
 170              "transition which generated the communication is not an action taken "
 171              "to reach state(C) (the state of the configuration), which should "
 172              "be an impossibility if `%s` is enabled. Please report this as "
 173              "a bug in SimGrid's UDPOR implementation",
 174              wait_action->get_comm(), wait_action->to_string(false).c_str());
 175   const UnfoldingEvent* e_issuer = *issuer;
 176   const History e_issuer_history(e_issuer);
 177
 178   // 1. if `a` is enabled at state(config({preEvt(a,C)})), then
 179   // create `e' := <a, config({preEvt(a,C)})>` and add `e'` to `ex(C)`
 180   //
 181   // First, if `pre_event_a_C == std::nullopt`, then there is nothing to
 182   // do: `CommWait` will never be enabled in the empty configuration (at
 183   // least two actions must be executed before)
 184   if (pre_event_a_C.has_value(); const auto* unwrapped_pre_event = pre_event_a_C.value()) {
 185     // A necessary condition is that the issuer be present in
 186     // config({preEvt(a, C)}); otherwise, the `CommWait` could not
 187     // be enabled since the communication on which it waits would not
 188     // have been created for it!
 189     if (const auto config_pre_event = History(unwrapped_pre_event); config_pre_event.contains(e_issuer)) {
 190       // If the issuer is a `CommRecv` (resp. `CommSend`), then we check that there
 191       // are at least as many `CommSend` (resp. `CommRecv`) transitions in `config_pre_event`
 192       // as needed to reach the receive/send number that is `issuer`.
 193       // ...
 194       // ...
 195       if (const CommRecvTransition* e_issuer_receive =
 196               dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 197           e_issuer_receive != nullptr) {
 198         const unsigned issuer_mailbox = e_issuer_receive->get_mailbox();
 199
 200         // Check from the config -> how many sends have there been
 201         const unsigned send_position =
 202             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
 203               const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 204               if (e_send != nullptr) {
 205                 return e_send->get_mailbox() == issuer_mailbox;
 206               }
 207               return false;
 208             });
 209
 210         // Check from e_issuer -> what place is the issuer in?
 211         const unsigned receive_position =
 212             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 213               const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 214               if (e_receive != nullptr) {
 215                 return e_receive->get_mailbox() == issuer_mailbox;
 216               }
 217               return false;
 218             });
 219
 220         if (send_position >= receive_position) {
 221           exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
 222         }
 223
 224       } else if (const CommSendTransition* e_issuer_send =
 225                      dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 226                  e_issuer_send != nullptr) {
 227         const unsigned issuer_mailbox = e_issuer_send->get_mailbox();
 228
 229         // Check from e_issuer -> what place is the issuer in?
 230         const unsigned send_position =
 231             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 232               const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 233               if (e_send != nullptr) {
 234                 return e_send->get_mailbox() == issuer_mailbox;
 235               }
 236               return false;
 237             });
 238
 239         // Check from the config -> how many sends have there been
 240         const unsigned receive_position =
 241             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
 242               const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 243               if (e_receive != nullptr) {
 244                 return e_receive->get_mailbox() == issuer_mailbox;
 245               }
 246               return false;
 247             });
 248
 249         if (send_position <= receive_position) {
 250           exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
 251         }
 252
 253       } else {
 254         xbt_die("The transition which created the communication on which `%s` waits "
 255                 "is neither an async send nor an async receive. The current UDPOR "
 256                 "implementation does not know how to check if `CommWait` is enabled in "
 257                 "this case. Was a new transition added?",
 258                 e_issuer->get_transition()->to_string().c_str());
 259       }
 260     }
 261   }
 262
 263   // 3. foreach event e in C do
 264   if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 265       e_issuer_send != nullptr) {
 266     for (const auto e : C) {
 267       // If the provider of the communication for `CommWait` is a
 268       // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
 269       // All other actions would be independent with the wait action (including
 270       // another `CommSend` to the same mailbox: `CommWait` is "waiting" for its
 271       // corresponding receive action)
 272       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_RECV) {
 273         continue;
 274       }
 275
 276       const auto issuer_mailbox        = e_issuer_send->get_mailbox();
 277       const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 278       if (e_recv->get_mailbox() != issuer_mailbox) {
 279         continue;
 280       }
 281
 282       // If the `issuer` is not in `config(K)`, this implies that
 283       // `WaitAny()` is always disabled in `config(K)`; hence, it
 284       // is independent of any transition in `config(K)` (according
 285       // to formal definition of independence)
 286       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 287       const auto config_K = History(K);
 288       if (not config_K.contains(e_issuer)) {
 289         continue;
 290       }
 291
 292       // What send # is the issuer
 293       const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 294         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 295         if (e_send != nullptr) {
 296           return e_send->get_mailbox() == issuer_mailbox;
 297         }
 298         return false;
 299       });
 300
 301       // What receive # is the event `e`?
 302       const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 303         const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 304         if (e_receive != nullptr) {
 305           return e_receive->get_mailbox() == issuer_mailbox;
 306         }
 307         return false;
 308       });
 309
 310       if (send_position == receive_position) {
 311         exC.insert(U->discover_event(std::move(K), wait_action));
 312       }
 313     }
 314   } else if (const CommRecvTransition* e_issuer_recv =
 315                  dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 316              e_issuer_recv != nullptr) {
 317     for (const auto e : C) {
 318       // If the provider of the communication for `CommWait` is a
 319       // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
 320       // All other actions would be independent with the wait action (including
 321       // another `CommRecv` to the same mailbox: `CommWait` is "waiting" for its
 322       // corresponding send action)
 323       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_SEND) {
 324         continue;
 325       }
 326
 327       const auto issuer_mailbox        = e_issuer_recv->get_mailbox();
 328       const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 329       if (e_send->get_mailbox() != issuer_mailbox) {
 330         continue;
 331       }
 332
 333       // If the `issuer` is not in `config(K)`, this implies that
 334       // `WaitAny()` is always disabled in `config(K)`; hence, it
 335       // is independent of any transition in `config(K)` (according
 336       // to formal definition of independence)
 337       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 338       const auto config_K = History(K);
 339       if (not config_K.contains(e_issuer)) {
 340         continue;
 341       }
 342
 343       // What receive # is the event `e`?
 344       const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 345         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 346         if (e_send != nullptr) {
 347           return e_send->get_mailbox() == issuer_mailbox;
 348         }
 349         return false;
 350       });
 351
 352       // What send # is the issuer
 353       const unsigned receive_position =
 354           std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 355             const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 356             if (e_receive != nullptr) {
 357               return e_receive->get_mailbox() == issuer_mailbox;
 358             }
 359             return false;
 360           });
 361
 362       if (send_position == receive_position) {
 363         exC.insert(U->discover_event(std::move(K), wait_action));
 364       }
 365     }
 366   } else {
 367     xbt_die("The transition which created the communication on which `%s` waits "
 368             "is neither an async send nor an async receive. The current UDPOR "
 369             "implementation does not know how to check if `CommWait` is enabled in "
 370             "this case. Was a new transition added?",
 371             e_issuer->get_transition()->to_string().c_str());
 372   }
 373
 374   return exC;
 375 }
 376
 377 EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration& C, Unfolding* U,
 378                                                            std::shared_ptr<Transition> action)
 379 {
 380   EventSet exC;
 381
 382   const auto test_action   = std::static_pointer_cast<CommTestTransition>(std::move(action));
 383   const auto test_comm     = test_action->get_comm();
 384   const auto test_aid      = test_action->aid_;
 385   const auto pre_event_a_C = C.pre_event(test_action->aid_);
 386
 387   // Add the previous event as a dependency (if it's there)
 388   if (pre_event_a_C.has_value()) {
 389     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), test_action);
 390     exC.insert(e_prime);
 391   }
 392
 393   // Determine the _issuer_ of the communication of the `CommTest` event
 394   // in `C`. The issuer of the `CommTest` in `C` is the event in `C`
 395   // whose transition is the `CommRecv` or `CommSend` whose resulting
 396   // communication this `CommTest` tests on
 397   const auto issuer = std::find_if(C.begin(), C.end(), [=](const UnfoldingEvent* e) {
 398     if (const CommRecvTransition* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 399         e_issuer_receive != nullptr) {
 400       return e_issuer_receive->aid_ == test_aid && test_comm == e_issuer_receive->get_comm();
 401     }
 402
 403     if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 404         e_issuer_send != nullptr) {
 405       return e_issuer_send->aid_ == test_aid && test_comm == e_issuer_send->get_comm();
 406     }
 407
 408     return false;
 409   });
 410   xbt_assert(issuer != C.end(),
 411              "An enabled `CommTest` transition (%s) is testing a communication"
 412              "%u not created by a receive/send "
 413              "transition. SimGrid cannot currently handle test actions "
 414              "under which a test is performed on a communication that was "
 415              "not directly created by a receive/send operation of the same actor.",
 416              test_action->to_string(false).c_str(), test_action->get_comm());
 417   const UnfoldingEvent* e_issuer = *issuer;
 418   const History e_issuer_history(e_issuer);
 419
 420   // 3. foreach event e in C do
 421   if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 422       e_issuer_send != nullptr) {
 423     for (const auto e : C) {
 424       // If the provider of the communication for `CommTest` is a
 425       // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
 426       // All other actions would be independent with the test action (including
 427       // another `CommSend` to the same mailbox: `CommTest` is testing the
 428       // corresponding receive action)
 429       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_RECV) {
 430         continue;
 431       }
 432
 433       const auto issuer_mailbox = e_issuer_send->get_mailbox();
 434
 435       if (const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 436           e_recv->get_mailbox() != issuer_mailbox) {
 437         continue;
 438       }
 439
 440       // If the `issuer` is not in `config(K)`, this implies that
 441       // `CommTest()` is always disabled in `config(K)`; hence, it
 442       // is independent of any transition in `config(K)` (according
 443       // to formal definition of independence)
 444       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 445       const auto config_K = History(K);
 446       if (not config_K.contains(e_issuer)) {
 447         continue;
 448       }
 449
 450       // What send # is the issuer
 451       const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 452         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 453         if (e_send != nullptr) {
 454           return e_send->get_mailbox() == issuer_mailbox;
 455         }
 456         return false;
 457       });
 458
 459       // What receive # is the event `e`?
 460       const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 461         const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 462         if (e_receive != nullptr) {
 463           return e_receive->get_mailbox() == issuer_mailbox;
 464         }
 465         return false;
 466       });
 467
 468       if (send_position == receive_position) {
 469         exC.insert(U->discover_event(std::move(K), test_action));
 470       }
 471     }
 472   } else if (const CommRecvTransition* e_issuer_recv =
 473                  dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 474              e_issuer_recv != nullptr) {
 475
 476     for (const auto e : C) {
 477       // If the provider of the communication for `CommTest` is a
 478       // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
 479       // All other actions would be independent with the wait action (including
 480       // another `CommRecv` to the same mailbox: `CommWait` is "waiting" for its
 481       // corresponding send action)
 482       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_SEND) {
 483         continue;
 484       }
 485
 486       const auto issuer_mailbox        = e_issuer_recv->get_mailbox();
 487       const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 488       if (e_send->get_mailbox() != issuer_mailbox) {
 489         continue;
 490       }
 491
 492       // If the `issuer` is not in `config(K)`, this implies that
 493       // `WaitAny()` is always disabled in `config(K)`; hence, it
 494       // is independent of any transition in `config(K)` (according
 495       // to formal definition of independence)
 496       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 497       const auto config_K = History(K);
 498       if (not config_K.contains(e_issuer)) {
 499         continue;
 500       }
 501
 502       // What receive # is the event `e`?
 503       const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 504         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 505         if (e_send != nullptr) {
 506           return e_send->get_mailbox() == issuer_mailbox;
 507         }
 508         return false;
 509       });
 510
 511       // What send # is the issuer
 512       const unsigned receive_position =
 513           std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 514             const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 515             if (e_receive != nullptr) {
 516               return e_receive->get_mailbox() == issuer_mailbox;
 517             }
 518             return false;
 519           });
 520
 521       if (send_position == receive_position) {
 522         exC.insert(U->discover_event(std::move(K), test_action));
 523       }
 524     }
 525   } else {
 526     xbt_die("The transition which created the communication on which `%s` waits "
 527             "is neither an async send nor an async receive. The current UDPOR "
 528             "implementation does not know how to check if `CommWait` is enabled in "
 529             "this case. Was a new transition added?",
 530             e_issuer->get_transition()->to_string().c_str());
 531   }
 532   return exC;
 533 }
 534
 535 EventSet ExtensionSetCalculator::partially_extend_MutexAsyncLock(const Configuration& C, Unfolding* U,
 536                                                                  std::shared_ptr<Transition> action)
 537 {
 538   EventSet exC;
 539   const auto mutex_lock    = std::static_pointer_cast<MutexTransition>(std::move(action));
 540   const auto pre_event_a_C = C.pre_event(mutex_lock->aid_);
 541
 542   // for each event e in C
 543   // 1. If lambda(e) := pre(a) -> add it. Note that if
 544   // pre_event_a_C.has_value() == false, this implies `C` is
 545   // empty or which we treat as implicitly containing the bottom event
 546   if (pre_event_a_C.has_value()) {
 547     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_lock);
 548     exC.insert(e_prime);
 549   } else {
 550     const auto e_prime = U->discover_event(EventSet(), mutex_lock);
 551     exC.insert(e_prime);
 552   }
 553
 554   // for each event e in C
 555   for (const auto e : C) {
 556     // Check for other locks on the same mutex
 557     if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
 558         e_mutex != nullptr) {
 559
 560       if (e_mutex->type_ == Transition::Type::MUTEX_ASYNC_LOCK && mutex_lock->get_mutex() == e_mutex->get_mutex()) {
 561         const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
 562         exC.insert(U->discover_event(std::move(K), mutex_lock));
 563       }
 564     }
 565   }
 566   return exC;
 567 }
 568
 569 EventSet ExtensionSetCalculator::partially_extend_MutexUnlock(const Configuration& C, Unfolding* U,
 570                                                               std::shared_ptr<Transition> action)
 571 {
 572   EventSet exC;
 573   const auto mutex_unlock  = std::static_pointer_cast<MutexTransition>(std::move(action));
 574   const auto pre_event_a_C = C.pre_event(mutex_unlock->aid_);
 575
 576   // for each event e in C
 577   // 1. If lambda(e) := pre(a) -> add it. Note that if
 578   // pre_event_a_C.has_value() == false, this implies `C` is
 579   // empty or which we treat as implicitly containing the bottom event
 580   if (pre_event_a_C.has_value()) {
 581     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_unlock);
 582     exC.insert(e_prime);
 583   } else {
 584     const auto e_prime = U->discover_event(EventSet(), mutex_unlock);
 585     exC.insert(e_prime);
 586   }
 587
 588   // for each event e in C
 589   for (const auto e : C) {
 590     // Check for MutexTest
 591     if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
 592         e_mutex != nullptr) {
 593
 594       if (e_mutex->type_ == Transition::Type::MUTEX_TEST || e_mutex->type_ == Transition::Type::MUTEX_WAIT) {
 595         // TODO: Check if dependent or not
 596         // This entails getting information about
 597         // the relative position of the mutex in the queue, which
 598         // again means we need more context...
 599         const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
 600         exC.insert(U->discover_event(std::move(K), mutex_unlock));
 601       }
 602     }
 603   }
 604   return exC;
 605 }
 606
 607 EventSet ExtensionSetCalculator::partially_extend_MutexWait(const Configuration& C, Unfolding* U,
 608                                                             std::shared_ptr<Transition> action)
 609 {
 610   EventSet exC;
 611   const auto mutex_wait    = std::static_pointer_cast<MutexTransition>(std::move(action));
 612   const auto pre_event_a_C = C.pre_event(mutex_wait->aid_);
 613
 614   // for each event e in C
 615   // 1. If lambda(e) := pre(a) -> add it. In the case of MutexWait, we also check that the
 616   // actor which is executing the MutexWait is the owner of the mutex
 617   if (pre_event_a_C.has_value() && mutex_wait->get_owner() == mutex_wait->aid_) {
 618     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_wait);
 619     exC.insert(e_prime);
 620   } else {
 621     const auto e_prime = U->discover_event(EventSet(), mutex_wait);
 622     exC.insert(e_prime);
 623   }
 624
 625   // for each event e in C
 626   for (const auto e : C) {
 627     // Check for any unlocks
 628     if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
 629         e_mutex != nullptr && e_mutex->type_ == Transition::Type::MUTEX_UNLOCK) {
 630       // TODO: Check if dependent or not
 631       // This entails getting information about
 632       // the relative position of the mutex in the queue, which
 633       // again means we need more context...
 634       const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
 635       exC.insert(U->discover_event(std::move(K), mutex_wait));
 636     }
 637   }
 638   return exC;
 639 }
 640
 641 EventSet ExtensionSetCalculator::partially_extend_MutexTest(const Configuration& C, Unfolding* U,
 642                                                             std::shared_ptr<Transition> action)
 643 {
 644   EventSet exC;
 645   const auto mutex_test    = std::static_pointer_cast<MutexTransition>(std::move(action));
 646   const auto pre_event_a_C = C.pre_event(mutex_test->aid_);
 647
 648   // for each event e in C
 649   // 1. If lambda(e) := pre(a) -> add it. Note that if
 650   // pre_evevnt_a_C.has_value() == false, this implies `C` is
 651   // empty or which we treat as implicitly containing the bottom event
 652   if (pre_event_a_C.has_value()) {
 653     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), mutex_test);
 654     exC.insert(e_prime);
 655   } else {
 656     const auto e_prime = U->discover_event(EventSet(), mutex_test);
 657     exC.insert(e_prime);
 658   }
 659
 660   // for each event e in C
 661   for (const auto e : C) {
 662     // Check for any unlocks
 663     if (const MutexTransition* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
 664         e_mutex != nullptr && e_mutex->type_ == Transition::Type::MUTEX_UNLOCK) {
 665       // TODO: Check if dependent or not
 666       // This entails getting information about
 667       // the relative position of the mutex in the queue, which
 668       // again means we need more context...
 669       const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
 670       exC.insert(U->discover_event(std::move(K), mutex_test));
 671     }
 672   }
 673   return exC;
 674 }
 675
 676 EventSet ExtensionSetCalculator::partially_extend_ActorJoin(const Configuration& C, Unfolding* U,
 677                                                             std::shared_ptr<Transition> action)
 678 {
 679   EventSet exC;
 680
 681   const auto join_action   = std::static_pointer_cast<ActorJoinTransition>(std::move(action));
 682   const auto pre_event_a_C = C.pre_event(join_action->aid_);
 683
 684   // Handling ActorJoin is very simple: it is independent with all
 685   // other transitions. Thus the only event it could possibly depend
 686   // on is pre(a, C) or the root
 687   if (pre_event_a_C.has_value()) {
 688     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), join_action);
 689     exC.insert(e_prime);
 690   } else {
 691     const auto e_prime = U->discover_event(EventSet(), join_action);
 692     exC.insert(e_prime);
 693   }
 694
 695   return exC;
 696 }
 697
 698 } // namespace simgrid::mc::udpor