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