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