X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/29fc93df5d19fd8fdf5d52359726988ed5d4fe83..9307ac7861b490d95759a67b7cb0bfc25d349577:/src/mc/explo/odpor/Execution.hpp

diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp
index dca1c5df74..7903f61981 100644
--- a/src/mc/explo/odpor/Execution.hpp
+++ b/src/mc/explo/odpor/Execution.hpp
@@ -8,6 +8,8 @@
 
 #include "src/mc/api/ClockVector.hpp"
 #include "src/mc/explo/odpor/odpor_forward.hpp"
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/mc_record.hpp"
 #include "src/mc/transition/Transition.hpp"
 
 #include <list>
@@ -17,10 +19,6 @@
 
 namespace simgrid::mc::odpor {
 
-using ProcessSequence   = std::list<aid_t>;
-using ExecutionSequence = std::list<const State*>;
-using Hypothetical      = ExecutionSequence;
-
 /**
  * @brief The occurrence of a transition in an execution
  *
@@ -29,16 +27,16 @@ using Hypothetical      = ExecutionSequence;
  * actor `j`
  */
 class Event {
-  std::pair<const Transition*, ClockVector> contents_;
+  std::pair<std::shared_ptr<Transition>, ClockVector> contents_;
 
 public:
   Event()                        = default;
   Event(Event&&)                 = default;
   Event(const Event&)            = default;
   Event& operator=(const Event&) = default;
-  explicit Event(std::pair<const Transition*, ClockVector> pair) : contents_(std::move(pair)) {}
+  explicit Event(std::pair<std::shared_ptr<Transition>, ClockVector> pair) : contents_(std::move(pair)) {}
 
-  const Transition* get_transition() const { return std::get<0>(contents_); }
+  std::shared_ptr<Transition> get_transition() const { return std::get<0>(contents_); }
   const ClockVector& get_clock_vector() const { return std::get<1>(contents_); }
 };
 
@@ -84,12 +82,7 @@ public:
  */
 class Execution {
 private:
-  /**
-   * @brief The actual steps that are taken by the process
-   * during exploration, relative to the
-   */
   std::vector<Event> contents_;
-
   Execution(std::vector<Event>&& contents) : contents_(std::move(contents)) {}
 
 public:
@@ -100,8 +93,6 @@ public:
   Execution(const Execution&)            = default;
   Execution& operator=(Execution const&) = default;
   Execution(Execution&&)                 = default;
-  Execution(ExecutionSequence&& seq);
-  Execution(const ExecutionSequence& seq);
 
   size_t size() const { return this->contents_.size(); }
   bool empty() const { return this->contents_.empty(); }
@@ -150,6 +141,27 @@ public:
    */
   std::optional<aid_t> get_first_sdpor_initial_from(EventHandle e, std::unordered_set<aid_t> backtrack_set) const;
 
+  /**
+   * @brief For a given sequence of actors `v` and a sequence of transitions `w`,
+   * computes the sequence, if any, that should be inserted as a child a wakeup tree for
+   * this execution
+   */
+  std::optional<PartialExecution> get_shortest_odpor_sq_subset_insertion(const PartialExecution& v,
+                                                                         const PartialExecution& w) const;
+
+  /**
+   * @brief For a given reversible race
+   *
+   * @invariant: This method assumes that events `e` and
+   * `e_prime` are in a *reversible* race as is the case
+   * in ODPOR
+   */
+  std::optional<PartialExecution> get_odpor_extension_from(EventHandle e, EventHandle e_prime,
+                                                           const State& state_at_e) const;
+
+  bool is_initial_after_execution(const PartialExecution& w, aid_t p) const;
+  bool is_independent_with_execution(const PartialExecution& w, std::shared_ptr<Transition> next_E_p) const;
+
   /**
    * @brief Determines the event associated with
    * the given handle `handle`
@@ -162,6 +174,15 @@ public:
    */
   aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; }
 
+  /**
+   * @brief Returns a handle to the newest event of the execution,
+   * if such an event exists
+   */
+  std::optional<EventHandle> get_latest_event_handle() const
+  {
+    return contents_.empty() ? std::nullopt : std::optional<EventHandle>{static_cast<EventHandle>(size() - 1)};
+  }
+
   /**
    * @brief Returns a set of events which are in
    * "immediate conflict" (according to the definition given
@@ -183,15 +204,6 @@ public:
    */
   std::unordered_set<EventHandle> get_racing_events_of(EventHandle handle) const;
 
-  /**
-   * @brief Returns a handle to the newest event of the execution,
-   * if such an event exists
-   */
-  std::optional<EventHandle> get_latest_event_handle() const
-  {
-    return contents_.empty() ? std::nullopt : std::optional<EventHandle>{static_cast<EventHandle>(size() - 1)};
-  }
-
   /**
    * @brief Computes `pre(e, E)` as described in ODPOR [1]
    *
@@ -202,7 +214,7 @@ public:
    * causes that permitted event `e` to exist (roughly
    * speaking)
    */
-  Execution get_prefix_up_to(EventHandle) const;
+  Execution get_prefix_before(EventHandle) const;
 
   /**
    * @brief Whether the event represented by `e1`
@@ -232,7 +244,7 @@ public:
    * notation of [1]) `E.proc(t)` where `proc(t)` is the
    * actor which executed transition `t`.
    */
-  void push_transition(const Transition*);
+  void push_transition(std::shared_ptr<Transition>);
 };
 
 } // namespace simgrid::mc::odpor