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 private:
  20   /**
  21    * @brief All of the events that are currently are a part of the unfolding
  22    *
  23    * @invariant Each unfolding event maps itself to the owner of that event,
  24    * i.e. the unique pointer that owns the address. The Unfolding owns all
  25    * of the addresses that are referenced by EventSet instances and Configuration
  26    * instances. UDPOR guarantees that events are persisted for as long as necessary
  27    */
  28   std::unordered_map<const UnfoldingEvent*, std::unique_ptr<UnfoldingEvent>> global_events_;
  29
  30   /**
  31    * @brief: The collection of events in the unfolding
  32    *
  33    * @invariant: All of the events in this set are elements of `global_events_`
  34    * and is kept updated at the same time as `global_events_`
  35    */
  36   EventSet event_handles;
  37
  38   /**
  39    * @brief The "irrelevant" portions of the unfolding that do not need to be kept
  40    * around to ensure that UDPOR functions correctly
  41    *
  42    * The set `G` is another global variable maintained by the UDPOR algorithm which
  43    * is used to keep track of all events which used to be important to UDPOR.
  44    *
  45    * @note: The current implementation does not touch the set `G`. Its use is perhaps
  46    * limited to debugging and/or model-checking acyclic state spaces
  47    */
  48   EventSet G;
  49
  50 public:
  51   Unfolding()                       = default;
  52   Unfolding& operator=(Unfolding&&) = default;
  53   Unfolding(Unfolding&&)            = default;
  54
  55   void remove(const UnfoldingEvent* e);
  56   void remove(const EventSet& events);
  57   void insert(std::unique_ptr<UnfoldingEvent> e);
  58   bool contains_event_equivalent_to(const UnfoldingEvent* e) const;
  59
  60   auto begin() const { return this->event_handles.begin(); }
  61   auto end() const { return this->event_handles.end(); }
  62   auto cbegin() const { return this->event_handles.cbegin(); }
  63   auto cend() const { return this->event_handles.cend(); }
  64   size_t size() const { return this->global_events_.size(); }
  65   bool empty() const { return this->global_events_.empty(); }
  66
  67   /// @brief Computes "#ⁱ_U(e)" for the given event
  68   EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
  69 };
  70
  71 } // namespace simgrid::mc::udpor
  72 #endif