src/mc/explo/udpor/Unfolding.hpp

   1 /* Copyright (c) 2007-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 #ifndef SIMGRID_MC_UDPOR_UNFOLDING_HPP
   7 #define SIMGRID_MC_UDPOR_UNFOLDING_HPP
   8
   9 #include "src/mc/explo/udpor/EventSet.hpp"
  10 #include "src/mc/explo/udpor/UnfoldingEvent.hpp"
  11 #include "src/mc/explo/udpor/udpor_forward.hpp"
  12
  13 #include <memory>
  14 #include <unordered_map>
  15
  16 namespace simgrid::mc::udpor {
  17
  18 class Unfolding {
  19 public:
  20   Unfolding()                       = default;
  21   Unfolding& operator=(Unfolding&&) = default;
  22   Unfolding(Unfolding&&)            = default;
  23
  24   auto begin() const { return this->event_handles.begin(); }
  25   auto end() const { return this->event_handles.end(); }
  26   auto cbegin() const { return this->event_handles.cbegin(); }
  27   auto cend() const { return this->event_handles.cend(); }
  28   size_t size() const { return this->event_handles.size(); }
  29   bool empty() const { return this->event_handles.empty(); }
  30   bool contains(const UnfoldingEvent* e) const { return this->event_handles.contains(e); }
  31
  32   void remove(const UnfoldingEvent* e);
  33   void remove(const EventSet& events);
  34
  35   /// @brief Adds a new event `e` to the Unfolding if that
  36   /// event is not equivalent to any of those already contained
  37   /// in the unfolding
  38   const UnfoldingEvent* insert(std::unique_ptr<UnfoldingEvent> e);
  39
  40   /**
  41    * @brief Informs the unfolding of a (potentially) new event
  42    *
  43    * The unfolding of a concurrent program is a well-defined
  44    * structure. Given the labeled transition system (LTS) of
  45    * a program, the unfolding of that program can be determined
  46    * algorithmically. However, UDPOR does not a priori know the structure of the
  47    * unfolding as it performs its exploration. Thus, events in the
  48    * unfolding are "discovered" as they are encountered, specifically
  49    * when computing the extension sets of the configurations that
  50    * UDPOR decides to search.
  51    *
  52    * This lends itself to the following problem: the extension sets
  53    * of two different configurations may overlap one another. That
  54    * is, for two configurations C and C' explored by UDPOR where C != C',
  55    *
  56    * ex(C) - ex(C') != empty
  57    *
  58    * Hence, when extending both `C` and `C'`, any events contained in
  59    * the intersection of ex(C) and ex(C') will be attempted to be added
  60    * twice. The unfolding will notice that these events have already
  61    * been added and simply return the event already added to the unfolding
  62    *
  63    * @tparam ...Args arguments passed to the `UnfoldingEvent` constructor
  64    * @return the handle to either the newly created event OR
  65    * to an equivalent event that was already noted by the unfolding
  66    * at some point in the past
  67    */
  68   template <typename... Args> const UnfoldingEvent* discover_event(Args... args)
  69   {
  70     auto candidate_event = std::make_unique<UnfoldingEvent>(std::forward<Args>(args)...);
  71     return insert(std::move(candidate_event));
  72   }
  73
  74   /// @brief Computes "#ⁱ_U(e)" for the given event, where `U` is the set
  75   /// of the events in this unfolding
  76   EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
  77
  78 private:
  79   /**
  80    * @brief All of the events that are currently are a part of the unfolding
  81    *
  82    * @invariant Each unfolding event maps itself to the owner of that event,
  83    * i.e. the unique pointer that manages the data at the address. The Unfolding owns all
  84    * of the addresses that are referenced by EventSet instances and Configuration
  85    * instances. UDPOR guarantees that events are persisted for as long as necessary
  86    */
  87   std::unordered_map<const UnfoldingEvent*, std::unique_ptr<UnfoldingEvent>> global_events_;
  88
  89   /**
  90    * @brief: The collection of events in the unfolding
  91    *
  92    * @invariant: All of the events in this set are elements of `global_events_`
  93    * and is kept updated at the same time as `global_events_`
  94    *
  95    * @note: This is for the convenience of iteration over the unfolding
  96    */
  97   EventSet event_handles;
  98
  99   /**
 100    * @brief The "irrelevant" portions of the unfolding that do not need to be kept
 101    * around to ensure that UDPOR functions correctly
 102    *
 103    * The set `G` is another global variable maintained by the UDPOR algorithm which
 104    * is used to keep track of all events which used to be important to UDPOR.
 105    *
 106    * @note: The current implementation does not touch the set `G`. Its use is perhaps
 107    * limited to debugging and/or model-checking acyclic state spaces
 108    */
 109   EventSet G;
 110
 111   auto find_equivalent(const UnfoldingEvent* e)
 112   {
 113     return std::find_if(begin(), end(), [=](const UnfoldingEvent* e_i) { return *e == *e_i; });
 114   }
 115 };
 116
 117 } // namespace simgrid::mc::udpor
 118 #endif