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
  31   if (const auto handler = handlers.find(action->type_); handler != handlers.end()) {
  32     return handler->second(C, U, std::move(action));
  33   } else {
  34     xbt_assert(false,
  35                "There is currently no specialized computation for the transition "
  36                "'%s' for computing extension sets in UDPOR, so the model checker cannot "
  37                "determine how to proceed. Please submit a bug report requesting "
  38                "that the transition be supported in SimGrid using UDPOR and consider "
  39                "using the other model-checking algorithms supported by SimGrid instead "
  40                "in the meantime",
  41                action->to_string().c_str());
  42     DIE_IMPOSSIBLE;
  43   }
  44 }
  45
  46 EventSet ExtensionSetCalculator::partially_extend_CommSend(const Configuration& C, Unfolding* U,
  47                                                            const std::shared_ptr<Transition> action)
  48 {
  49   EventSet exC;
  50
  51   // TODO: if this is the first action by the actor, no such previous event exists.
  52   // How do we react here? Do we say we're dependent with the root event?
  53   const auto send_action        = std::static_pointer_cast<CommSendTransition>(std::move(action));
  54   const unsigned sender_mailbox = send_action->get_mailbox();
  55   const auto pre_event_a_C      = C.pre_event(send_action->aid_).value();
  56
  57   // 1. Create `e' := <a, config(preEvt(a, C))>` and add `e'` to `ex(C)`
  58   const auto e_prime = U->discover_event(EventSet({pre_event_a_C}), send_action);
  59   exC.insert(e_prime);
  60
  61   // 2. foreach e ∈ C s.t. λ(e) ∈ {AsyncSend(m, _), TestAny(Com)} where
  62   // Com contains a matching c' = AsyncReceive(m, _) with a
  63   for (const auto e : C) {
  64     const bool transition_type_check = [&]() {
  65       if (const auto* async_send = dynamic_cast<const CommSendTransition*>(e->get_transition());
  66           e != nullptr && async_send->get_mailbox() == sender_mailbox) {
  67         return true;
  68       } else if (const auto* e_test_any = dynamic_cast<const CommTestTransition*>(e->get_transition());
  69                  e_test_any != nullptr) {
  70         // TODO: Check if there's a way to find a matching AsyncReceive -> matching when? in the history?
  71         return true;
  72       }
  73       return false;
  74     }();
  75
  76     if (transition_type_check) {
  77       const EventSet K = EventSet({e, pre_event_a_C}).get_largest_maximal_subset();
  78
  79       // TODO: How do we compute D_K(a, b)? There's a specialized
  80       // function for each case it appears, but I don't see where
  81       // `config(K)` comes in
  82       if (false) {
  83         const auto e_prime = U->discover_event(std::move(K), send_action);
  84         exC.insert(e_prime);
  85       }
  86     }
  87   }
  88
  89   return exC;
  90 }
  91
  92 EventSet ExtensionSetCalculator::partially_extend_CommRecv(const Configuration& C, Unfolding* U,
  93                                                            const std::shared_ptr<Transition> recv_action)
  94 {
  95   return EventSet();
  96 }
  97
  98 EventSet ExtensionSetCalculator::partially_extend_CommWait(const Configuration&, Unfolding* U,
  99                                                            std::shared_ptr<Transition> wait_action)
 100 {
 101   return EventSet();
 102 }
 103
 104 EventSet ExtensionSetCalculator::partially_extend_CommTest(const Configuration&, Unfolding* U,
 105                                                            std::shared_ptr<Transition> test_action)
 106 {
 107   return EventSet();
 108 }
 109
 110 } // namespace simgrid::mc::udpor