src/mc/explo/udpor/UnfoldingEvent.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_EVENT_HPP
   7 #define SIMGRID_MC_UDPOR_UNFOLDING_EVENT_HPP
   8
   9 #include "src/mc/explo/udpor/EventSet.hpp"
  10 #include "src/mc/explo/udpor/udpor_forward.hpp"
  11 #include "src/mc/transition/Transition.hpp"
  12
  13 #include <initializer_list>
  14 #include <memory>
  15 #include <string>
  16
  17 namespace simgrid::mc::udpor {
  18
  19 class UnfoldingEvent {
  20 public:
  21   explicit UnfoldingEvent(std::initializer_list<const UnfoldingEvent*> init_list);
  22   UnfoldingEvent(EventSet immediate_causes              = EventSet(),
  23                  std::shared_ptr<Transition> transition = std::make_unique<Transition>());
  24
  25   UnfoldingEvent(const UnfoldingEvent&)            = default;
  26   UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
  27   UnfoldingEvent(UnfoldingEvent&&)                 = default;
  28
  29   EventSet get_history() const;
  30   EventSet get_local_config() const;
  31   bool in_history_of(const UnfoldingEvent* other) const;
  32
  33   /**
  34    * @brief Whether or not the given event is a decendant
  35    * of or an ancestor of the given event
  36    */
  37   bool related_to(const UnfoldingEvent* other) const;
  38
  39   /// @brief Whether or not this event is in conflict with
  40   /// the given one (i.e. whether `this # other`)
  41   bool conflicts_with(const UnfoldingEvent* other) const;
  42
  43   /// @brief Whether or not this event is in conflict with
  44   /// any event in the given set
  45   bool conflicts_with_any(const EventSet& events) const;
  46
  47   /// @brief Computes "this #ⁱ other"
  48   bool immediately_conflicts_with(const UnfoldingEvent* other) const;
  49   bool is_dependent_with(const Transition*) const;
  50   bool is_dependent_with(const UnfoldingEvent* other) const;
  51
  52   unsigned get_id() const { return this->id; }
  53   aid_t get_actor() const { return get_transition()->aid_; }
  54   const EventSet& get_immediate_causes() const { return this->immediate_causes; }
  55   Transition* get_transition() const { return this->associated_transition.get(); }
  56
  57   void set_transition(std::shared_ptr<Transition> t) { this->associated_transition = std::move(t); }
  58
  59   std::string to_string() const;
  60
  61   bool operator==(const UnfoldingEvent&) const;
  62   bool operator!=(const UnfoldingEvent& other) const { return not(*this == other); }
  63
  64 private:
  65   /**
  66    * @brief The transition that UDPOR "attaches" to this
  67    * specific event for later use while computing e.g. extension
  68    * sets
  69    *
  70    * The transition points to that of a particular actor
  71    * in the state reached by the configuration C (recall
  72    * this is denoted `state(C)`) that excludes this event.
  73    * In other words, this transition was the "next" event
  74    * of the actor that executes it in `state(C)`.
  75    */
  76   std::shared_ptr<Transition> associated_transition;
  77
  78   /**
  79    * @brief The "immediate" causes of this event.
  80    *
  81    * An event `e` is an immediate cause of an event `e'` if
  82    *
  83    * 1. e < e'
  84    * 2. There is no event `e''` in E such that
  85    * `e < e''` and `e'' < e'`
  86    *
  87    * Intuitively, an immediate cause "happened right before"
  88    * this event was executed. It is sufficient to store
  89    * only the immediate causes of any event `e`, as any indirect
  90    * causes of that event would either be an indirect cause
  91    * or an immediate cause of the immediate causes of `e`, and
  92    * so on.
  93    */
  94   EventSet immediate_causes;
  95
  96   /**
  97    * @brief An identifier which is used to sort events
  98    * deterministically
  99    */
 100   uint64_t id = 0;
 101 };
 102
 103 } // namespace simgrid::mc::udpor
 104 #endif