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
  33   if (const auto handler = handlers.find(action->type_); handler != handlers.end()) {
  34     return handler->second(C, U, std::move(action));
  35   } else {
  36     xbt_assert(false,
  37                "There is currently no specialized computation for the transition "
  38                "'%s' for computing extension sets in UDPOR, so the model checker cannot "
  39                "determine how to proceed. Please submit a bug report requesting "
  40                "that the transition be supported in SimGrid using UDPOR and consider "
  41                "using the other model-checking algorithms supported by SimGrid instead "
  42                "in the meantime",
  43                action->to_string().c_str());
  44     DIE_IMPOSSIBLE;
  45   }
  46 }
  47
  48 EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& C, Unfolding* U,
  49                                                            const std::shared_ptr<Transition> action)
  50 {
  51   EventSet exC;
  52
  53   const auto send_action        = std::static_pointer_cast<CommSendTransition>(std::move(action));
  54   const auto pre_event_a_C      = C.pre_event(send_action->aid_);
  55   const unsigned sender_mailbox = send_action->get_mailbox();
  56
  57   // 1. Create `e' := <a, config(preEvt(a, C))>` and add `e'` to `ex(C)`
  58   // NOTE: If `preEvt(a, C)` doesn't exist, we're effectively asking
  59   // about `config({})`
  60   if (pre_event_a_C.has_value()) {
  61     const auto* e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), send_action);
  62     exC.insert(e_prime);
  63   } else {
  64     const auto* e_prime = U->discover_event(EventSet(), send_action);
  65     exC.insert(e_prime);
  66   }
  67
  68   // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
  69   // Com contains a matching c' = AsyncReceive(m, _) with `action`
  70   for (const auto e : C) {
  71     const bool transition_type_check = [&]() {
  72       if (const auto* async_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
  73           async_send != nullptr) {
  74         return async_send->get_mailbox() == sender_mailbox;
  75       }
  76       // TODO: Add `TestAny` dependency
  77       return false;
  78     }();
  79
  80     if (transition_type_check) {
  81       const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
  82
  83       // TODO: Check D_K(a, lambda(e))
  84       if (true) {
  85         const auto* e_prime = U->discover_event(std::move(K), send_action);
  86         exC.insert(e_prime);
  87       }
  88     }
  89   }
  90
  91   // TODO: Add `TestAny` dependency case
  92   return exC;
  93 }
  94
  95 EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& C, Unfolding* U,
  96                                                            const std::shared_ptr<Transition> action)
  97 {
  98   EventSet exC;
  99
 100   const auto recv_action      = std::static_pointer_cast<CommRecvTransition>(std::move(action));
 101   const unsigned recv_mailbox = recv_action->get_mailbox();
 102   const auto pre_event_a_C    = C.pre_event(recv_action->aid_);
 103
 104   // 1. Create `e' := <a, config(preEvt(a, C))>` and add `e'` to `ex(C)`
 105   if (pre_event_a_C.has_value()) {
 106     const auto* e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), recv_action);
 107     exC.insert(e_prime);
 108   } else {
 109     const auto* e_prime = U->discover_event(EventSet(), recv_action);
 110     exC.insert(e_prime);
 111   }
 112
 113   // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
 114   // Com contains a matching c' = AsyncReceive(m, _) with a
 115   for (const auto e : C) {
 116     const bool transition_type_check = [&]() {
 117       if (const auto* async_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 118           async_recv != nullptr && async_recv->get_mailbox() == recv_mailbox) {
 119         return true;
 120       }
 121       // TODO: Add `TestAny` dependency
 122       return false;
 123     }();
 124
 125     if (transition_type_check) {
 126       const EventSet K = EventSet({e, pre_event_a_C.value_or(e)}).get_largest_maximal_subset();
 127
 128       // TODO: Check D_K(a, lambda(e)) (ony matters in the case of TestAny)
 129       if (true) {
 130         const auto* e_prime = U->discover_event(std::move(K), recv_action);
 131         exC.insert(e_prime);
 132       }
 133     }
 134   }
 135
 136   // TODO: Add `TestAny` dependency case
 137   return exC;
 138 }
 139
 140 EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration& C, Unfolding* U,
 141                                                            std::shared_ptr<Transition> action)
 142 {
 143   EventSet exC;
 144
 145   const auto wait_action   = std::static_pointer_cast<CommWaitTransition>(std::move(action));
 146   const auto wait_comm     = wait_action->get_comm();
 147   const auto pre_event_a_C = C.pre_event(wait_action->aid_);
 148
 149   // Determine the _issuer_ of the communication of the `CommWait` event
 150   // in `C`. The issuer of the `CommWait` in `C` is the event in `C`
 151   // whose transition is the `CommRecv` or `CommSend` whose resulting
 152   // communication this `CommWait` waits on
 153   const auto issuer = std::find_if(C.begin(), C.end(), [&](const UnfoldingEvent* e) {
 154     if (const CommRecvTransition* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 155         e_issuer_receive != nullptr) {
 156       return e_issuer_receive->aid_ == wait_action->aid_ && wait_comm == e_issuer_receive->get_comm();
 157     }
 158
 159     if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 160         e_issuer_send != nullptr) {
 161       return e_issuer_send->aid_ == wait_action->aid_ && wait_comm == e_issuer_send->get_comm();
 162     }
 163
 164     return false;
 165   });
 166   xbt_assert(issuer != C.end(),
 167              "Invariant violation! A (supposedly) enabled `CommWait` transition "
 168              "waiting on communication %lu should not be enabled: the receive/send "
 169              "transition which generated the communication is not an action taken "
 170              "to reach state(C) (the state of the configuration), which should "
 171              "be an impossibility if `%s` is enabled. Please report this as "
 172              "a bug in SimGrid's UDPOR implementation",
 173              wait_action->get_comm(), wait_action->to_string(false).c_str());
 174   const UnfoldingEvent* e_issuer = *issuer;
 175   const History e_issuer_history(e_issuer);
 176
 177   // 1. if `a` is enabled at state(config({preEvt(a,C)})), then
 178   // create `e' := <a, config({preEvt(a,C)})>` and add `e'` to `ex(C)`
 179   //
 180   // First, if `pre_event_a_C == std::nullopt`, then there is nothing to
 181   // do: `CommWait` will never be enabled in the empty configuration (at
 182   // least two actions must be executed before)
 183   if (pre_event_a_C.has_value(); const auto* unwrapped_pre_event = pre_event_a_C.value()) {
 184     // A necessary condition is that the issuer be present in
 185     // config({preEvt(a, C)}); otherwise, the `CommWait` could not
 186     // be enabled since the communication on which it waits would not
 187     // have been created for it!
 188     if (const auto config_pre_event = History(unwrapped_pre_event); config_pre_event.contains(e_issuer)) {
 189       // If the issuer is a `CommRecv` (resp. `CommSend`), then we check that there
 190       // are at least as many `CommSend` (resp. `CommRecv`) transitions in `config_pre_event`
 191       // as needed to reach the receive/send number that is `issuer`.
 192       // ...
 193       // ...
 194       if (const CommRecvTransition* e_issuer_receive =
 195               dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 196           e_issuer_receive != nullptr) {
 197         const unsigned issuer_mailbox = e_issuer_receive->get_mailbox();
 198
 199         // Check from the config -> how many sends have there been
 200         const unsigned send_position =
 201             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
 202               const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 203               if (e_send != nullptr) {
 204                 return e_send->get_mailbox() == issuer_mailbox;
 205               }
 206               return false;
 207             });
 208
 209         // Check from e_issuer -> what place is the issuer in?
 210         const unsigned receive_position =
 211             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 212               const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 213               if (e_receive != nullptr) {
 214                 return e_receive->get_mailbox() == issuer_mailbox;
 215               }
 216               return false;
 217             });
 218
 219         if (send_position >= receive_position) {
 220           exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
 221         }
 222
 223       } else if (const CommSendTransition* e_issuer_send =
 224                      dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 225                  e_issuer_send != nullptr) {
 226         const unsigned issuer_mailbox = e_issuer_send->get_mailbox();
 227
 228         // Check from e_issuer -> what place is the issuer in?
 229         const unsigned send_position =
 230             std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 231               const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 232               if (e_send != nullptr) {
 233                 return e_send->get_mailbox() == issuer_mailbox;
 234               }
 235               return false;
 236             });
 237
 238         // Check from the config -> how many sends have there been
 239         const unsigned receive_position =
 240             std::count_if(config_pre_event.begin(), config_pre_event.end(), [=](const auto e) {
 241               const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 242               if (e_receive != nullptr) {
 243                 return e_receive->get_mailbox() == issuer_mailbox;
 244               }
 245               return false;
 246             });
 247
 248         if (send_position <= receive_position) {
 249           exC.insert(U->discover_event(EventSet({unwrapped_pre_event}), wait_action));
 250         }
 251
 252       } else {
 253         xbt_die("The transition which created the communication on which `%s` waits "
 254                 "is neither an async send nor an async receive. The current UDPOR "
 255                 "implementation does not know how to check if `CommWait` is enabled in "
 256                 "this case. Was a new transition added?",
 257                 e_issuer->get_transition()->to_string().c_str());
 258       }
 259     }
 260   }
 261
 262   // 3. foreach event e in C do
 263   if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 264       e_issuer_send != nullptr) {
 265     for (const auto e : C) {
 266       // If the provider of the communication for `CommWait` is a
 267       // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
 268       // All other actions would be independent with the wait action (including
 269       // another `CommSend` to the same mailbox: `CommWait` is "waiting" for its
 270       // corresponding receive action)
 271       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_RECV) {
 272         continue;
 273       }
 274
 275       const auto issuer_mailbox        = e_issuer_send->get_mailbox();
 276       const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 277       if (e_recv->get_mailbox() != issuer_mailbox) {
 278         continue;
 279       }
 280
 281       // If the `issuer` is not in `config(K)`, this implies that
 282       // `WaitAny()` is always disabled in `config(K)`; hence, it
 283       // is independent of any transition in `config(K)` (according
 284       // to formal definition of independence)
 285       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 286       const auto config_K = History(K);
 287       if (not config_K.contains(e_issuer)) {
 288         continue;
 289       }
 290
 291       // What send # is the issuer
 292       const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 293         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 294         if (e_send != nullptr) {
 295           return e_send->get_mailbox() == issuer_mailbox;
 296         }
 297         return false;
 298       });
 299
 300       // What receive # is the event `e`?
 301       const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 302         const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 303         if (e_receive != nullptr) {
 304           return e_receive->get_mailbox() == issuer_mailbox;
 305         }
 306         return false;
 307       });
 308
 309       if (send_position == receive_position) {
 310         exC.insert(U->discover_event(std::move(K), wait_action));
 311       }
 312     }
 313   } else if (const CommRecvTransition* e_issuer_recv =
 314                  dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 315              e_issuer_recv != nullptr) {
 316     for (const auto e : C) {
 317       // If the provider of the communication for `CommWait` is a
 318       // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
 319       // All other actions would be independent with the wait action (including
 320       // another `CommRecv` to the same mailbox: `CommWait` is "waiting" for its
 321       // corresponding send action)
 322       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_SEND) {
 323         continue;
 324       }
 325
 326       const auto issuer_mailbox        = e_issuer_recv->get_mailbox();
 327       const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 328       if (e_send->get_mailbox() != issuer_mailbox) {
 329         continue;
 330       }
 331
 332       // If the `issuer` is not in `config(K)`, this implies that
 333       // `WaitAny()` is always disabled in `config(K)`; hence, it
 334       // is independent of any transition in `config(K)` (according
 335       // to formal definition of independence)
 336       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 337       const auto config_K = History(K);
 338       if (not config_K.contains(e_issuer)) {
 339         continue;
 340       }
 341
 342       // What receive # is the event `e`?
 343       const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 344         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 345         if (e_send != nullptr) {
 346           return e_send->get_mailbox() == issuer_mailbox;
 347         }
 348         return false;
 349       });
 350
 351       // What send # is the issuer
 352       const unsigned receive_position =
 353           std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 354             const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 355             if (e_receive != nullptr) {
 356               return e_receive->get_mailbox() == issuer_mailbox;
 357             }
 358             return false;
 359           });
 360
 361       if (send_position == receive_position) {
 362         exC.insert(U->discover_event(std::move(K), wait_action));
 363       }
 364     }
 365   } else {
 366     xbt_die("The transition which created the communication on which `%s` waits "
 367             "is neither an async send nor an async receive. The current UDPOR "
 368             "implementation does not know how to check if `CommWait` is enabled in "
 369             "this case. Was a new transition added?",
 370             e_issuer->get_transition()->to_string().c_str());
 371   }
 372
 373   return exC;
 374 }
 375
 376 EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration& C, Unfolding* U,
 377                                                            std::shared_ptr<Transition> action)
 378 {
 379   EventSet exC;
 380
 381   const auto test_action   = std::static_pointer_cast<CommTestTransition>(std::move(action));
 382   const auto test_comm     = test_action->get_comm();
 383   const auto test_aid      = test_action->aid_;
 384   const auto pre_event_a_C = C.pre_event(test_action->aid_);
 385
 386   // Add the previous event as a dependency (if it's there)
 387   if (pre_event_a_C.has_value()) {
 388     const auto e_prime = U->discover_event(EventSet({pre_event_a_C.value()}), test_action);
 389     exC.insert(e_prime);
 390   }
 391
 392   // Determine the _issuer_ of the communication of the `CommTest` event
 393   // in `C`. The issuer of the `CommTest` in `C` is the event in `C`
 394   // whose transition is the `CommRecv` or `CommSend` whose resulting
 395   // communication this `CommTest` tests on
 396   const auto issuer = std::find_if(C.begin(), C.end(), [=](const UnfoldingEvent* e) {
 397     if (const CommRecvTransition* e_issuer_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 398         e_issuer_receive != nullptr) {
 399       return e_issuer_receive->aid_ == test_aid && test_comm == e_issuer_receive->get_comm();
 400     }
 401
 402     if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 403         e_issuer_send != nullptr) {
 404       return e_issuer_send->aid_ == test_aid && test_comm == e_issuer_send->get_comm();
 405     }
 406
 407     return false;
 408   });
 409   xbt_assert(issuer != C.end(),
 410              "An enabled `CommTest` transition (%s) is testing a communication"
 411              "%lu not created by a receive/send "
 412              "transition. SimGrid cannot currently handle test actions "
 413              "under which a test is performed on a communication that was "
 414              "not directly created by a receive/send operation of the same actor.",
 415              test_action->to_string(false).c_str(), test_action->get_comm());
 416   const UnfoldingEvent* e_issuer = *issuer;
 417   const History e_issuer_history(e_issuer);
 418
 419   // 3. foreach event e in C do
 420   if (const CommSendTransition* e_issuer_send = dynamic_cast<const CommSendTransition*>(e_issuer->get_transition());
 421       e_issuer_send != nullptr) {
 422     for (const auto e : C) {
 423       // If the provider of the communication for `CommTest` is a
 424       // `CommSend(m)`, then we only care about `e` if `λ(e) == `CommRecv(m)`.
 425       // All other actions would be independent with the test action (including
 426       // another `CommSend` to the same mailbox: `CommTest` is testing the
 427       // corresponding receive action)
 428       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_RECV) {
 429         continue;
 430       }
 431
 432       const auto issuer_mailbox = e_issuer_send->get_mailbox();
 433
 434       if (const CommRecvTransition* e_recv = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 435           e_recv->get_mailbox() != issuer_mailbox) {
 436         continue;
 437       }
 438
 439       // If the `issuer` is not in `config(K)`, this implies that
 440       // `CommTest()` is always disabled in `config(K)`; hence, it
 441       // is independent of any transition in `config(K)` (according
 442       // to formal definition of independence)
 443       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 444       const auto config_K = History(K);
 445       if (not config_K.contains(e_issuer)) {
 446         continue;
 447       }
 448
 449       // What send # is the issuer
 450       const unsigned send_position = std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 451         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 452         if (e_send != nullptr) {
 453           return e_send->get_mailbox() == issuer_mailbox;
 454         }
 455         return false;
 456       });
 457
 458       // What receive # is the event `e`?
 459       const unsigned receive_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 460         const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 461         if (e_receive != nullptr) {
 462           return e_receive->get_mailbox() == issuer_mailbox;
 463         }
 464         return false;
 465       });
 466
 467       if (send_position == receive_position) {
 468         exC.insert(U->discover_event(std::move(K), test_action));
 469       }
 470     }
 471   } else if (const CommRecvTransition* e_issuer_recv =
 472                  dynamic_cast<const CommRecvTransition*>(e_issuer->get_transition());
 473              e_issuer_recv != nullptr) {
 474
 475     for (const auto e : C) {
 476       // If the provider of the communication for `CommTest` is a
 477       // `CommRecv(m)`, then we only care about `e` if `λ(e) == `CommSend(m)`.
 478       // All other actions would be independent with the wait action (including
 479       // another `CommRecv` to the same mailbox: `CommWait` is "waiting" for its
 480       // corresponding send action)
 481       if (e->get_transition()->type_ != Transition::Type::COMM_ASYNC_SEND) {
 482         continue;
 483       }
 484
 485       const auto issuer_mailbox        = e_issuer_recv->get_mailbox();
 486       const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 487       if (e_send->get_mailbox() != issuer_mailbox) {
 488         continue;
 489       }
 490
 491       // If the `issuer` is not in `config(K)`, this implies that
 492       // `WaitAny()` is always disabled in `config(K)`; hence, it
 493       // is independent of any transition in `config(K)` (according
 494       // to formal definition of independence)
 495       const EventSet K    = EventSet({e, pre_event_a_C.value_or(e)});
 496       const auto config_K = History(K);
 497       if (not config_K.contains(e_issuer)) {
 498         continue;
 499       }
 500
 501       // What receive # is the event `e`?
 502       const unsigned send_position = std::count_if(config_K.begin(), config_K.end(), [=](const auto e) {
 503         const CommSendTransition* e_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
 504         if (e_send != nullptr) {
 505           return e_send->get_mailbox() == issuer_mailbox;
 506         }
 507         return false;
 508       });
 509
 510       // What send # is the issuer
 511       const unsigned receive_position =
 512           std::count_if(e_issuer_history.begin(), e_issuer_history.end(), [=](const auto e) {
 513             const CommRecvTransition* e_receive = dynamic_cast<const CommRecvTransition*>(e->get_transition());
 514             if (e_receive != nullptr) {
 515               return e_receive->get_mailbox() == issuer_mailbox;
 516             }
 517             return false;
 518           });
 519
 520       if (send_position == receive_position) {
 521         exC.insert(U->discover_event(std::move(K), test_action));
 522       }
 523     }
 524   } else {
 525     xbt_die("The transition which created the communication on which `%s` waits "
 526             "is neither an async send nor an async receive. The current UDPOR "
 527             "implementation does not know how to check if `CommWait` is enabled in "
 528             "this case. Was a new transition added?",
 529             e_issuer->get_transition()->to_string().c_str());
 530   }
 531
 532   return exC;
 533 }
 534
 535 } // namespace simgrid::mc::udpor