src/mc/explo/udpor/Configuration.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_CONFIGURATION_HPP
   7 #define SIMGRID_MC_UDPOR_CONFIGURATION_HPP
   8
   9 #include "src/mc/explo/udpor/EventSet.hpp"
  10 #include "src/mc/explo/udpor/udpor_forward.hpp"
  11
  12 namespace simgrid::mc::udpor {
  13
  14 using StateHandle = uint64_t;
  15
  16 class Configuration {
  17 public:
  18   Configuration()                                = default;
  19   Configuration(const Configuration&)            = default;
  20   Configuration& operator=(Configuration const&) = default;
  21   Configuration(Configuration&&)                 = default;
  22
  23   inline auto begin() const { return this->events_.begin(); }
  24   inline auto end() const { return this->events_.end(); }
  25   inline const EventSet& get_events() const { return this->events_; }
  26   inline const EventSet& get_maximal_events() const { return this->max_events_; }
  27
  28   void add_event(UnfoldingEvent*);
  29   UnfoldingEvent* get_latest_event() const;
  30
  31 private:
  32   /**
  33    * @brief The most recent event added to the configuration
  34    */
  35   UnfoldingEvent* newest_event = nullptr;
  36   EventSet events_;
  37
  38   /**
  39    * The <-maxmimal events of the configuration. These are
  40    * dynamically adjusted as events are added to the configuration
  41    *
  42    * @invariant: Each event that is part of this set is
  43    *
  44    * 1. a <-maxmimal event of the configuration, in the sense that
  45    * there is no event in the configuration that is "greater" than it.
  46    * In UDPOR terminology, each event does not "cause" another event
  47    *
  48    * 2. contained in the set of events `events_` which comprise
  49    * the configuration
  50    */
  51   EventSet max_events_;
  52
  53 private:
  54   void recompute_maxmimal_events(UnfoldingEvent* new_event);
  55 };
  56
  57 class UnfoldingEvent {
  58 public:
  59   UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes,
  60                  StateHandle sid);
  61   UnfoldingEvent(unsigned int nb_events, std::string const& trans_tag, EventSet const& immediate_causes);
  62   UnfoldingEvent(const UnfoldingEvent&)            = default;
  63   UnfoldingEvent& operator=(UnfoldingEvent const&) = default;
  64   UnfoldingEvent(UnfoldingEvent&&)                 = default;
  65
  66   EventSet get_history() const;
  67   bool in_history(const UnfoldingEvent* otherEvent) const;
  68
  69   bool conflicts_with(const UnfoldingEvent* otherEvent) const;
  70   bool conflicts_with(const Configuration& config) const;
  71   bool immediately_conflicts_with(const UnfoldingEvent* otherEvt) const;
  72
  73   bool operator==(const UnfoldingEvent&) const { return false; };
  74
  75   inline StateHandle get_state_id() const { return state_id; }
  76   inline void set_state_id(StateHandle sid) { state_id = sid; }
  77
  78 private:
  79   int id = -1;
  80
  81   /**
  82    * @brief The "immediate" causes of this event.
  83    *
  84    * An event `e` is an immediate cause of an event `e'` if
  85    *
  86    * 1. e < e'
  87    * 2. There is no event `e''` in E such that
  88    * `e < e''` and `e'' < e'`
  89    *
  90    * Intuitively, an immediate cause "happened right before"
  91    * this event was executed. It is sufficient to store
  92    * only the immediate causes of any event `e`, as any indirect
  93    * causes of that event would either be an indirect cause
  94    * or an immediate cause of the immediate causes of `e`, and
  95    * so on.
  96    */
  97   EventSet immediate_causes;
  98   StateHandle state_id = 0ul;
  99 };
 100
 101 class StateManager {
 102 private:
 103   using Handle = StateHandle;
 104
 105   Handle current_handle_ = 1ul;
 106   std::unordered_map<Handle, std::unique_ptr<State>> state_map_;
 107
 108 public:
 109   Handle record_state(std::unique_ptr<State>);
 110   std::optional<std::reference_wrapper<State>> get_state(Handle);
 111 };
 112
 113 } // namespace simgrid::mc::udpor
 114 #endif