Merge branch 'master' of https://framagit.org/simgrid/simgrid

[simgrid.git] / src / mc / explo / odpor / Execution.hpp

diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp
index cfe24bd54476bdab91b6193e206ffb4ead3d62d1..f3bd7eddb177e5deb71eb8137c97826a9c36c785 100644 (file)
--- a/src/mc/explo/odpor/Execution.hpp
+++ b/src/mc/explo/odpor/Execution.hpp
@@ -19,6 +19,8 @@
 
 namespace simgrid::mc::odpor {
 
+std::vector<std::string> get_textual_trace(const PartialExecution& w);
+
 /**
  * @brief The occurrence of a transition in an execution
  *
@@ -86,13 +88,15 @@ private:
   Execution(std::vector<Event>&& contents) : contents_(std::move(contents)) {}
 
 public:
-  using Handle      = decltype(contents_)::const_iterator;
   using EventHandle = uint32_t;
 
   Execution()                            = default;
   Execution(const Execution&)            = default;
   Execution& operator=(Execution const&) = default;
   Execution(Execution&&)                 = default;
+  Execution(const PartialExecution&);
+
+  std::vector<std::string> get_textual_trace() const;
 
   size_t size() const { return this->contents_.size(); }
   bool empty() const { return this->contents_.empty(); }
@@ -139,7 +143,8 @@ public:
    * can serve as an initial to reverse the race between `e`
    * and `e'`
    */
-  std::optional<aid_t> get_first_sdpor_initial_from(EventHandle e, std::unordered_set<aid_t> backtrack_set) const;
+  std::unordered_set<aid_t> get_missing_source_set_actors_from(EventHandle e,
+                                                               const std::unordered_set<aid_t>& backtrack_set) const;
 
   /**
    * @brief Computes the analogous lines from the SDPOR algorithm
@@ -232,6 +237,14 @@ public:
    */
   aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; }
 
+  /**
+   * @brief Determines the transition associated with the given handle `handle`
+   */
+  const Transition* get_transition_for_handle(EventHandle handle) const
+  {
+    return get_event_with_handle(handle).get_transition().get();
+  }
+
   /**
    * @brief Returns a handle to the newest event of the execution,
    * if such an event exists
@@ -262,6 +275,25 @@ public:
    */
   std::unordered_set<EventHandle> get_racing_events_of(EventHandle handle) const;
 
+  /**
+   * @brief Returns a set of events which are in a reversible
+   * race with the given event handle `handle`
+   *
+   * Two events `e` and `e'` in an execution `E` are said to
+   * be in a reversible race iff
+   *
+   * 1. `e` and `e'` race
+   * 2. In any equivalent execution sequence `E'` to `E`
+   * where `e` occurs immediately before `e'`, the actor
+   * running `e'` was enabled in the state prior to `e`
+   *
+   * @param handle the event with respect to which
+   * reversible races are computed
+   * @returns a set of event handles from which are in a reversible
+   * race with `handle`
+   */
+  std::unordered_set<EventHandle> get_reversible_races_of(EventHandle handle) const;
+
   /**
    * @brief Computes `pre(e, E)` as described in ODPOR [1]
    *
@@ -303,6 +335,11 @@ public:
    * actor which executed transition `t`.
    */
   void push_transition(std::shared_ptr<Transition>);
+
+  /**
+   * @brief Extends the execution by a sequence of steps
+   */
+  void push_partial_execution(const PartialExecution&);
 };
 
 } // namespace simgrid::mc::odpor