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
  12 #include <string>
  13
  14 namespace simgrid::mc::udpor {
  15
  16 class UnfoldingEvent {
  17 public:
  18   UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes,
  19                  StateHandle sid);
  20   UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes);
  21   UnfoldingEvent(const UnfoldingEvent&)            = default;
  22   UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
  23   UnfoldingEvent(UnfoldingEvent&&)                 = default;
  24
  25   EventSet get_history() const;
  26   bool in_history_of(const UnfoldingEvent* otherEvent) const;
  27
  28   bool conflicts_with(const UnfoldingEvent* otherEvent) const;
  29   bool conflicts_with(const Configuration& config) const;
  30   bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
  31
  32   inline StateHandle get_state_id() const { return state_id; }
  33   inline void set_state_id(StateHandle sid) { state_id = sid; }
  34
  35   bool operator==(const UnfoldingEvent&) const
  36   {
  37     // TODO: Implement semantic equality
  38     return false;
  39   };
  40
  41 private:
  42   int id = -1;
  43
  44   /**
  45    * @brief The "immediate" causes of this event.
  46    *
  47    * An event `e` is an immediate cause of an event `e'` if
  48    *
  49    * 1. e < e'
  50    * 2. There is no event `e''` in E such that
  51    * `e < e''` and `e'' < e'`
  52    *
  53    * Intuitively, an immediate cause "happened right before"
  54    * this event was executed. It is sufficient to store
  55    * only the immediate causes of any event `e`, as any indirect
  56    * causes of that event would either be an indirect cause
  57    * or an immediate cause of the immediate causes of `e`, and
  58    * so on.
  59    */
  60   EventSet immediate_causes;
  61   StateHandle state_id = 0ul;
  62 };
  63
  64 } // namespace simgrid::mc::udpor
  65 #endif