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 <memory>
  14 #include <string>
  15
  16 namespace simgrid::mc::udpor {
  17
  18 class UnfoldingEvent {
  19 public:
  20   UnfoldingEvent(std::shared_ptr<Transition> transition = std::make_unique<Transition>(),
  21                  EventSet immediate_causes = EventSet(), unsigned long event_id = 0);
  22
  23   UnfoldingEvent(const UnfoldingEvent&)            = default;
  24   UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
  25   UnfoldingEvent(UnfoldingEvent&&)                 = default;
  26
  27   EventSet get_history() const;
  28   bool in_history_of(const UnfoldingEvent* otherEvent) const;
  29
  30   bool conflicts_with(const UnfoldingEvent* otherEvent) const;
  31   bool conflicts_with(const Configuration& config) const;
  32   bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
  33
  34   Transition* get_transition() const { return this->associated_transition.get(); }
  35
  36   bool operator==(const UnfoldingEvent&) const;
  37
  38 private:
  39   /**
  40    * @brief The transition that UDPOR "attaches" to this
  41    * specific event for later use while computing e.g. extension
  42    * sets
  43    *
  44    * The transition points to that of a particular actor
  45    * in the state reached by the configuration C (recall
  46    * this is denoted `state(C)`) that excludes this event.
  47    * In other words, this transition was the "next" event
  48    * of the actor that executes it in `state(C)`.
  49    */
  50   std::shared_ptr<Transition> associated_transition;
  51
  52   /**
  53    * @brief The "immediate" causes of this event.
  54    *
  55    * An event `e` is an immediate cause of an event `e'` if
  56    *
  57    * 1. e < e'
  58    * 2. There is no event `e''` in E such that
  59    * `e < e''` and `e'' < e'`
  60    *
  61    * Intuitively, an immediate cause "happened right before"
  62    * this event was executed. It is sufficient to store
  63    * only the immediate causes of any event `e`, as any indirect
  64    * causes of that event would either be an indirect cause
  65    * or an immediate cause of the immediate causes of `e`, and
  66    * so on.
  67    */
  68   EventSet immediate_causes;
  69
  70   unsigned long event_id = 0;
  71 };
  72
  73 } // namespace simgrid::mc::udpor
  74 #endif